[Agda] Re: Associativity for free!

[Alan Jeffrey]

Yes, it may be that if I'd found the right collection of cons- vs- 
snoc-lists I'd have been able to get NBE to go through without 
associators. At this point, using difference lists around allows me to 
be sloppy about associativity, and have it all magically go through.

So far the main annoyances with difference lists I've found are:

a) Huge normal forms for terms, which tend to bog Agda down, especially 
in proofs with lots of holes.

b) A side-effect of (a) is that error messages or anything else which 
prints a normal form aren't much use, which makes proving properties a 
bit error-prone.

c) There are some unifications on difference lists that Agda fails to 
make, the most annoying of which is unifying (a ∷ as) with (b ∷ bs) 
doesn't unify a with b or as with bs, which is something weird to do 
with unification happening under lambdas.

You pays your money and you takes your choice.

A.

On 11/04/2011 01:15 PM, Nils Anders Danielsson wrote:
> 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).
>