[Agda] type check cost for `open'

[Peter Selinger]

Thanks, that was the sort of answer I was looking for!

I will give --sharing a try and report back!

I imagine it may be necessary to extend the internal syntax with local
let bindings to get sharing to work properly. For the purpose of
checking equality (of normal forms), these bindings would have to be
translated away, I guess.

-- Peter

Andrea Vezzosi wrote:
> 
> 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
>