[TYPES] polymorphic isomorphisms

[Thorsten Altenkirch]

Hi Paul,

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

As far as standard models are concerned: as far as I know it isn't so  
easy to construct a
parametric model, this was done by Bainbridge et al and is called the  
"Parametric PER
model". The standard PER models are in general not parametric, i.e.  
there is a counterexample
by Ivar Rummelhof where he constructs a particular PCA so that the type
polynat = Pi X.X -> (X->X) -> X contains non-standard numerals. I'd  
think that in
this model also your isomorphisms should fail.

Cheers,
Thorsten


On 23 Jan 2008, at 19:09, Paul B Levy wrote:

> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/ 
> types-list ]
>
>
>
> Dear all,
>
> Do the following System F isomorphisms appear in the literature, and
> are they validated by the standard models?
>
> (1)
>
> Prod X. ((X -> B) -> A) cong A [ nu X. B / X ]
> where X is negative in A and positive in B
>
> (2)
>
> Prod X. ((B -> X) -> A) cong A [ mu X. B / X ]
> where X is positive in A and B
>
> Also, are any other isomorphisms (beyond the obvious beta-eta ones)  
> known?
> (By "isomorphism" I mean definable both ways by terms that are  
> inverse up
> to observational equivalence.)
>
> The following isomorphisms are similar, but they're already  
> derivable from
> (1)-(2).
>
> (3)
>
> Sum X. ((X -> B) x A) cong A [ nu X. B / X ]
> where X is positive in A and B
>
> (4)
>
> Sum X. ((B -> X) x A) cong A [ mu X. B / X ]
> where X is negative in A and positive in B
>
> regards,
> Paul
>
>
>
> -- 
> 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


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.