[Agda] type check cost for `open'

[Andrea Vezzosi]

On Tue, Aug 18, 2015 at 10:57 PM, Peter Selinger
<selinger at mathstat.dal.ca> wrote:
>
> My question remains: what would be involved in equipping Agda with an
> efficient evaluation strategy? Could a proficient Haskell programmer
> do it by modifying some well-defined set of modules, or would it
> require a more pervasive set of changes to the internals of Agda?

There are specific reduction modules, however expressing local
bindings is kinda impossible in the internal syntax, both function
definitions and metas are in a closed context.
The closest thing is what we have in master with --sharing, which uses
actual IORef's, have you tried if your example works linearly there?

By the way, "let" doesn't make it to the internal syntax, it gets
substituted away. Also definitions in where clauses get lambda-lifted
to the toplevel. That's already destroying a lot of opportunities for
sharing even if you switch to call-by-need, unless you have a
common-expression-elimination pass. This is what Philipp was referring
to I think.

Call-by-need would be great, but there are also other problems, where
the best strategy is not to reduce:

https://github.com/agda/agda/issues/1625




Best,
Andrea



> -- Peter
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda