[TYPES] Fwd: polymorphic isomorphisms

[Paul B Levy]

Thanks Thorsten.

Masahito Hasegawa pointed out to me that all the isomorphisms I mentioned 
are provable in Plotkin-Abadi logic and System R.

Paul

PS System F is consistent :-)



On Mon, 28 Jan 2008, Thorsten Altenkirch wrote:

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

-- 
Paul Blain Levy              email: pbl at cs.bham.ac.uk
School of Computer Science, University of Birmingham
Birmingham B15 2TT, U.K.      tel: +44 121-414-4792
http://www.cs.bham.ac.uk/~pbl