Являются ли параметризованные лямбда-термины Монадой?

У меня есть это представление членов в лямбда-исчислении, параметризованное по типу имени:

{-# LANGUAGE DeriveFunctor #-}

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

Мне было интересно, может ли Lambda сделать экземпляр монады? Я думал, что для реализации join может работать что-то вроде следующего:

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

В третьем случае я не имею никакого понятия... но это должно быть возможно - это безымянное представление лямбда-терминов, взятое из De Bruijn Notation как вложенный тип данных, является экземпляром Monad (Maybe используется для различения между связанными и свободными переменными в этом представлении):

{-# 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 достаточно для 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

Предположим далее следующие две функции преобразования между представлениями:
unname :: Lamba a -> Expr a и name :: Expr a -> Lambda a. С помощью этих возможностей мы можем реализовать join для Lambda, используя изоморфизм между двумя конструкторами типов:

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

Но это кажется очень сложным. Есть ли более простой способ, или я пропускаю что-то важное?

Изменить: вот функции name и uname, которые, как я думал, будут выполнять эту работу. Как было отмечено в комментариях и ответе, a действительно требуется ограничение Eq, которое нарушает изоморфизм.

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

Ответы

Ответ 1

Ваш инстинкт был прав: термины, которые содержат явные имена на сайтах связывания, не образуют монаду.

Подпись >>= предлагает некоторую пищу для размышлений:

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

Связывание лямбда-члена выполняет замену. Функция, которую вы связываете, представляет собой сопоставление имен среды a с терминами Lambda b; >>= находит все вхождения имен a и свопирует каждый для значения из среды, к которой он относится. (Сравните a -> Lambda b с более традиционным типом среды, [(a, Lambda b)]).

Но нет смысла заменять на сайте привязки. Аргумент лямбда-термина не может синтаксически быть лямбдой. (\(\x -> y) -> y не является синтаксически допустимым.) Помещение a в ваш конструктор Lam означает Lambda не может быть монадой.

Конкретный закон, который вы нарушаете, является правильной личностью, которая содержит x >>= return = x для всех x. (Чтобы увидеть нарушение, попробуйте установить x на термин Lam.)

Чтобы увидеть это другим способом, подумайте о том, как реализовать реалистичную замену захвата, которую >>= предоставляет в документе Paterson and Bird. Невозможность замещения захвата затруднительна, если вы не используете индексы Bruijn: вам нужен источник свежих имен и возможность идентифицировать совпадающие имена (чтобы определить, когда вам нужно использовать свежий). Тип такой функции будет выглядеть примерно так:

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

Ограничения класса и монадический контекст делают эту подпись очень отличной от таковой >>=! Если вы действительно пытались реализовать name и unname, вы увидите, что типы, которые вы предположили, были неправильными, и что joinL потребует этих классов.

Представление лямбда-членов Берда и Патерсона является монадой, потому что оно локально безымянно. Там нет a в своем конструкторе L; вместо этого вы обнаружите сайт привязки переменных, увеличивая масштаб до значения переменной. Как объясняет газета, это один из способов представления индексов де Брейна (сравните Just (Just Nothing) с натуральным числом S (S Z)).

Подробнее см. Kmett подробная статья, описывающая дизайн его bound, которая использует подход Bird and Paterson в качестве одного из источников вдохновения.