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

[Konstantin Tretjakov]

> Just a quick comment:  In intensional type theory, e.g. Agda,
>
>    if t then a else a
>
> is not definitionally equal to
>
>    a

I guess this means I cannot assert equality between [if true then a else b] and a, right?
OK, but my main question is still different. Namely, why is it possible to define

   f : (t : Bool) → if[Set*] t then Bool else ℕ

but not

   f : (t : Bool) → if t then Bool else ℕ

where the only difference between if and if[Set*] is that the former is defined for

   (Bool, A: Set i, B: Set j)

and the latter - for

   (Bool, Set i, Set j)

K.


>
> 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
>>
>
>