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 _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe