[Agda] Question regarding a simple "dependently typed IF-THEN-ELSE"

[Andreas Abel]

Just a quick comment:  In intensional type theory, e.g. Agda,

   if t then a else a

is not definitionally equal to

   a

hence, the error.

On 10.03.2014 16:54, Konstantin Tretjakov wrote:
> 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) → ...)
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Depeartment of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/