[Agda] type check performance

[Sergei Meshveliani]

On Tue, 2017-01-10 at 13:35 +0100, Jesper Cockx wrote:
> 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.
> 

Indeed.
I am sorry, I have missed the fact that  (id id)  also has the needed
type there in RHS, as well as 
(id ∘ id).

------
Sergei


> 
> 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
>         
> 
>