[Agda] Slow type-checking of records

[Carter Schonwald]

I'd like to remark that the language project I'm currently working on,
https://github.com/hopper-lang/hopper
,

A lot of the work that myself and colleagues are  currently doing for
hopper is towards supporting having a performant efficient shared substrate
for evaluation and normalization of dependently typed programs.

But once it's a little bit more mature, the hopper type theory and runtime
should be a viable substrate for normalizing open terms from Agda, because
we intend to support a lot of ideas that Agda has done a lovely job of
iterating on.

Point being, having efficient term normalization for type checking turns
into "what's a good shared runtime for evaluation and normalization" very
quickly, and that's still a design space that's not entirely satisfactorily
explored.

In coq their solution is to patch the ocaml byte code intepreter to support
open terms, which some iteration of landed in coq 8.5

I'm not quite sure how lean treats their runtime system / heap rep, but
there's possibly interesting lessons there.

That said, it does look like the new "treeless" rep in Agda master / 2.5
does pave the way to thinking about this stuff more.


Perhaps flipped around : what about adding tracing / profiling facilitaties
to tease apart bottle necks in code? My admittedly still fuzzy
understanding is that having fast type checking crucially intersects with
understanding the nature of reductions that are done during any
normalization (by evaluation ) strategy.

On Wednesday, March 16, 2016, Nils Anders Danielsson <nad at cse.gu.se> wrote:

> On 2016-03-12 00:33, Nils Anders Danielsson wrote:
>
>> I found another problem. I've created a ticket on the bug tracker:
>> https://github.com/agda/agda/issues/1901.
>>
>
> This problem has been fixed, and I can now type-check Andreas' old code
> on my machine. However, Agda is still slow.
>
> I tried replacing all lambdas in coreAdjunction with pattern-matching
> lambdas, and then Agda became roughly ten times faster and used roughly
> nine times less memory. This suggests to me that (part of) the problem
> is that Agda always reduces lambda applications (as opposed to
> applications of pattern-matching lambdas and defined functions), as
> pointed out by Andrea.
>
> What can we do about this? I don't want to force users to use
> workarounds like copattern matching. Could we for instance add support
> for beta-redexes to the internal syntax?
>
> --
> /NAD
> _______________________________________________
> 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/20160316/0280b944/attachment.html