1. ホーム
  2. haskell

[解決済み] アジャンクションとしてのモナド

2023-07-19 22:39:25

質問

カテゴリ理論におけるモナドについて読んでいます。モナドの1つの定義は、アドジョイントファンクターのペアを使用しています。モナドはこれらのファンクタを使ったラウンドトリップによって定義されます。どうやら、隣接関数はカテゴリ理論では非常に重要なようですが、Haskell のモナドを隣接ファンクタの観点から説明したものは見たことがありません。どなたか考えてみたことはありませんか?

どのように解決するのですか?

編集 : 一応、ちゃんとやりますよ。元の答えは以下に保存されています。

現在のcategory-extrasのadjunctionのコードはadjunctionsのパッケージにあります。 http://hackage.haskell.org/package/adjunctions

ステートモナドを明示的かつシンプルにやり通すだけです。このコードでは Data.Functor.Compose を使用していますが、それ以外は自己完結しています。

f (D -> C) と g (C -> D) の間のアジャンクションは、f -| g と書かれ、多くの方法で特徴づけることができます。ここでは、2 つの自然な変換 (ファンクタ間のモルヒズム) を与える、counit/unit (イプシロン/エータ) の記述を使用することにします。

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

counit の "a" は実際には C の identity functor であり、unit の "a" は実際には D の identity functor であることに注意してください。

また、couit/unitの定義からhom-set adjunctionの定義を復元することができる。

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がまさに我々の古典的なstateモナドであることが確認できる。なお、逆の構成で、Costate Comonad (別名 store comonad)を得ることができる。

この方法でモナドにできる隣接は他にもたくさんあります((Bool,) Pairなど)が、これらは一種の奇妙なモナドです。残念ながら、HaskellではReaderとWriterを直接誘導するような心地よい方法での連接はできません。私たちは はできます。 Cont はできるが,copumpkin が説明するように,それには反対のカテゴリからの隣接が必要なので,実際にはいくつかの矢印を反転させる "Adjoint" 型クラスの別の "form" を使うことになる.この形式は adjunctions パッケージの別のモジュールで実装されています。

この材料は、The Monad Reader 13 -- Calculating Monads with Category Theory の Derek Elkins の記事で、別の方法でカバーされています。 http://www.haskell.org/wikiupload/8/85/TMR-Issue13.pdf

また、Hinze の最近の論文 Kan Extensions for Program Optimization では、リストモナドの構築について、以下の間の連接から説明されています。 MonSet : http://www.cs.ox.ac.uk/ralf.hinze/Kan.pdf


古い回答です。

2つのリファレンス

1) Category-Extrasは、いつものように、隣接関数の表現と、そこからどのようにモナドが発生するかを提供しています。いつものように、それは一緒に考えるには良いですが、ドキュメントについてはかなり軽いです。 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