[Haskell-cafe] Fixed point newtype confusion

[Sebastien Zany]

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 <wren at 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 at haskell.org
> http://www.haskell.org/**mailman/listinfo/haskell-cafe<http://www.haskell.org/mailman/listinfo/haskell-cafe>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20120508/2cfff26c/attachment.htm>