82

圏論のモナドについて読んでいます。モナドの定義の 1 つは、随伴関手 (adjoint functor) のペアを使用します。モナドは、それらのファンクターを使用したラウンドトリップによって定義されます。どうやら随伴は圏論では非常に重要ですが、随伴関手の観点から Haskell モナドの説明を見たことがありません。誰かがそれを考えましたか？

4

5 に答える 5

41

編集：楽しみのために、私はこれを正しく行うつもりです。以下に保存されている元の回答

category-extrasの現在の随伴コードは、随伴パッケージに含まれています：http: //hackage.haskell.org/package/adjunctions

ステートモナドを明示的かつ単純に処理します。このコードはData.Functor.Composeトランスフォーマーパッケージから使用しますが、それ以外は自己完結型です。

f（D-> C）とg（C-> D）の間の随伴関手、f-|と書かれている gは、いくつかの方法で特徴付けることができます。counit / unit（epsilon / eta）の説明を使用します。これにより、2つの自然変換（ファンクター間の射）が得られます。

class (Functor f, Functor g) => Adjoint f g where
     counit :: f (g a) -> a
     unit   :: a -> g (f a)

コユニットの「a」は実際にはCのアイデンティティファンクターであり、ユニットの「a」は実際にはDのアイデンティティファンクターであることに注意してください。

counit/unit定義からhom-set随伴定義を復元することもできます。

phiLeft :: Adjoint f g => (f a -> b) -> (a -> g b)
phiLeft f = fmap f . unit

phiRight :: Adjoint f g => (a -> g b) -> (f a -> b)
phiRight f = counit . fmap f

いずれの場合も、次のように、ユニット/コユニットの随伴からモナドを定義できます。

instance Adjoint f g => Monad (Compose g f) where
    return x = Compose $ unit x
    x >>= f  = Compose . fmap counit . getCompose $ fmap (getCompose . f) x

これで、（a、）と（a->）の間の古典的な随伴を実装できます。

instance Adjoint ((,) a) ((->) a) where
    -- counit :: (a,a -> b) -> b
    counit (x, f) = f x
    -- unit :: b -> (a -> (a,b))
    unit x = \y -> (y, x)

そして今、タイプの同義語

type State s = Compose ((->) s) ((,) s)

そして、これをghciにロードすると、Stateがまさに私たちの古典的な州のモナドであることを確認できます。反対の構成を取り、Costate Comonad（別名ストアcomonad）を取得できることに注意してください。

この方法でモナドにすることができる他の随伴（（Bool、）Pairなど）はたくさんありますが、それらは一種の奇妙なモナドです。残念ながら、Haskellで直接ReaderとWriterを誘導する随伴関手を快適な方法で行うことはできません。Contを実行することはできますが、copumpkinが説明しているように、反対のカテゴリの随伴を必要とするため、実際には、いくつかの矢印を反転させる「随伴」型クラスの別の「形式」を使用します。その形式は、随伴関手パッケージの別のモジュールにも実装されています。

この資料は、The Monad Reader13のDerekElkinsの記事で別の方法でカバーされています-圏論によるモナドの計算：http：//www.haskell.org/wikiupload/8/85/TMR-Issue13.pdf

Monまた、Hinzeの最近のKan Extensions for Program Optimizationの論文では、との間の随伴からリストモナドの構築について説明しています。httpSet： //www.cs.ox.ac.uk/ralf.hinze/Kan.pdf

古い答え：

2つの参照。

1）カテゴリーエクストラは、いつものように、随伴関手とそれらからモナドがどのように発生するかを表現します。いつものように、考えるのは良いことですが、ドキュメントについてはかなり軽いです：http: //hackage.haskell.org/packages/archive/category-extras/0.53.5/doc/html/Control-Functor-Adjunction.html

2）-カフェはまた、随伴関手の役割についての有望であるが簡単な議論を提供します。そのうちのいくつかはcategory-extrasの解釈に役立つかもしれません：http：//www.haskell.org/pipermail/haskell-cafe/2007-December/036328.html

