Monads as adjunctions

Question

私はカテゴリ理論でモナドについて読んできました。モナドの定義の1つは、1組の随伴ファンクタを使用します。モナドは、それらのファンクタを使用するラウンドトリップによって定義されます。どうやら副作用はカテゴリ理論では非常に重要ですが、私は橋渡しファンクタの観点からハスケルのモナドについて何の説明も見ていません。誰かがそれを考えていたのですか？

Answer 1

を編集してください：ちょうど楽しみのために、私はこれを正しく行うつもりです。私は明示的に、単純な状態モナドを介して動作するつもりですhttp://hackage.haskell.org/package/adjunctions

：

今カテゴリのエキストラのための現在のadjunctionコードの下に保存され、元の答えはadjunctionsパッケージです。このコードでは、トランスフォーマーパッケージのData.Functor.Composeを使用しますが、それ以外の場合は自己完結型です。

f（D - > C）とg（C - > D）の間の補助は、f - gは、多くの点で特徴づけることができる。私たちは、2つの自然な変換（ファンクタ間の変形）を与えるcounit/unit（ε/η）の説明を使用します。 「」counit本当にCにおけるアイデンティティファンクタであり、「」の単位は、本当に我々はまた、HOM-セットを回復することができますD.

におけるアイデンティティファンクタであることを

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

注意カウント/ユニット定義からの補助的な定義。

いずれの場合においても

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 

、我々は今、とても気に入りまし単位/ counitのadjunctionからモナドを定義することができます。

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

は、今、私たちは（、）との間の古典的なadjunctionを実装することができます（ - > ）：

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にロードすると、状態が古典的な状態のモナドであることが確認できます。反対の構図をとり、Costate Comonad（別名店舗コモナード）を得ることができることに注意してください。

（Bool、）ペアのように、このような方法でモナドにすることができる他の補助機能がありますが、それらは奇妙なモナドの一種です。残念ながら、HaskellでReaderとWriterを楽しい方法で直接誘導する補助機能を実行することはできません。私たちはです。 do Contを使っていますが、反対派の補助詞を必要とするので、実際にはいくつかの矢印を反転する "Adjoint"型の別の "形式"を使用しています。そのフォームは、adjunctionsパッケージ内の別のモジュールでも実装されています。またhttp://www.haskell.org/wikiupload/8/85/TMR-Issue13.pdf

、プログラムの最適化、紙用Hinzeの最近のKan拡張が建設を通じて歩く：圏論でモナドの計算 -

この材料はモナドリーダー13でデレク・エルキンズ記事によって異なる方法で覆われています。 MonとSet間adjunctionからリストモナド：http://www.cs.ox.ac.uk/ralf.hinze/Kan.pdf

---

旧答え：

つ参照。

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

2）-Cafeはまた、補助療法の役割について有望ではあるが簡単な議論を提供します。いくつかはカテゴリーエクストラの解釈に役立つかもしれません：http://www.haskell.org/pipermail/haskell-cafe/2007-December/036328.html

Answer 2

デレク・エルキンズは最近、コントラモナードが(_ -> k)反作用ファンクタを構成することからどのようにして夕食を取ったかを私に示していました。それはあなたがそれから(a -> k) -> kを得る方法です。しかし、その議会は、二重否定撤廃につながり、ハスケルでは書けない。

これを例示して証明する一部のAgdaコードについては、http://hpaste.org/68257を参照してください。

Answer 3

私はEilenberg-Mooreのモナドの補助ファンクタの標準的な構成を見つけましたが、問題に洞察を加えているかどうかはわかりません。構築の第2のカテゴリーは、T-代数のカテゴリである。 T代数は初期カテゴリに「製品」を追加します。

リストモナドではどのように動作しますか？リストモナドのファンクタは、タイプコンストラクタ、例えば、Int->[Int]と、ファンクションのマッピング（例えば、リストのマップの標準アプリケーション）とからなる。代数はリストから要素へのマッピングを追加します。 1つの例は、整数リストのすべての要素を追加（または掛け算）することです。ファンクタFは、Intなどの任意の型を取って、Intadのリストで定義された代数にマッピングします。ここで、製品はモナド結合によって定義されます（またはその逆は、結合として定義されます）。忘れてしまったファンクタGは代数を取り、製品を忘れてしまいます。次に、通常の方法でモナドを構築するために、adjoint functorのF、Gのペアを使用します。

私は誰も賢明ではないと言わなければなりません。

Answer 4

これは古いスレッドですが、興味深い質問がありました。 私は自分で計算をしました。うまくいけばBartoszはまだそこにある そしてこれを読むかもしれない..

実際、このケースでは、Eilenberg-Mooreの構築は非常に明確な画像を与える。 （私は、構文のように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この構造のためにモノイド準同型となることを証明しています。逆に、Haskellで定義された任意のモノイド構造体< a,a0,* >は、当然、T代数として定義される。このようにして

（h = foldr (*) a0、機能その '置き換え' (:)(*)と、そしてマップ[]アイデンティティ、a0まで）。

この場合、T-algebrasのカテゴリは、HaskellのHaskellで定義される単層構造のカテゴリに過ぎません。

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

