[Agda] type check performance

[Jesper Cockx]

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.

Jesper

On Tue, Jan 10, 2017 at 12:43 PM, Sergei Meshveliani <mechvel at botik.ru>
wrote:

> On Tue, 2017-01-10 at 11:42 +0100, Nils Anders Danielsson wrote:
> > On 2017-01-08 20:20, Sergei Meshveliani wrote:
> > > He said that the only source of an unnatural type check cost with Coq
> > > can be not of the language/compiler/interpreter itself, but due to
> > > unlucky usage of proof _tactics_ in the user program.
> >
> > Consider the following Coq code (which is based on an example in
> > "Implementing Typed Intermediate Languages" by Shao, League and
> > Monnier):
> >
> >    Definition id {A : Set} (x : A) : A := x.
> >
> >    Definition slow {A : Set} : A -> A :=
> >      id id id id id id id id id id id id id id id id id id.
> >
> > The time required to check this code using Coq 8.4pl4 seems to be
> > roughly exponential in the number of occurrences of "id" on the last
> > line [*], and as far as I can tell the code does not use a single
> > tactic.
> >
> > [*] With enough occurrences of "id" Coq complains about stack overflows,
> > so I guess that the code isn't actually checked.
> >
>
>
> Nice example. Thank you.
> I tried Agda-2.5.2 on
>  f :  {A : Set} → A → A
>  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
>
> It type-checks it in a moment.
>
> ------
> Sergei
>
> _______________________________________________
> 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/20170110/a5735ff5/attachment.html>