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

[Ulf Norell]

For f : (t : Bool) -> X to be well-typed you need X : Set i, for some i.
if[Set*] t then Bool else N : Set (if[Level] t then zero else zero), so
that's fine.
On the other hand, if t then Bool else N has type if[Set*] t then Set else
Set,
which does not have the form Set i for some i.

It is however the case that (if true then a else b) equals a, by simple
reduction
of the definition of if_then_else.

/ Ulf


On Tue, Mar 11, 2014 at 12:02 AM, Konstantin Tretjakov <kt at ut.ee> wrote:

> 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
>>>
>>>
>>
>>  _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20140311/3db6fb5a/attachment-0001.html