[Agda] Re: Associativity for free!

[Nils Anders Danielsson]

On 2011-11-04 18:55, Alan Jeffrey wrote:
> This came up in the context of normalization by evaluation, which needs
> a Kripke-like structure which extends the context on every function
> application. Associators were really getting in the way, as I was
> needing to prove a bunch of coherence properties. Have you tried getting
> an NBE proof to go through in your setting?

I don't know about James' setting, but I've implemented something close
to NBE [*] in a well-typed way for a dependently typed object language,
and didn't have any problems with associativity (once I found the right
definitions):

    http://www.cse.chalmers.se/~nad/listings/dependently-typed-syntax/README.html

The key trick to avoid problems with associativity was to use cons-based
context extensions.

[*] I didn't prove uniqueness of normal forms, but rather its negation
(almost).

-- 
/NAD