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

[Nicolas Frisby]

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