[TYPES] Fwd: polymorphic isomorphisms

[Thorsten Altenkirch]

Hi Paul,

On 24 Jan 2008, at 14:24, Thorsten Altenkirch wrote:
> we know that parametricity implies that
>
> mu X.B(X) ~ Pi X.(B(X) -> X) -> X
>
> where X is positive in B. Your question (2) seems to boil down to
>
> A(Pi X.(B(X) -> X) -> X) ~ Pi X.(B(X) -> X) -> A(X)
>
> which I think is also implied by parametricity (but I haven't checked
> it).

I have now, it does indeed follow. The candidate isomorphism

(phi,phi^-1) : A(mu X.B(X)) ~ Pi X.(B(X) -> X) -> A(X)

clearly is

phi a X f  = A (fold X f) a
phi^-1 f = f mu in

where mu X.B(X) = Pi X.(B(X) -> X) -> X ,
  fold : Pi X.(B(X) -> X) -> mu X.B(X) -> X
fold X f b =  b X f
in : B(mu X.B(X)) -> mu X.B(X)
in b X f = f (B(fold f) b)

To see that phi^-1 o phi = id we only need the functor laws for A and  
that fold (mu X.B(X)) in = id which is indeed a part of Wadler's  
proof that mu X.B(X) is initial. To show that phi o phi^-1 = id we  
need to employ parametricity: given g : Pi X.(B(X) -> X) -> A(X) then  
for any B-algebra f: A(C) -> C we have that f is related to in in the  
relational interpretation of A(X) -> X applied to the graph of fold  
f, which I denote as (fold f)^#. Hence, by parametricity of g we have  
that g X f and g (mu X. B(X)) in are related in the raelational  
interpretation of B(X) applied to (fold f)^#, which can be spells out  
as B (fold X f)(g (mu X.B(X) in) = g X f. This implies the desired  
result using eta

phi (phi^- g) = \ X f.B(fold f) (g mu X.B(X) in)
= \ X f .g X f
= g

Background can be found in Wadler's seminal paper "Theorem's for  
free" and his note "Recursive types for free!" available from http:// 
homepages.inf.ed.ac.uk/wadler/papers/free-rectypes/free-rectypes.txt  
(was this ever published?). I also summarized this in a recent post  
on our fp-lunch blog (http://sneezy.cs.nott.ac.uk/fplunch/weblog/?p=83).

Disclaimer: For those who know me better, I'd like to point out that  
I consider System F only as a formal game inspired by Type:Type,  
whose consistency (i.e. Pi X.X is empty) is irrelevant for the  
discussion above. :-)

Cheers,
Thorsten

P.S. Why are you actually interested in those isos?



This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.