Are parameterized lambda terms a Monad?

Question

I have this representation of terms in the lambda calculus parameterized over the type of the name:

{-# LANGUAGE DeriveFunctor #-}

data Lambda a = Var a | App (Lambda a) (Lambda a) | Lam a (Lambda a) 
    deriving Functor

I was wondering if Lambda can be made an instance of monad? I thought that something like the following might work for the implementation of join:

joinT :: Lambda (Lambda a) -> Lambda a
joinT (Var a) = a
joinT (fun `App` arg) = joinT fun `App` joinT arg
joinT (Lam n body) = ?

For the third case I have absolutely no clue ... but it should be possible - this nameless representation of lambda-terms, taken from De Bruijn Notation as a Nested Datatype, is an instance of Monad (Maybe is used to discriminate between bound and free variables in this representation):

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE DeriveFunctor #-}

data Expr a 
    = V a
    | A (Expr a) (Expr a)
    | L (Expr (Maybe a))
    deriving (Show, Eq, Functor)

gfoldT :: forall m n b.
    (forall a. m a -> n a) ->
    (forall a. n a -> n a -> n a) ->
    (forall a. n (Maybe a) -> n a) ->
    (forall a. (Maybe (m a)) ->  m (Maybe a)) ->
    Expr (m b) -> n b
gfoldT v _ _ _ (V x) = v x
gfoldT v a l t (fun `A` arg) = a (gfoldT v a l t fun) (gfoldT v a l t arg)
gfoldT v a l t (L body) = l (gfoldT v a l t (fmap t body))

joinT :: Expr (Expr a) -> Expr a
joinT = gfoldT id (:@) Lam distT

distT :: Maybe (Expr a) -> Expr (Maybe a)
distT Nothing = Var Nothing
distT (Just x) = fmap Just x

joinT is sufficient for instance Monad Expr:

instance Applicative Expr where
    pure = Var
    ef <*> ea = do
        f <- ef
        a <- ea
        return $ f a

instance Monad Expr where
    return = Var
    t >>= f = (joinT . fmap f) t

Assume further the following two transformation functions between the representations:
unname :: Lamba a -> Expr a and name :: Expr a -> Lambda a. With those we can implement join for Lambda by exploiting the isomorphism between the two type constructors:

joinL :: Lambda (Lambda a) -> Lambda a
joinL = name . joinT . uname . fmap uname

But this seems very complicated. Is there a more straightforward way, or am I missing something important?

Edit: Here are the functions name and uname that I thought would do the job. As was pointed out in the comments and the answer, a really needs an Eq constraint which breaks the isomorphism.

foldT :: forall n b.
    (forall a. a -> n a) ->
    (forall a. n a -> n a -> n a) ->
    (forall a. n (Maybe a) -> n a) ->
    Expr b -> n b
foldT v _ _ (V x) = v x
foldT v a l (A fun arg) = a (foldT v a l fun) (foldT v a l arg)
foldT v a l (L body) = l (foldT v a l body)

abstract :: Eq a => a -> Expr a -> Expr a
abstract x = L . fmap (match x)

match :: Eq a => a -> a -> Maybe a
match x y = if x == y then Nothing else Just y

apply :: Expr a -> Expr (Maybe a) -> Expr a
apply t = joinT . fmap (subst t . fmap V)

uname :: Eq a => Lambda a -> Expr a
uname = foldL V A abstract

name :: Eq a => Expr a -> Lambda a
name e = nm [] e where
    nm vars (V n) = Var n
    nm vars (A fun arg) = nm vars fun `App` nm vars arg
    nm vars (L body) =
        Lam fresh $ nm (fresh:vars) (apply (V fresh) body) where
        fresh = head (names \ vars)

names :: [String]
names = [ [i] | i <- ['a'..'z']] ++ [i : show j | j <- [1..], i <- ['a'..'z'] ]

Are parameterized lambda terms a Monad?

1 Answers