[PRL] polyadic, unordered binders

[Dave Herman]

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