于 2011-01-15T22:31:48.763 に答える
10

(_ -> k)Derek Elkins は最近夕食の席で、 Contravariant functor を自分自身で構成することから Cont モナドがどのように発生するかを見せてくれました。それがあなたがそれから抜け出す方法です(a -> k) -> k。ただし、その counit は、Haskell では記述できない二重否定除去につながります。

これを説明および証明する Agda コードについては、 http://hpaste.org/68257を参照してください。

于 2011-01-15T03:05:52.077 に答える
9

これは古いスレッドですが、質問が面白いと思ったので、自分で計算をしました。うまくいけば、バルトスはまだそこにいて、これを読むかもしれません。

実際、この場合、アイレンベルグ・ムーア構造は非常に明確な画像を提供します。（私はHaskellのような構文でCWM表記を使用します）

Tリストモナド（< T,eta,mu >およびeta = return）mu = concatとし、T代数を考えh:T a -> aます。

（これT a = [a]は自由モノイド<[a],[],(++)>、つまりアイデンティティ[]と乗算であることに注意してください(++)。）

定義上、とhを満たす必要がh.T h == h.mu aありh.eta a== idます。

さて、いくつかの簡単な図の追跡は、実際に（で定義される）にhモノイド構造を誘導し、それがこの構造のモノイド準同型になることを証明します。x*y = h[x,y]h

逆に、< a,a0,* >Haskellで定義されているモノイド構造は、自然にT代数として定義されます。

このように（h = foldr ( * ) a0、'を'に置き換え、'(:)を アイデンティティに(*)マップ[]する関数）。a0

したがって、この場合、T代数のカテゴリは、HaskMon、HaskMonで定義可能なモノイド構造のカテゴリにすぎません。

（T代数の射が実際にモノイド準同型であることを確認してください。）

また、Grpの無料製品、CRngの多項式環などのように、リストをHaskMonのユニバーサルオブジェクトとして特徴付けます。

上記の構成に対応する裁定は< F,G,eta,epsilon >

どこ

  • F:Hask -> HaskMon、タイプaを'によって生成された自由モノイド'に取りますa。つまり[a]、、
  • G:HaskMon -> Hask、忘却関手（掛け算を忘れる）、
  • eta:1 -> GF 、によって定義される自然変換\x::a -> [x]、
  • epsilon: FG -> 1、上記の折りたたみ関数によって定義された自然変換（自由モノイドからその商モノイドへの「正準全射」）

次に、別の「クライスリ圏」とそれに対応する随伴関手があります。それが射のあるHaskellタイプのカテゴリでa -> T bあり、その合成がいわゆる「クライスリ合成」によって与えられていることを確認できます(>=>)。典型的なHaskellプログラマーは、このカテゴリーをよりよく知っているでしょう。

最後に、CWMに示されているように、T代数のカテゴリ（またはKleisliカテゴリ）は、適切な意味でリストモナドTを定義する裁定のカテゴリの最終（または初期）オブジェクトになります。

二分木ファンクターについても同様の計算を行ってT a = L a | B (T a) (T a)、理解度を確認することをお勧めします。

于 2011-02-26T05:04:22.480 に答える
2

Eilenberg-Moore による任意のモナドの付属ファンクターの標準的な構造を見つけましたが、それが問題への洞察を追加するかどうかはわかりません。構成の 2 番目のカテゴリは、T 代数のカテゴリです。AT 代数は、最初のカテゴリに「製品」を追加します。

では、リストモナドではどのように機能するのでしょうか? リストモナドのファンクターは、型構築子、例えば、Int->[Int]関数のマッピング (例えば、リストへのマップの標準的な適用) で構成されます。代数は、リストから要素へのマッピングを追加します。1 つの例は、整数のリストのすべての要素を加算 (または乗算) することです。functor は Int などのF任意の型を取り、それを Int のリストで定義された代数にマップします。ここで積はモナド結合によって定義されます (逆の場合、結合は積として定義されます)。忘却関手Gは代数を取り、積を忘れます。次に、随伴関手のペアF, , を使用して、通常の方法でモナドを構築します。G

