[PRL] polyadic, unordered binders

[Matthias Felleisen]

You could ask the question about Typed Scheme's type system and no,  
it doesn't work:

#lang typed-scheme

(: f (∀ (α β) (α β -> β)))
(define (f x y) y)

(: g (∀ (β α) (α β -> β)))
(define (g x y) y)

(: h ((∀ (α β) (α β -> β)) -> Number))
(define (h i) (i 4 2))

And you could ask whether it makes sense to do this. -- Matthias



On Oct 14, 2008, at 3:12 PM, Dave Herman wrote:

> FWIW, Ryan pointed out a similar situation where you could end up with
> unordered binders: subtyping in a language with higher-rank
> polymorphism. You would like these two types to be the same:
>
>      forall a. forall b. a -> b -> b
>      forall b. forall a. a -> b -> b
>
> GHC support higher-rank polymorphism; I wonder how they implement the
> subtyping check for its polymorphic types.
>
> Dave
>
> Dave Herman wrote:
>> Imagine a language with a polyadic binding construct where you could
>> permute the bindings without changing its meaning. Say, a parallel- 
>> let form:
>>
>>      (let/par ((x1 e1) ... (xn en)) e)
>>
>> Then it seems the alpha-equivalence relation would hold up to  
>> permuting
>> bindings:
>>
>>      pi * (x_i ...) = (x_j ...)                   (z_j ...) fresh
>>                         forall j . e_j == e'_j
>>                 e[z_j/x_j, ...] == e'[z_j/y_j, ...]
>>      ------------------------------------------------------------
>>      (let/par ((x_i e_i) ...) e) == (let/par ((y_j e'_j) ...) e')
>>
>> This should be read as existentially positing a permutation `pi'  
>> of the
>> bindings on the left-hand side to unify with the bindings of the
>> right-hand side. It's simple enough to specify, although it's a royal
>> pain to implement efficiently, i.e. to avoid comparing n!  
>> permutations
>> of bindings.
>>
>> This seems natural but I've never seen it before, since polyadic  
>> binders
>> are usually order-sensitive. Does anyone know of a precedent for this
>> kind of thing?
>>
>> Thanks,
>> Dave
>>
>> _______________________________________________
>> PRL mailing list
>> PRL at lists.ccs.neu.edu
>> https://lists.ccs.neu.edu/bin/listinfo/prl
>
>
> _______________________________________________
> PRL mailing list
> PRL at lists.ccs.neu.edu
> https://lists.ccs.neu.edu/bin/listinfo/prl