haskell - 参数化 lambda 项是 Monad 吗？

Question

我在 lambda 演算中通过名称类型参数化了术语表示:

{-# LANGUAGE DeriveFunctor #-}

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

我想知道 Lambda 是否可以成为 monad 的实例？我认为类似以下内容可能适用于 join 的实现:

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

对于第三种情况我完全不知道......但应该是可能的 -这个 lambda 项的无名表示，取自 De Bruijn Notation as a Nested Datatype ，是 Monad 的一个实例(Maybe 用于区分此表示中的绑定(bind)变量和自由变量):

{-# 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 对于实例 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'] ]

Answer 1

您的直觉是对的:在结合位点具有显式名称的术语不会形成单子(monad)。

>>= 的签名提供了一些值得深思的内容:

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

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

但是在结合位点进行替换是没有意义的。 lambda 项的参数在语法上不能是 lambda。 (\(\x -> y) -> y 在语法上无效。)在 Lam 构造函数中放入 a 意味着 Lambda 不能是 monad。

您要违反的特定法律是正确身份，其中规定对于所有x，x >>= return = 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 的 lambda 项表示是一个 monad，因为它局部无名。它们的 L 构造函数中没有 a；相反，您可以通过缩小变量值的长度来找到变量的绑定(bind)位点。正如论文所解释的，这是表示 de Bruijn 指数的一种方式(将 Just (Just Nothing) 与自然数 S (S Z) 进行比较)。

有关更多信息，请参阅 Kmett 的 detailed article描述他的设计bound图书馆，它使用伯德和帕特森的方法作为灵感来源之一。