Do morphisms exist in Haskell?

I have some GADT which is a member in 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 common interface for converting this type. It should have a type signature like this:

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

It is 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, does the haskell (or haskell library) have some kind of common structure to make such transformations (similar to Functor, probably, this should be called morphism)?

+5
source share
5 answers

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 out, 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)

, , f (Var v), .

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)

, , Term a Monad (>>=). , Functor Monad . Bird and Paterson , .

, , , - , uniplate, . , , , - & rsquo; .

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

v, l a Term - , y, Term x, , , . y m (Term x) m (, ), Term x. , y, y . .

( ) fold-operator. , , .

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)

Term a, TermF a t , t . Term, Fix. , In, .

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

. , fixFold - . a y ,

TermF a y -> y

( v, l a ) , , y. , , .

+12

. , , .

+7

fmap', , f Var -. Lambda Apply - , fmap', .

fmap' , , Var 1 Lambda 1 (Var 1), . ?

fmap' , :

fmap' :: (Term a β†’ Term a) β†’ Term a β†’ Term a 
fmap' f t = f t

, $.

(, , fmap' , fmap.)

+4

-, , , , .

, , , , - :

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)

- , f. , , - ( - , ).

-, , :

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 the state monad to track lambda bindings. Also this function is the same as above, when you use the Identity monad, you can write a simple function by taking f :: (Term a β†’ Term a) and use fmap 'f = fmapM (f. (Return :: β†’ Authentication a )).

Let me know if this is helpful :)

+2
source

You can find a useful unbound package, especially substations .

+1
source

All Articles