参数化的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作为嵌套数据类型,是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'] ]

Answer 1

你的直觉是对的:在绑定站点上具有显式名称的术语不会形成monad.

签名>>=提供了一些思考的东西:

(>>=) :: 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)

类约束和monadic上下文使得这个签名与那个签名截然不同>>=!如果你真的试图实现name,unname你会发现你假设的类型是不正确的,joinL那就需要这些类.

Bird和Paterson对lambda术语的表示是monad,因为它在本地无名.a他们的L构造函数中没有; 相反,只要变量的值很长,就可以通过缩小找到变量的绑定站点.正如论文所解释的,这是表示de Bruijn指数的一种方式(Just (Just Nothing)与自然数相比S (S Z)).

有关更多内容,请参阅Kmett 详细描述其bound图书馆设计的文章,该文章使用Bird和Paterson的方法作为灵感来源.