[Haskell-cafe] Fixed point newtype confusion

[wren ng thornton]

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

-- 
Live well,
~wren