[Agda] Associativity for free!

[Nils Anders Danielsson]

On 2011-10-26 23:01, James Chapman wrote:
> This may sound silly and perhaps you might somewhere else need append
> to associate to the right. Nisse told me that in a recent
> implementation of a dependently typed lambda calculus he defined both
> versions and didn't end up needing them both at the same time.

Contexts:

   data Ctxt : Set where
     ε   : Ctxt
     _▻_ : (Γ : Ctxt) (σ : Type Γ) → Ctxt

Cons-based context extensions:

   data Ctxt₊ (Γ : Ctxt) : Set where
     ε   : Ctxt₊ Γ
     _◅_ : (σ : Type Γ) (Γ₊ : Ctxt₊ (Γ ▻ σ)) → Ctxt₊ Γ

Snoc-based context extensions:

   data Ctxt⁺ (Γ : Ctxt) : Set where
     ε   : Ctxt⁺ Γ
     _▻_ : (Γ⁺ : Ctxt⁺ Γ) (σ : Type (Γ ++⁺ Γ⁺)) → Ctxt⁺ Γ

The cons-based extensions are convenient if you want to define something
like weakening for a Kripke model, because

   (Γ ▻ σ) ++₊ Γ₊

is by definition equal to

   Γ ++₊ (σ ◅ Γ₊).

On the other hand, the snoc-based extensions are convenient if you want
to go under many lambdas, because

   (Γ ++⁺ Γ⁺) ▻ σ

is by definition equal to

   Γ ++⁺ (Γ⁺ ▻ σ).

For more details (work in progress):

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

-- 
/NAD