Home
Reading
Searching
Subscribe
Sponsors
Statistics
Posting
Contact
Spam
Lists
Links
About
Hosting
Filtering
Features Download
Marketing
Archives
FAQ
Blog
 
Gmane
From: Konstantin Tretjakov <kt-HgUWewaQDNA <at> public.gmane.org>
Subject: Question regarding a simple "dependently typed IF-THEN-ELSE"
Newsgroups: gmane.comp.lang.agda
Date: Monday 10th March 2014 15:54:12 UTC (over 3 years ago)
Hello,

suppose I would like to be able to use if-then-else in something like the
following:

   f t = if t then true else zero

My current attempt at doing it (Agda 2.3.0.1, Windows) is this:

--------------------------------
module Test1 where

postulate
   Level  : Set
   lze    : Level
   lsu    : Level -> Level
   lmax   : Level -> Level -> Level

{-# BUILTIN LEVEL         Level  #-}
{-# BUILTIN LEVELZERO     lze    #-}
{-# BUILTIN LEVELSUC      lsu    #-}
{-# BUILTIN LEVELMAX      lmax   #-}


data Bool : Set where
   true false : Bool

data ℕ : Set  where
   zero : ℕ
   suc : ℕ → ℕ

{- Set level of the return type of the if-then-else operator -}
if[Level]_then_else_ : Bool → Level → Level → Level
if[Level] true then x else y = x
if[Level] false then x else y = y

{- Return type of the if-then-else operator -}
if[Set*]_then_else_ : ∀ {i j} (t : Bool) → Set i → Set j → Set
(if[Level] t then i else j)
if[Set*] true then A else B = A
if[Set*] false then A else B = B

{- Define the actual if-then-else operator -}
if_then_else_ : ∀ {i j}{A : Set i}{B : Set j}(t : Bool) → A → B →
(if[Set*] t then A else B)
if true then x else y = x
if false then x else y = y


{- The test -}
f : (t : Bool) → if[Set*] t then Bool else ℕ
f t = if t then true else zero
--------------------------------

This seems to work fine. However, the version, where I use the "most
general" 
if_then_else_ in the type declaration, i.e.:

   f : (t : Bool) → if t then Bool else ℕ
   f t = if t then true else zero

would not go through, reporting that:

   if[Set*] t then Set else Set !=< Set (_53 t) of type
   Set (if[Level] t then lsu lze else lsu lze)
   when checking that the expression if t then Bool else ℕ has type
   Set (_53 t)

I do not understand the reason for this behaviour. Is it a bug of the
version I am using, 
or am I misunderstanding something here? After all, simply writing

g1 : Set
g1 = if[Set*] true then Bool else ℕ
g2 : Set
g2 = if true then Bool else ℕ

seems to work totally fine.


Thank you,
K.


PS: A couple of optional noob questions, once I'm at it:
* Is it possible to somehow verify that g1 == g2 in the last code snippet
above?
* Is there a possibility to do pattern-matching on type expressions in
Agda?
(e.g.
  f: (t = true) → ...
  f: (t = false) → ...)
 
CD: 3ms