Er, sorry – "fix = id" should be "fix = Fix". On Tue, May 8, 2012 at 5:24 PM, Sebastien Zany < sebast...@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 <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
