<div dir="ltr"><div><div><div>> But thm is useless, because the type for its first argument is empty.<br></div><a href="http://www.cse.chalmers.se/~nad/listings/lib-0.7/Data.Empty.html#326">⊥-elim</a> is looking at you questionably?</div>
<br></div></div><div class="gmail_extra"><br><br><div class="gmail_quote">2014-07-02 20:42 GMT+03:00 Sergei Meshveliani <span dir="ltr"><<a href="mailto:mechvel@botik.ru" target="_blank">mechvel@botik.ru</a>></span>:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">On Wed, 2014-07-02 at 18:00 +0200, Ulf Norell wrote:<br>
><br>
> [..]<br>
<div><div class="h5"><br>
<br>
> > For instance,<br>
> ><br>
> > False : ℕ → Set<br>
> > False _ = ⊥<br>
> ><br>
> > decFalse : Decidable False<br>
> > decFalse _ = no (λ x → x)<br>
> ><br>
> > loopy : ¬ (∀ n → ¬ False n) → Σ ℕ False<br>
> > loopy H = findNatByContra False decFalse H<br>
> ><br>
> ><br>
> > Here, loopy will happily evaluate forever with the<br>
> hypothetical<br>
> > (classical) proof that there is a number satisfying False.<br>
> There > is no need to evaluate under the case since decFalse<br>
> comes back > 'no' for any number.<br>
><br>
><br>
> Can you, please, explain further?<br>
><br>
> To apply (loopy H), one needs to provide<br>
> H : (∀ n → ¬ False n) → ⊥.<br>
><br>
> And this is not possible, because its type normalizes to<br>
><br>
> ((n : ℕ) → (False n → ⊥)) → ⊥, and to ((n : ℕ) → (⊥ → ⊥)) →<br>
> ⊥,<br>
><br>
> and the type (n : ℕ) → (⊥ → ⊥) has a value (\n → id) in<br>
> it.<br>
><br>
><br>
> As one cannot provide any argument value to `loopy', how can<br>
> it<br>
> evaluate forever?<br>
><br>
><br>
> The problem is that in Agda programs need to terminate not only at<br>
> run-time when you apply them to actual arguments, but also at type<br>
> checking-time when the type checker runs programs to check for<br>
> equality. For instance, suppose you define loopy as above and then try<br>
> to prove that loopy always returns 42<br>
><br>
><br>
> thm : (H : ¬ (∀ n → ¬ False n)) → proj₁ (loopy H) ≡ 42<br>
> thm _ = refl<br>
><br>
><br>
> In this case the type checker needs to evaluate loopy in the context<br>
> of the<br>
> free variable H to check if it normalises to 42. This evaluation will<br>
> not terminate<br>
> with your definition of findNatByContra.<br>
><br>
<br>
</div></div>But thm is useless, because the type for its first argument is empty.<br>
I hope, I can provide examples of practically usable programs which<br>
apply findNatByContra.<br>
<br>
1) But can `loopy' be introduced other than by a mistake?<br>
Is there an example of a practically usable program which also uses<br>
`loopy' ?<br>
<br>
2) Suppose one introduces `loopy' by a mistake, and sets its various<br>
invocations, also by a mistake. What can happen then, in the worst case?<br>
Probably, the type checker will loop forever, and the user will<br>
interrupt the process of checking (as I did 10 minutes ago!).<br>
This will not make the whole usage worse, because there are many other<br>
ways in Agda to make the checker loop forever.<br>
<br>
Am I missing something?<br>
<div class="HOEnZb"><div class="h5"><br>
Regards,<br>
<br>
------<br>
Sergei<br>
<br>
<br>
<br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</div></div></blockquote></div><br></div>