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

Answer 1

Your instinct was right: terms which feature explicit names at binding sites do not form a monad.

The signature of >>= offers some food for thought:

(>>=) :: Lambda a -> (a -> Lambda b) -> Lambda b

Binding a lambda term performs substitution. The function you bind is the environment mapping names a to terms Lambda b; >>= finds all the occurences of names a and swaps each for the value from the environment to which it refers. (Compare a -> Lambda b with a more traditional environment type, [(a, Lambda b)]).

But it doesn't make sense to substitute at a binding site. The argument of a lambda term can't syntactically be a lambda. (\(\x -> y) -> y is not syntactically valid.) Putting an a in your Lam constructor means Lambda can't be a monad.

The particular law that you'd violate is right identity, which states x >>= return = x for all x. (To see the violation, try setting x to a Lam term.)

---

To see it another way, consider how you'd implement the capture-avoiding substitution that >>= provides in Paterson and Bird's paper. Capture-avoiding substitution is tricky when you're not using de Bruijn indices: you need a source of fresh names and the ability to identify coinciding names (to determine when you need to use a fresh one). The type of such a function would look something like:

subst :: (MonadFresh a m, Eq a) => Lambda a -> (a -> Lambda a) -> m (Lambda a)

The class constraints and the monadic context make this signature very different than that of >>=! If you actually tried to implement name and unname you would see that the types you hypothesised were incorrect, and that joinL would require these classes.

Bird and Paterson's representation of lambda terms is a monad because it is locally nameless. There's no a in their L constructor; instead, you find a variable's binding site by zooming out as far as the variable's value is long. As the paper explains, this is one way of representing de Bruijn indices (compare Just (Just Nothing) with the natural number S (S Z)).

For more, see Kmett's detailed article describing the design of his bound library, which uses Bird and Paterson's approach as one source of inspiration.