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

[Antoine Latter]

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?

-Antoine

On Jan 24, 2008 10:31 AM, Edsko de Vries <devriese at cs.tcd.ie> wrote:
> On Thu, Jan 24, 2008 at 10:06:04AM -0600, Antoine Latter wrote:
> > Can "Fix" be made to work with higher-kinded types?  If so, would the
> > following work:
> >
> > Perfect = /\ A . Fix (L :: * -> *) . (A + L (A,A))
>
> Hi,
>
> Thanks for your quick reply. Unfortunately, your solution does not work. For
>
>   Fix X. t
>
> to be well-defined, we must have that if 'X' has kind 'k', then 't' must
> also have kind 'k' (compare the type of 'fix' in Haskell: (a -> a) -> a).
>
> > Keep in mind I have no idea what the "Perfect" data structure is
> > supposed to look like.
>
> The Haskell equivalent would be
>
> data Perfect a = Leaf a | Branch (Perfect (a, a))
>
> and models perfect binary trees (I admit, slightly headwrecking datatype! :)
>
> Edsko
>