<div dir="ltr"><div>On the other hand, f = id id id id id id id id id id id id id id id id id id id id id id id id also takes a lot of time (and memory) to typecheck in Agda.<br><br></div>Jesper<br></div><div class="gmail_extra"><br><div class="gmail_quote">On Tue, Jan 10, 2017 at 12:43 PM, Sergei Meshveliani <span dir="ltr"><<a href="mailto:mechvel@botik.ru" target="_blank">mechvel@botik.ru</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><span class="">On Tue, 2017-01-10 at 11:42 +0100, Nils Anders Danielsson wrote:<br>
> On 2017-01-08 20:20, Sergei Meshveliani wrote:<br>
> > He said that the only source of an unnatural type check cost with Coq<br>
> > can be not of the language/compiler/interpreter itself, but due to<br>
> > unlucky usage of proof _tactics_ in the user program.<br>
><br>
> Consider the following Coq code (which is based on an example in<br>
> "Implementing Typed Intermediate Languages" by Shao, League and<br>
> Monnier):<br>
><br>
>    Definition id {A : Set} (x : A) : A := x.<br>
><br>
>    Definition slow {A : Set} : A -> A :=<br>
>      id id id id id id id id id id id id id id id id id id.<br>
><br>
> The time required to check this code using Coq 8.4pl4 seems to be<br>
> roughly exponential in the number of occurrences of "id" on the last<br>
> line [*], and as far as I can tell the code does not use a single<br>
> tactic.<br>
><br>
> [*] With enough occurrences of "id" Coq complains about stack overflows,<br>
> so I guess that the code isn't actually checked.<br>
><br>
<br>
<br>
</span>Nice example. Thank you.<br>
I tried Agda-2.5.2 on<br>
 f :  {A : Set} → A → A<br>
 f =  id ∘ id ∘ id ∘ id ∘  id ∘ id ∘ id ∘ id ∘  id ∘ id ∘ id ∘ id ∘<br>
      id ∘ id ∘ id ∘ id ∘  id ∘ id ∘ id ∘ id ∘  id ∘ id ∘ id ∘ id<br>
<br>
It type-checks it in a moment.<br>
<br>
------<br>
Sergei<br>
<div class="HOEnZb"><div class="h5"><br>
______________________________<wbr>_________________<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" rel="noreferrer" target="_blank">https://lists.chalmers.se/<wbr>mailman/listinfo/agda</a><br>
</div></div></blockquote></div><br></div>