Are there morphisms in Haskell?

I have some GADT which开发者_运维百科 represents a term in the lambda-calculus.

data Term a = 
      Var a
    | Lambda a (Term a)
    | Apply (Term a) (Term a)

What I want to do is to have a general interface for transformation on that type. It should have type signature similar to this:

(Term a -> Term a) -> Term a -> Term a

It's easy to write this function:

fmap' :: (Term a → Term a) → Term a → Term a 
fmap' f (Var v) = f (Var v)
fmap' f (Lambda v t) = Lambda v (fmap' f t)
fmap' f (Apply t1 t2) = Apply (fmap' f t1) (fmap' f t2)

So, my question is there some kind of general structure in haskell (or haskell library) to make this kind of transformations (similar to Functor, it should probably called morphism)?

---

For reference, here are the terms...

data Term a = 
      Var a
    | Lambda a (Term a)
    | Apply (Term a) (Term a)

(I note that the representation of variables is abstracted, which is often a good plan.)

...and here is the proposed function.

fmap' :: (Term a → Term a) → Term a → Term a 
fmap' f (Var v) = f (Var v)
fmap' f (Lambda v t) = Lambda v (fmap' f t)
fmap' f (Apply t1 t2) = Apply (fmap' f t1) (fmap' f t2)

What bothers me about this definition is that f is only ever applied to terms of form (Var v), so you might as well implement substitution.

subst :: (a → Term a) → Term a → Term a 
subst f (Var v) = f v
subst f (Lambda v t) = Lambda v (subst f t)
subst f (Apply t1 t2) = Apply (subst f t1) (subst f t2)

If you took slightly more care to distinguish bound from free variables, you'd be able to make Term a Monad with substitution implementing (>>=). In general, terms can have a Functor structure for renaming and a Monad structure for substitution. There's a lovely paper by Bird and Paterson about that, but I digress.

Meanwhile, if you do want to act other than at variables, one general approach is to use general purpose traversal toolkits like uniplate, as augustss suggests. Another possibility, perhaps slightly more disciplined, is to work with the ‘fold’ for your type.

tmFold :: (x -> y) -> (x -> y -> y) -> (y -> y -> y) -> Term x -> y
tmFold v l a (Var x)       = v x
tmFold v l a (Lambda x t)  = l x (tmFold v l a t)
tmFold v l a (Apply t t')  = a (tmFold v l a t) (tmFold v l a t')

Here, v, l and a define an alternative algebra for your Term-forming operations, only acting on y, rather than Term x, explaining how to handle variables, lambdas and applications. You might choose y to be m (Term x) for some suitable monad m (e.g., threading an environment for the variables), rather than just Term x itself. Each subterm is processed to give a y, then the appropriate function is chosen to produce the y for the whole term. The fold captures the standard recursion pattern.

Ordinary first-order datatypes (and some well-behaved higher-order datatypes) can all be equipped with fold-operators. At a cost to readability, you can even write the fold operator once and for all.

data Fix f = In (f (Fix f))

fixFold :: Functor f => (f y -> y) -> Fix f -> y
fixFold g (In xf) = g (fmap (fixFold g) xf)

data TermF a t
  = VarF a
  | LambdaF a t
  | ApplyF t t

type Term a = Fix (TermF a)

Unlike your recursive Term a, this TermF a t explains how to make one layer of a term, with t elements in the subterm places. We get back the recursive Term structure by using the recursive Fix type. We lose a little cosmetically, in that each layer has an extra In wrapping it. We can define

var x      = In (VarF x)
lambda x t = In (LambdaF x t)
apply t t' = In (Apply x t t')

but we can't use those definitions in pattern matching. The payoff, though, is that we can use the generic fixFold at no extra cost. To compute a y from a term, we need only give a function of type

TermF a y -> y

which (just like v, l, and a above) explains how to handle any term whose subterms have already been processed to values of type y. By being explicit in types about what one layer consists of, we can tap into the general pattern of working layer by layer.

---

Have a look at the uniplate package. It can do the kind of transformations you are talking about, but for an arbitrary data structure.

---

With the fmap' you quoted in the question, the transformation function f can only transform Var values to different lambda expressions. It cannot transform a Lambda or Apply into something else, since it's hardcoded in the fmap' function that these constructors stay the same.

Your fmap' can for example transform Var 1 into Lambda 1 (Var 1), but not the other way around. Is this really your intention?

If fmap' should allow arbitrary transformations, you end up with this:

fmap' :: (Term a → Term a) → Term a → Term a 
fmap' f t = f t

This is the same as $.

(If, on the other hand, fmap' should only be allowed to change the values in the expression, without changing its structure at all, you would be back at the usual fmap.)

---

Firstly, I don't have an answer to your actual question, though I do have some ideas that might be useful to you, not sure.

That seems to me to be less general than it might be, I'd expect you to use something like:

fmap' :: (Term a → Term a) → Term a → Term a 
fmap' f (Var v) = f $ Var v
fmap' f (Lambda v t) = f $ Lambda v (fmap' f t)
fmap' f (Apply t1 t2) = f $ Apply (fmap' f t1) (fmap' f t2)

which still allows you the same functionality, you just do pattern matching within f itself. I think this function can be used to things like evaluation of your lambda calculus (though, there's some state you need to bring around with you).

Something that might be more useful in the future for you might be:

fmapM :: Monad m => (Term a -> m (Term a)) -> Term a -> m (Term a)
fmapM f (Var v)         = f (Var v)
fmapM f (Lambda v t)    = do
    t' <-fmapM f t
    f (Lambda v t')
fmapM f (Apply t1 t2)   = do
    t1' <- fmapM f t1
    t2' <- fmapM f t2
    f (Apply t1' t2')

Which you can then use later with a State monad to keep track of bindings from lambdas. Also this function is the same as the one above when you use the Identity monad, you could write a simple function taking f :: (Term a -> Term a) and use fmap' f = fmapM (f.(return :: -> Identity a)).

Let me know if this is helpful :)

---

You may find the unbound package useful, especially the substs function.