[Haskell-cafe] Fixed point newtype confusion

[Sebastien Zany]

Er, sorry – "fix = id" should be "fix = Fix".

On Tue, May 8, 2012 at 5:24 PM, Sebastien Zany <
sebastien at chaoticresearch.com> wrote:

> 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/7c6882ac/attachment.htm>