21

さて、私は Haskell モナドを勉強しています。ウィキブックのカテゴリ理論の記事を読んだとき、モナド射の署名は論理のトートロジーにかなり似ていることがわかりましたが、 に変換する必要がありますM a。~~Aここ~に論理否定があります。

return :: a -> M a -- Map to tautology A => ~~A, double negation introduction
(>>=) :: M a -> (a -> M b) -> M b -- Map to tautology ~~A => (A => ~~B) => ~~B

他の操作もトートロジーです。

fmap :: (a -> b) -> M a -> M b -- Map to (A => B) -> (~~A => ~~B)
join :: M (M a) -> M a -- Map to ~~(~~A) => ~~A

また、通常の関数型言語のカリー・ハワード対応は古典論理ではなく直観論理であるという事実から、対応を持つことができるようなトートロジーを期待できないことも理解されてい~~A => Aます。

しかし、私は別のことを考えています。モナドが二重否定にしか関係ないのはなぜですか? 単一否定の対応は何ですか? これにより、次のクラス定義にたどり着きました。

class Nomad n where
    rfmap :: (a -> b) -> n b -> n a
    dneg :: a -> n (n a)

return :: Nomad n => a -> n (n a)
return = dneg
(>>=) :: Nomad n => n (n a) -> (a -> n (n b)) -> n (n b)
x >>= f = rfmap dneg $ rfmap (rfmap f) x

ここで「ノマド」と呼ばれる概念を定義し、2 つの操作をサポートします (どちらも直観的ロジックの論理公理に関連しています)。「rfmap」という名前は、そのシグニチャーが functor の に似ているが、とfmapの順序が逆になっているという事実を意味することに注意してください。これで、replace to を使用して、Monad 操作を再定義できます。abM an (n a)

それでは、質問の部分に行きましょう。モナドが圏論からの概念であるということは、私の「ノマド」も圏論の概念であることを意味しているようです。それで、それは何ですか？それは役に立ちますか？このトピックに関する論文や研究結果はありますか?

4

2 に答える 2

20

二重否定は特定のモナドです

data Void --no constructor because it is uninhabited

newtype DN a = DN {runDN :: (a -> Void) -> Void}

instance Monad DN where
   return x = DN $ \f -> f x
   m >>= k  = DN $ \c -> runDN m (\a -> runDN (k a) c))

実際、これはより一般的なモナドの例です

type DN = Cont Void
newtype Cont r a = Cont {runCont :: (a -> r) -> r}

これは継続渡しのモナドです。

「モナド」のような概念は、署名だけで定義されるのではなく、いくつかの法則によっても定義されます。では、ここで質問があります。建設に関する法律はどうあるべきですか?

(a -> b) -> f b -> f a

は、圏論でよく知られているメソッド、反変関手の署名です。基本的にファンクターと同じ法則に従います ((共) 構成と同一性を保持します)。実際、反変関手はまさに反対圏の関手です。エンドファンクターであるはずの「haskell ファンクター」に関心があるので、「haskell 反変ファンクター」がファンクターであることがわかりHask -> Hask_Opます。

一方、どうでしょう。

a -> f (f a)

これにはどのような法律が必要ですか？提案があります。圏論では、ファンクター間のマッピングが可能です。カテゴリからカテゴリへのF, Gそれぞれから2 つの関手が与えられた場合、からへの自然な変換は次の射です。CDFGD

forall a. F a -> G a

特定の一貫性の法則に従います。「ファンクタ カテゴリ」の定義に使用するなど、自然な変換を使用して多くのことができます。しかし、古典的なジョーク (Mac Lane による) は、カテゴリーはファンクターについて話すために発明され、ファンクターは自然変換について話すために発明され、自然変換は付加物について話すために発明されたというものです。

2 つの自然な変換が存在する場合、ファンクターF : D -> CとファンクターはtoG : C -> Dからの随伴を形成します。CD

unit : Id -> G . F
counit : F . G -> Id

この随伴の考え方は、モナドを理解するためのよくある方法です。すべての随伴は、完全に自然な方法でモナドを生じさせます。つまり、これら 2 つのファンクターの構成はエンドファンクターであり、返されるのに似たもの (ユニット) があるため、必要なのは結合だけです。しかし、それは簡単G . F . G . F -> G . Fです。join は、「中間」の counit を使用するだけで得られる関数にすぎません。

それで、これで、あなたが探しているのは何ですか？良い

dneg :: a -> n (n a)

unitは、反変関手とそれ自体の随伴の とまったく同じように見えます。したがって、あなたのNomad型は (確かに、モナドを構築するためにそれを使用するのが正しいなら) 「自己随伴である反変関手」とまったく同じである可能性があります。自己随伴ファンクターを検索すると、二重否定と継続の受け渡しに戻ります...これはまさに私たちが始めたところです!

編集:ほぼ確実に、上記の矢印のいくつかは後方です。ただし、基本的な考え方は正しいです。以下の引用を使用して、自分で解決できます。

圏論に関する最良の本はおそらく、

  • Steve Awodey、圏論
  • サンダース・マクレーン、働く数学者のためのカテゴリー

コンピュータ科学者のための圏論に関する Benjamin Pierces の本など、より親しみやすい入門書が多数存在しますが。

ビデオ講義オンライン

多くの論文が、継続モナドの随伴角を調査しています。たとえば、

  • ハヨ・ティーレケ、継続意味論と自己随伴性

「自己随伴」、「継続」、「モナド」という検索語が適しています。また、多くのブロガーがこれらの問題について書いています。「モナドはどこから来たのか」をグーグルで検索すると、n カテゴリ カフェのこのような有用な結果が得られます。また、sigfpeのこのような結果が得られます。Sjoerd Vissche の Comonad リーダーへのリンクもあります。

于 2012-12-20T13:32:24.020 に答える
8

それは自己随伴反変ファンクターになります。rfmap反変関手部分を提供しdneg、随伴の単位と補単位です。

Op rは、継続モナドを作成する例です。一部のコードについては、 http: //hackage.haskell.org/package/adjunctions の反変モジュールを参照してください。

関連する非常に興味深いhttp://comonad.com/reader/2011/monads-from-comonads/を読む必要があります。

于 2012-12-20T12:29:08.087 に答える