[Haskell-cafe] OT: Isorecursive types and type abstraction
Edsko de Vries
devriese at cs.tcd.ie
Thu Jan 24 12:02:46 EST 2008
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.
More information about the Haskell-Cafe