<div dir="ltr">For f : (t : Bool) -> X to be well-typed you need X : Set i, for some i.<div>if[Set*] t then Bool else N : Set (if[Level] t then zero else zero), so that's fine.</div><div>On the other hand, if t then Bool else N has type if[Set*] t then Set else Set,</div>
<div>which does not have the form Set i for some i.</div><div><br></div><div>It is however the case that (if true then a else b) equals a, by simple reduction</div><div>of the definition of if_then_else.</div><div><br></div>
<div>/ Ulf</div></div><div class="gmail_extra"><br><br><div class="gmail_quote">On Tue, Mar 11, 2014 at 12:02 AM, Konstantin Tretjakov <span dir="ltr"><<a href="mailto:kt@ut.ee" target="_blank">kt@ut.ee</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div class=""><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
Just a quick comment: In intensional type theory, e.g. Agda,<br>
<br>
if t then a else a<br>
<br>
is not definitionally equal to<br>
<br>
a<br>
</blockquote>
<br></div>
I guess this means I cannot assert equality between [if true then a else b] and a, right?<br>
OK, but my main question is still different. Namely, why is it possible to define<div class=""><br>
<br>
f : (t : Bool) → if[Set*] t then Bool else ℕ<br>
<br></div>
but not<div class=""><br>
<br>
f : (t : Bool) → if t then Bool else ℕ<br>
<br></div>
where the only difference between if and if[Set*] is that the former is defined for<br>
<br>
(Bool, A: Set i, B: Set j)<br>
<br>
and the latter - for<br>
<br>
(Bool, Set i, Set j)<span class="HOEnZb"><font color="#888888"><br>
<br>
K.</font></span><div class="HOEnZb"><div class="h5"><br>
<br>
<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<br>
hence, the error.<br>
<br>
On 10.03.2014 16:54, Konstantin Tretjakov wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
Hello,<br>
<br>
suppose I would like to be able to use if-then-else in something like<br>
the following:<br>
<br>
f t = if t then true else zero<br>
<br>
My current attempt at doing it (Agda 2.3.0.1, Windows) is this:<br>
<br>
------------------------------<u></u>--<br>
module Test1 where<br>
<br>
postulate<br>
Level : Set<br>
lze : Level<br>
lsu : Level -> Level<br>
lmax : Level -> Level -> Level<br>
<br>
{-# BUILTIN LEVEL Level #-}<br>
{-# BUILTIN LEVELZERO lze #-}<br>
{-# BUILTIN LEVELSUC lsu #-}<br>
{-# BUILTIN LEVELMAX lmax #-}<br>
<br>
<br>
data Bool : Set where<br>
true false : Bool<br>
<br>
data ℕ : Set where<br>
zero : ℕ<br>
suc : ℕ → ℕ<br>
<br>
{- Set level of the return type of the if-then-else operator -}<br>
if[Level]_then_else_ : Bool → Level → Level → Level<br>
if[Level] true then x else y = x<br>
if[Level] false then x else y = y<br>
<br>
{- Return type of the if-then-else operator -}<br>
if[Set*]_then_else_ : ∀ {i j} (t : Bool) → Set i → Set j → Set<br>
(if[Level] t then i else j)<br>
if[Set*] true then A else B = A<br>
if[Set*] false then A else B = B<br>
<br>
{- Define the actual if-then-else operator -}<br>
if_then_else_ : ∀ {i j}{A : Set i}{B : Set j}(t : Bool) → A → B →<br>
(if[Set*] t then A else B)<br>
if true then x else y = x<br>
if false then x else y = y<br>
<br>
<br>
{- The test -}<br>
f : (t : Bool) → if[Set*] t then Bool else ℕ<br>
f t = if t then true else zero<br>
------------------------------<u></u>--<br>
<br>
This seems to work fine. However, the version, where I use the "most<br>
general" if_then_else_ in the type declaration, i.e.:<br>
<br>
f : (t : Bool) → if t then Bool else ℕ<br>
f t = if t then true else zero<br>
<br>
would not go through, reporting that:<br>
<br>
if[Set*] t then Set else Set !=< Set (_53 t) of type<br>
Set (if[Level] t then lsu lze else lsu lze)<br>
when checking that the expression if t then Bool else ℕ has type<br>
Set (_53 t)<br>
<br>
I do not understand the reason for this behaviour. Is it a bug of the<br>
version I am using, or am I misunderstanding something here? After all,<br>
simply writing<br>
<br>
g1 : Set<br>
g1 = if[Set*] true then Bool else ℕ<br>
g2 : Set<br>
g2 = if true then Bool else ℕ<br>
<br>
seems to work totally fine.<br>
<br>
<br>
Thank you,<br>
K.<br>
<br>
<br>
PS: A couple of optional noob questions, once I'm at it:<br>
* Is it possible to somehow verify that g1 == g2 in the last code<br>
snippet above?<br>
* Is there a possibility to do pattern-matching on type expressions in<br>
Agda?<br>
(e.g.<br>
f: (t = true) → ...<br>
f: (t = false) → ...)<br>
______________________________<u></u>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/<u></u>mailman/listinfo/agda</a><br>
<br>
</blockquote>
<br>
<br>
</blockquote>
______________________________<u></u>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/<u></u>mailman/listinfo/agda</a><br>
</div></div></blockquote></div><br></div>