パラメータ化されたラムダ条件はMonadですか？

Question

私は名前の種類の上にパラメータ化ラムダ計算における用語のこの表現を持っている：

{-# 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から、モナド（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を。我々は2種類のコンストラクタ間の同型を利用することにより、ラムダのため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

あなたの本能は正しかった：バインディングサイトに明示的な名前を付ける用語はモナドを形成しない。

>>=の署名は思考のためのいくつかの食べ物を提供しています：

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

はラムダ項をバインド置換を実行します。バインドする関数は、環境マッピング名aと、用語Lambda bです。 >>=は、名前がすべてaであることを検出し、それぞれが参照する環境の値と入れ替えます。 （従来の環境タイプのa -> Lambda bと[(a, Lambda b)]を比較してください）。

しかし、結合サイトで代用することは意味がありません。ラムダ項の議論は、構文的にラムダとはなり得ない。 （\(\x -> y) -> yは構文上有効ではありません）Lamコンストラクタにaを入れると、Lambdaはモナドにはなりません。あなたは違反だろう

特定の法律は、すべてのxためx >>= return = xを述べ右アイデンティティ、です。 （違反を確認するには、xをLamに設定してみてください。）

---

あなたは>>=はパターソンと鳥の論文に提供することをキャプチャ回避置換を実装する方法を検討したい、別の方法でそれを参照してください。 de Bruijnインデックスを使用していないときには、取り込みを避けることは難しいです。新しい名前のソースと一致する名前を識別する機能（新鮮な名前を使用する必要があるときを判断する）が必要です。

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

クラス制約とモナドコンテキストが>>=のそれよりも非常に異なるこの署名を行います。そのような機能の種類は次のようになります！実際にnameとunnameを実装しようとすると仮定したタイプが間違っていて、joinLにこれらのクラスが必要であることがわかります。

ラムダ用語のバードとパターソンの表現は、というローカル名がないので、モナドです。彼らのLコンストラクタにはaがありません。代わりに、変数の値が長い限りズームアウトすることで、変数のバインディングサイトを見つけることができます。この論文が説明しているように、これはBruijn指数を表現する一つの方法です（Just (Just Nothing)と自然数S (S Z)を比較してください）。

詳細については、彼のboundライブラリのデザインを説明するKmettのdetailed articleを参照してください.BirdとPatersonのアプローチをインスピレーションの源として使用しています。