参数化的lambda项是否是一个Monad？

Question

我有一个用lambda演算表示的术语，参数化于名称类型上：

{-# 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 as a Nested Datatype，它是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。通过利用这两种类型构造函数之间的同构，我们可以实现Lambda的join。

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

- jules

---

我不熟悉这个框架，但我不明白 name 和 unname 是如何工作的。你如何将例如 Lam (\x -> x+1) (Var (\y -> 2*y)) :: Lambda (Int->Int) 转换成 Expr (Int->Int)？这些类型真的是同构的吗？这种转换是否需要函数的 Eq （我只是猜测...）？ - chi

@chi 你是对的... a 需要一个 Eq 约束。这会破坏同构吗？ - jules

我之所以提到这个，是因为 constraints 和 Monads 搭配得不好。例如，Set 应该是一个 monad，但涉及的 Ord 约束阻止了这种情况。另外，Lam fresh ... 看起来像是一个 Lambda String 值，而不是一个 Lambda a。它真的通过类型检查吗？ - chi

正如另一个最近的回答中提到的那样，@chi，“Set”仅是“Hask”中非满子范畴中的一个函子。唯一允许的态射是双射。 - dfeuer

Answer 1

你的直觉是正确的：在绑定位点具有显式名称的术语不形成单子。

>>=的签名值得深思：

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

绑定lambda项执行替换。您绑定的函数是将名称a映射到术语Lambda b的环境；>>=查找名称a的所有出现，并将每个名称替换为它引用的环境中的值。(将a -> Lambda b与更传统的环境类型[(a，Lambda b)]进行比较)。

但在绑定位置替换没有意义。lambda项的参数不能语法上是lambda。（\（x -> y）- > y不是语法上有效的。）将a放入Lam构造函数中意味着Lambda不能是一种单子。（monad）

您违反的特定规则是正确标识符，它声明x >>= return = x适用于所有x。（要看到违规情况，请尝试将x设置为Lam项。）

换个角度看，考虑如何实现Paterson和Bird论文中提供的避免捕获替换。如果您不使用de Bruijn指数，则避免捕获替换很棘手：您需要一种新名称的来源以及能够识别重合名称的能力（以确定何时需要使用新名称）。这样一个函数的类型会看起来像：

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

类约束和单子上下文使得这个签名与>>=非常不同！如果你实际尝试实现name和unname，你会发现你所假设的类型是错误的，并且joinL需要这些类。

Bird和Paterson对λ项的表示是一种单子，因为它是本地无名的。在他们的L构造函数中没有a；相反，你可以通过缩小到变量的值所在的位置来找到变量的绑定位置。正如论文所解释的那样，这是一种表示de Bruijn指数的方法（将Just (Just Nothing)与自然数S (S Z)进行比较）。

更多信息，请参见Kmett的详细文章，描述了他的bound库的设计，其中使用Bird和Paterson的方法作为灵感之一。

- Benjamin Hodgson