To slightly alter the question, is there a way to define a class

class (Functor f) => Fixpoint f x where ...

so that I can define something with a type signature that looks like

something :: (Fixpoint f x) => ... x ...

which will accept any

argument :: F (F (F ... (F a) ... ))

in place of x? Or alternatively could something analogous be done with type families? Thanks, Sebastien On Mon, May 7, 2012 at 5:45 PM, Sebastien Zany < sebastien@chaoticresearch.com> wrote:

Thanks Wren!

When I try

...

fix term ghci complains of an ambiguous type variable.

I have to specify

...

term :: (Expr (Expr (Expr (Fix Expr)))) for it to work.

Is there a way around this?

On Sun, May 6, 2012 at 4:04 PM, wren ng thornton wrote:

...

On 5/6/12 8:59 AM, Sebastien Zany wrote:

...

Hi,

Suppose I have the following types:

data Expr expr = Lit Nat | Add (expr, expr)

...

newtype Fix f = Fix {unFix :: f (Fix f)}

I can construct a sample term:

term :: Expr (Expr (Expr expr))

...

term = Add (Lit 1, Add (Lit 2, Lit 3))

But isn't quite what I need. What I really need is:

term' :: Fix Expr

...

term' = Fix . Add $ (Fix . Lit $ 1, Fix . Add $ (Fix . Lit $ 2, Fix . Lit

$ 3))

I feel like there's a stupidly simple way to automatically produce term' from term, but I'm not seeing it.

There's the smart constructors approach to building term' in the first place, but if someone else is giving you the term and you need to convert it, then you'll need to use a catamorphism (or similar).

That is, we already have:

Fix :: Expr (Fix Expr) -> Fix Expr

but we need to plumb this down through multiple layers:

fmap Fix :: Expr (Expr (Fix Expr)) -> Expr (Fix Expr)

fmap (fmap Fix) :: Expr (Expr (Expr (Fix Expr))) -> Expr (Expr (Fix Expr))

...

If you don't know how many times the incoming term has been unFixed, then you'll need a type class to abstract over the n in fmap^n Fix. How exactly you want to do that will depend on the application, how general it should be, etc. The problem, of course, is that we don't have functor composition for free in Haskell. Francesco's suggestion is probably the easiest:

instance Functor Expr where fmap _ (Lit i) = Lit i fmap f (Add e1 e2) = Add (f e1) (f e2)

class FixExpr e where fix :: e -> Fix Expr

instance FixExpr (Fix Expr) where fix = id

instance FixExpr e => FixExpr (Expr e) where fix = Fix . fmap fix

Note that the general form of catamorphisms is:

cata :: Functor f => (f a -> a) -> Fix f -> a cata f = f . fmap (cata f) . unFix

so we're just defining fix = cata Fix, but using induction on the type term itself (via type classes) rather than doing induction on the value term like we usually would.

-- Live well, ~wren

______________________________**_________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/**mailman/listinfo/haskell-cafehttp://www.haskell.org/mailman/listinfo/haskell-cafe

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 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/fixpointhttp://hackage.haskell.org/package/fixpoint

-- Live well, ~wren

______________________________**_________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/**mailman/listinfo/haskell-cafehttp://www.haskell.org/mailman/listinfo/haskell-cafe

On 5/8/12 8:24 PM, Sebastien Zany wrote:

Hmm, I don't understand how that would work.

Using one of the fundep versions: class (Functor f) => Fixpoint f x | ... where fix :: f x -> x unfix :: x -> f x We'd define instances like the following: data List a = Nil | Cons a (List a) data PreList a b = PNil | PCons a b deriving Functor instance Fixpoint (PreList a) (List a) where -- fix :: PreList a (List a) -> List a fix PNil = Nil fix (PCons x xs) = Cons x xs -- unfix :: List a -> PreList a (List a) unfix Nil = PNil unfix (Cons x xs) = PCons x xs Or we could do: newtype Fix f = Fix { unFix :: f (Fix f) } instance Fixpoint (PreList a) (Fix (PreList a)) where -- fix :: PreList a (Fix (PreList a)) -> Fix (PreList a) fix = Fix -- unfix :: Fix (PreList a) -> PreList a (Fix (PreList a)) unfix = unFix

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?)

Well, one problem is that (forall a. f a) is not a fixed-point of f. That is, f (forall a. f a) is not isomorphic to (forall a. f a) Another problem is that (forall a. f a) isn't exactly of kind *. It sort of is, but since it's quantifying over * you get into (im)predicativity issues. For example, do we allow the following type? Maybe (forall a. f a) Depending on what language extensions you have on and which version of GHC you're using, the answer could be yes or it could be no. There isn't a "right answer" per se, it just depends on what you want the semantics of the type system to be and what other features you want to have. Another problem is, I don't think that means what you think it means. Supposing we were to allow it, the expanded type of the first instance of fix would be: fix :: (forall a. f a) -> Fix f Which is isomorphic to fix :: exists a. f a -> Fix f Which means that supposing we have some (f A) where A is some unknown but defined type, then we can turn it into Fix f. The only way that could be possible is if we throw away all the As that occur in the (f A). But that's not what you mean, nor what you want.

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.

Yeah, that'd be nice. In System F, or in Haskell Core, the "forall a. b" is treated like a special version of the function arrow. So we have a big lambda for type abstraction (written "/\" below), and we have type application (written in Core with "@"). Thus we know that e is eta equivalent to: (/\a. e @a) :: forall a. F (F (F ... (F a) ... )) This is just like saying that given any function f :: A -> B, it is eta equivalent to (\(x::A). f x) :: A -> B. So if we wanted a version of e monomorphized on a = X, then we'd just say: e @X :: forall a. F (F (F ... (F X) ... )) There are tricks for gaining access to the type abstraction and type application of Core, but they're all fairly fragile as I recall. -- Live well, ~wren