[Haskell-cafe] OT: Isorecursive types and type abstraction
nicolas.frisby at gmail.com
Thu Jan 24 14:43:00 EST 2008
This paper, with a pdf available at Patricia Johann's publications page
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 <devriese at cs.tcd.ie> wrote:
> 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.
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
More information about the Haskell-Cafe