This paper, with a pdf available at Patricia Johann's publications page
http://crab.rutgers.edu/~pjohann/
seems to be related.
Initial Algebra Semantics is Enough! Patricia Johann and Neil Ghani.
Proceedings, Typed Lambda Calculus and Applications 2007 (TLCA'07)
Hope that helps.
On Jan 24, 2008 11:02 AM, 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 _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe