[Agda] Associativity for free!

[James Chapman]

Thanks for the references Randy.

I also forgot to say before…

Alan: neat trick!

Best,

James


On Oct 27, 2011, at 12:34 AM, Randy Pollack wrote:

>> 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
>> 
>>