私は賢明ではないと言わざるを得ません。

于 2011-01-15T21:51:18.390 に答える
1

興味のある方は、プログラミング言語におけるモナドと随伴の役割について、専門家ではない人の考えを以下に示します。

まず第一に、与えられたモナドTに対して のクライスリ圏への唯一の付属物が存在するT。Haskell では、モナドの使用は主にこのカテゴリの演算に限定されています (これは本質的に自由代数のカテゴリであり、商はありません)。実際、Haskell モナドでできることは、新しい射を作成するためa->T bに do 式などを使用して型の Kleisli 射を構成することだけです。(>>=)このコンテキストでは、モナドの役割は記法の経済だけに制限されています。射の結合性を利用して、 の[0,1,2] 代わりに(たとえば) 書けるようにし(Cons 0 (Cons 1 (Cons 2 Nil)))ます。つまり、シーケンスをツリーとしてではなく、シーケンスとして書けるのです。

現在の Haskell 型システムは、データのカプセル化 (存在型) を実現するのに十分強力であるため、IO モナドの使用でさえ必須ではありません。

これはあなたの元の質問に対する私の答えですが、Haskell の専門家がこれについて何と言っているか知りたいです。

一方、すでに述べたように、モナドと (T-) 代数の随伴の間には 1 対 1 の対応もあります。マクレーンの用語では、随伴は「カテゴリの同等性を表現する方法」です。がある種の「自由代数生成器」であり、G が「忘却関手」である典型的な随伴の設定では、対応するモナドは (T 代数を使用して) の代数構造がどのように (そしていつ)<F,G>:X->A構築されるかを記述します。のオブジェクト。FAX

Hask とリスト モナド T の場合、T導入される構造はモノイドの構造であり、モノイドの理論が提供する代数的方法を通じてコードのプロパティ (正確性を含む) を確立するのに役立ちます。たとえば、関数はモノイドであるfoldr (*) e::[a]->a限り連想演算と<a,(*),e>見なすことができます。これは、コンパイラが計算を最適化するために (たとえば、並列処理によって) 利用できるという事実です。もう 1 つのアプリケーションは、「関数型プログラミングの goto」である Y (任意の再帰コンビネーター) を (部分的に) 処分することを期待して、カテゴリー法を使用して関数型プログラミングの「再帰パターン」を識別および分類することです。

どうやら、この種の応用は圏論の創始者 (MacLane、Eilenberg など) の主な動機の 1 つであるようです。位相空間へのホモロジー的方法、プログラミングへの代数的方法など)。ここで、随伴とモナドは、このカテゴリの接続を利用するための不可欠なツールです。(ちなみに、モナド (およびその双対であるコモナド) の概念は非常に一般的であるため、Haskell 型の「コホモロジー」を定義することさえできます。しかし、私はまだ考えていません。)

あなたが言及した非決定的関数については、私が言うことははるかに少ないです...しかし、それに注意してください。<F,G>:Hask->Aあるカテゴリの付属物Aがリスト monadTを定義する場合、一意の「比較ファンクタ」K:A->MonHask(Haskell で定義可能なモノイドのカテゴリ) が存在する必要があります。CWM を参照してください。これは事実上、リストモナドを定義するために、関心のある圏が何らかの制限された形式のモノイドの圏でなければならないことを意味します (例えば、いくつかの商が欠けているかもしれませんが、自由代数ではないかもしれません)。

最後に、いくつかの発言:

前回の投稿で言及したバイナリ ツリー ファンクタは、任意のデータ型に簡単に一般化できます T a1 .. an = T1 T11 .. T1m | ...。つまり、Haskell の任意のデータ型は自然にモナドを定義し (対応する代数の圏と Kleisli 圏と共に)、これは Haskell の任意のデータ構成子が全である結果にすぎません。これが、Haskell の Monad クラスが単なる構文糖衣にすぎないと私が考えるもう 1 つの理由です (もちろん、これは実際には非常に重要です)。

于 2011-03-05T06:38:52.587 に答える