それはまたちょうどGrpの中のフリー製品のようHaskMonユニバーサルオブジェクト、CRNGにおける多項式環としてリストを特徴付けるなど

上記構成に対応adjuctionは、

• F:Hask -> HaskMon< F,G,eta,epsilon >

  ありますこれ 'aによって生成された自由モノイド'、すなわち、[a]、

• G:HaskMon -> Hask、物忘れファンクタ（乗算を忘れる）、
• eta:1 -> GF、\x::a -> [x]によって定義される自然形質転換にA型を取り、
• epsilon: FG -> 1 、（その商モノイドに自由モノイドから「正規全射」） 上記折り畳み機能によって定義される自然形質転換

次に、別の「クライスリ圏」および対応するadjunctionがあります。 これは、それが組成物がいわゆる「Kleisli組成」(>=>)によって与えられている場合に、それが形態素を有するハスケルタイプのカテゴリーだけであることを確認することができる。a -> T b、 。 典型的なHaskellのプログラマーは、このカテゴリーをよりよく知っています。

CWMに示すように最後に、T-代数 （RESP。クライスリ圏）のカテゴリが適切な意味でリストモナドTを定義adjuctionsのカテゴリ 端末（それぞれ初期）対象となります。

バイナリツリーファンクタT a = L a | B (T a) (T a)の同様の計算を行い、理解を確認することをお勧めします。

Answer 5

興味のある方は、ここではプログラミング言語でのモナドとadjunctionsの役割に関する非専門家 のいくつかの考えがあります：すべての

まず、Kleisliに固有adjunctionに与えられたモナドTのために存在しますカテゴリはTです。 ハスケルでは、モナドの使用は、主にこのカテゴリの操作 （これは本質的に無料代数のカテゴリであり、商はありません）に限定されています。 実際には、ハスケルモナドはdo_t式(>>=)などの タイプa->T bのいくつかのKleisliモーフィングを構成して、新しい モーフを作成することができます。このコンテキストでは、モナドの役割は表記の経済 に限定されています。ではなく[0,1,2] の代わりに を書くことができます。木。

IOモナドの使用は必須ではありません。現在のHaskellタイプのシステムは、データカプセル化（実在のタイプ）を実現するのに十分なほど強力です（ ）。

これは私のオリジナルの質問 に対する私の答えですが、私はハスケルの専門家がこれについて何を言わなければならないのか不思議です。

一方、前述したように、（T-）代数には、モナドと 補助関数との間にも1対1の対応があります。 MacLaneの言葉では、節点は「類義語を同等に表現する方法」です。 <F,G>:X->Aの典型的な設定では、Fが「無料代数ジェネレータ」とG a 'forgetful functor'の何種類かの である場合、対応するモナド は（T-代数を使用して）代数的方法構造AはXのオブジェクト上に構築されます。 Hask、リストモナドT、T発表はモノイドの であり、これはそのモノイドの理論代数 方法でコードの（正当含む）の特性を確立するために、私たちを助けることができる構造の場合

提供します。例えば、foldr (*) e::[a]->aは、がモノイドである限り、連想操作として容易に見ることができる。コンパイラが計算を最適化するために（例えば並列性によって）利用することができるファクトである。 もう1つのアプリケーションは、関数的プログラミングの '再帰パターン'を識別して分類することです（関数的プログラミングのGoto、Y（任意再帰結合子））を部分的に処分できるようにするために、カテゴリの メソッドを使用します。

明らかに、この種のアプリケーションは、カテゴリ理論（MacLane、Eilenbergなど）の作成者、すなわちカテゴリの自然な等価性を確立し、よく知られている方法を1つに移すことの主な動機の1つですカテゴリ を別のもの（例えば、位相空間への相同性方法、プログラムへの代数方法など）に変換する。 ここでは、随伴物とモナドは、このカテゴリの接続を利用するために不可欠なツールです。 （ちなみに、モナド（およびその二重のコモノド）の概念は非常に一般的で、 ハスケル型のコホモロジーを定義することさえできます。しかし、私はまだ考えを与えていません。）

あなたが言及した非決定的な機能については、私ははるかに少ないと述べています... しかし、注意してください;あるカテゴリののAがリストモナドを定義している場合T、 固有の「比較ファンクタ」K:A->MonHask（ハスケルで定義可能なモノイドのカテゴリ）はCWMを参照してください。 これは実際には、リストモナドを定義するために、関心のあるカテゴリがある制限された形式のモノイドのカテゴリでなければならないことを意味します（例えば、いくつかの商が不足していますが、自由な代数はありません）。

は最後に、いくつかの発言：

私は私の最後の投稿で述べたバイナリツリーファンクタは簡単に任意のデータ型 T a1 .. an = T1 T11 .. T1m | ...に一般化します。 つまり、ハスケルのどのデータ型でも、ハスケルのデータコンストラクタが合計された結果であるモナド（代数とKleisliカテゴリの対応するカテゴリと共に） が自然に定義されます。 これは、私がHaskellのMonadクラスが構文砂糖 （それは実際にはかなり重要です）以上のものではないと考えているもう一つの理由です。