Hmm, I don't understand how that would work.
I wish I could define something like this:
class (Functor f) => Fixpoint f x | x -> f where
fix :: x -> Fix f
instance (Functor f) => Fixpoint f (forall a. f a) where
fix = id
instance (Functor f, Fixpoint f x) => Fixpoint f (f x) where
fix = Fix . fmap fix
but instances with polymorphic types aren't allowed. (Why is that?)
Alternatively if I could write a function that could turn
e :: forall a. F (F (F ... (F a) ... ))
into
specialize e :: F (F (F ... (F X) ... ))
that would work too, but I don't see how that's possible.
On Mon, May 7, 2012 at 6:59 PM, wren ng thornton <w...@freegeek.org> wrote:
> On 5/7/12 8:55 PM, Sebastien Zany wrote:
>
>> To slightly alter the question, is there a way to define a class
>>
>> class (Functor f) => Fixpoint f x where
>>> ...
>>>
>>
> You can just do that (with MPTCs enabled). Though the usability will be
> much better if you use fundeps or associated types in order to constrain
> the relation between fs and xs. E.g.:
>
> -- All the following require the laws:
> -- > fix . unfix == id
> -- > unfix . fix == id
>
> -- With MPTCs and fundeps:
> class (Functor f) => Fixpoint f x | f -> x where
> fix :: f x -> x
> unfix :: x -> f x
>
> class (Functor f) => Fixpoint f x | x -> f where
> fix :: f x -> x
> unfix :: x -> f x
>
> class (Functor f) => Fixpoint f x | f -> x, x -> f where
> fix :: f x -> x
> unfix :: x -> f x
>
> -- With associated types:
> -- (Add a type/data family if you want both Fix and Pre.)
> class (Functor f) => Fixpoint f where
> type Fix f :: *
> fix :: f (Fix f) -> Fix f
> unfix :: Fix f -> f (Fix f)
>
> class (Functor f) => Fixpoint f where
> data Fix f :: *
> fix :: f (Fix f) -> Fix f
> unfix :: Fix f -> f (Fix f)
>
> class (Functor (Pre x)) => Fixpoint x where
> type Pre x :: * -> *
> fix :: Pre x x -> x
> unfix :: x -> Pre x x
>
> class (Functor (Pre x)) => Fixpoint x where
> data Pre x :: * -> *
> fix :: Pre x x -> x
> unfix :: x -> Pre x x
>
> Indeed, that last one is already provided in the fixpoint[1] package,
> though the names are slightly different. The differences between using "x
> -> f", "f -> x", or both, and between using "data" or "type", are how it
> affects inference. That is, implicitly there are two relations on types:
>
> Fix \subseteq * \cross *
> Pre \subseteq * \cross *
>
> And we need to know: (1) are these relations functional or not? And, (2)
> are they injective or not? The answers to those questions will affect how
> you can infer one of the types (f or x) given the other (x or f).
>
>
> [1]
> http://hackage.haskell.org/**package/fixpoint<http://hackage.haskell.org/package/fixpoint>
>
>
> --
> Live well,
> ~wren
>
> ______________________________**_________________
> Haskell-Cafe mailing list
> Haskell-Cafe@haskell.org
> http://www.haskell.org/**mailman/listinfo/haskell-cafe<http://www.haskell.org/mailman/listinfo/haskell-cafe>
>
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
