[Haskell-cafe] OT: Isorecursive types and type abstraction

[Edsko de Vries]

On Thu, Jan 24, 2008 at 10:46:36AM -0600, Antoine Latter wrote:
> Hmm ...
> 
> How about:
> 
> Perfect :: * -> * = Fix (L :: * -> *) . /\ A . (A + L (A,A))
> 
> unfold Perfect = [L := Fix L . t] t where t = /\ A . (A + L (A,A))
>  = /\ A . (A + (Fix L . /\ B . (B + L (B,B))) (A,A))
> 
> assuming alpha-equality.  Because L and (Fix L . t)  are of kind (* ->
> *), the substitution should be okay.  Am I missing something, again?

The problem is not that Perfect as it stands cannot be unrolled; the
problem is that without some hackery, I don't know how to unroll the
type of a term if that type is of the form ((Fix ..) applied to some
arguments rather than just (Fix ..) -- whether that is List or Perfect.
The only reason I mention Perfect is that for List I can 'lift' the
"/\A" over the "Fix", but I cannot do that with Perfect.

Edsko