[Agda] Associativity for free!

[Randy Pollack]

> 2. [...] Another solution I learnt from Conor [...]
>
> data _≤_ {X : Set} : List X → List X → Set where
>  done : [] ≤ []
>  keep : ∀{x}{xs xs'} → xs ≤ xs' → (x :: xs) ≤ (x :: xs')
>  skip : ∀{x}{xs xs'} → xs ≤ xs' → xs ≤ (x :: xs')

I think you will find this approach for weakening (of PTS typing) used
already in Geuvers and Nederhof, JAR 1991 (widely circulated by 1989).
 Following Geuvers and Nederhof, this approach is used in many papers
that mentions weakening of a type system or a logic since that time
(e.g. McKinna/Pollack, Pitts, Urban, ...).

Best,
Randy
---
On Wed, Oct 26, 2011 at 5:01 PM, James Chapman <james at cs.ioc.ee> wrote:
> Hi Alan,
>
> I too have encountered this problem, rather than tackling it head on here are two ways of tiptoeing around it.
>
> 1. A trivial solution for your example is simply to make _++_ associate to the left:
>
> data List (X : Set) : Set where
>  []   : List X
>  _::_ : X → List X → List X
>
> _++_ : ∀{X} → List X → List X → List X
> []        ++ xs' = xs'
> (x :: xs) ++ xs' = x :: (xs ++ xs')
>
> infixl 5 _++_
>
> postulate P : ∀{X} → List X → Set
>
> postulate weakening : ∀ {A} (as bs cs : List A) →
>                      P (as ++ cs) → P (as ++ bs ++ cs)
>
> weaken2 : ∀ {A} (as bs cs ds : List A) →
>   P (as ++ bs ++ ds) → P (as ++ bs ++ cs ++ ds)
> weaken2 as bs cs ds p = weakening (as ++ bs) cs ds p
>
> 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. Do you need both at the same time?
>
> 2. I guess you run into the this problem where ++ is an operation on contexts right? Another solution I learnt from Conor (exercise 15, his AFP notes http://www.strictlypositive.org/epigram-notes.ps.gz) is simply to avoid it. Instead of giving weakening this type, give a first order presentation of weakenings (functions from a context to the same context with more stuff chucked in arbitrary places). For  lists this function space would be the following inductively defined sublist relation:
>
> data _≤_ {X : Set} : List X → List X → Set where
>  done : [] ≤ []
>  keep : ∀{x}{xs xs'} → xs ≤ xs' → (x :: xs) ≤ (x :: xs')
>  skip : ∀{x}{xs xs'} → xs ≤ xs' → xs ≤ (x :: xs')
>
> Then, weakening would be something like:
>
> weakening : ∀{X}{xs xs' : List X} → P xs → xs ≤ xs' → P xs'
>
> By doing this ++ never appears in the types, so we don't have to use subst. I used this technique (called order preserving embeddings) in chapter 4 of my thesis (http://www.cs.ioc.ee/~james/papers/thesis.pdf ) and it was much more pleasant than using ++ as we did in our Big-step normalization paper (http://www.cs.ioc.ee/~james/papers/tait2.pdf) on which this chapter was based.
>
> Best wishes,
>
> James
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
>