7

私はモナドのカテゴリー定義を、他のチュートリアル/本で見た他の一般的な表現/定義と調和させようとしています。

以下で、私は (おそらく強制的に) 2 つの定義を近づけようとしています。間違いを指摘し、必要に応じて修正してください。

モナドの定義から始めます

モナドは、エンドファンクターのカテゴリの単なるモノイドです。

エンドファンクターを少し理解すれば、モナドは次のように書けると思います。

((a->b)->Ma->Mb)->((b->c)->Mb->Mc)

TypeLHS(左辺)の「 」Mbは 、RHSの型は ですMcので、以下のように書けると思います。

Mb-> (b->c)-> Mc, **which is how we define bind**

そして、これが私がエンドファクターのカテゴリーでモナドをどのように見るかです（それ自体はCategoryCにあり、 ' types' as objects）

視覚的にモナド.

これは理にかなっていますか？

4

3 に答える 3

5

「モナドはエンドファンクターの範疇にある単なるモノイドである」という定義は、正しいとはいえ、始めるには不適切です。これは主に冗談を意図したブログ投稿からのものです。しかし、通信に興味がある場合は、Haskell でデモンストレーションできます。

カテゴリの一般的な記述は、オブジェクトとオブジェクト間のモーフィズムの抽象的なコレクションです。カテゴリ間のマッピングはファンクターと呼ばれ、オブジェクトをオブジェクトに、射を射に連想的にマップし、同一性を保持します。エンドファンクタは、カテゴリからそれ自体へのファンクタです。

{-# LANGUAGE MultiParamTypeClasses, 
             ConstraintKinds,
             FlexibleInstances,
             FlexibleContexts #-}

class Category c where
  id  :: c x x
  (.) :: c y z -> c x y -> c x z

class (Category c, Category d) => Functor c d t where
  fmap :: c a b -> d (t a) (t b)

type Endofunctor c f = Functor c c f

いわゆる自然性条件を満たすファンクター間のマッピングは、自然変換と呼ばれます。Haskell では、これらは型の多相関数です: (Functor f, Functor g) => forall a. f a -> g a.

圏上のモナドは、エンドファンクター、恒等ファンクターのC3 つである。Mu と eta は、三角形恒等式と結合性恒等式を満たす 2 つの自然な変換であり、次のように定義されます。(T,η,μ)T1C

  • η : 1 → T
  • μ : T^2 → T

Haskellμでは isjoinとηisreturn

  • return :: Monad m => a -> m a
  • join :: Monad m => m (m a) -> m a

Haskell での Monad のカテゴリ定義は、次のように記述できます。

class (Endofunctor c t) => Monad c t where
  eta :: c a (t a)
  mu :: c (t (t a)) (t a)

これらからバインド演算子を導出できます。

(>>=) :: (Monad c t) => c a (t b) -> c (t a) (t b)
(>>=) f = mu . fmap f

これは完全な定義ですが、同等に、モナドの法則がファンクター カテゴリを持つモノイドの法則として表現できることも示すことができます。オブジェクトをファンクター (つまり、カテゴリー間のマッピング) として持ち、自然な変換 (つまり、ファンクター間のマッピング) を射として持つカテゴリーである、このファンクター カテゴリーを構築できます。エンドファンクターのカテゴリーでは、すべてのファンクターは同じカテゴリー間のファンクターです。

newtype CatFunctor c t a b = CatFunctor (c (t a) (t b))

これにより、写像合成としてのファンクター合成を持つカテゴリが生じることを示すことができます。

-- Note needs UndecidableInstances to typecheck
instance (Endofunctor c t) => Category (CatFunctor c t) where
  id = CatFunctor id
  (CatFunctor g) . (CatFunctor f) = CatFunctor (g . f)

モノイドには通常の定義があります。

class Monoid m where
  unit :: m
  mult :: m -> m -> m

関手の圏上のモノイドは単位 a としての自然な変換と、自然な変換を組み合わせた乗算演算を持ちます。Kleisli 合成は、乗法を満たすように定義できます。

(<=<) :: (Monad c t) => c y (t z) -> c x (t y) -> c x (t z)
f <=< g = mu . fmap f . g

したがって、「モナドはエンドファンクターのカテゴリのモノイドにすぎない」ということになります。これは、エンドファンクターおよび (mu, eta) からのモナドの通常の定義の「ポイントフリー」バージョンにすぎません。

instance (Monad c t) => Monoid (c a (t a)) where
  unit = eta
  mult = (<=<)

少し代入すると、 のモノイド特性が(<=<)、モナドの自然な変換の三角形と結合図の同等のステートメントであることを示すことができます。

f <=< unit == f
unit <=< f == f

f <=< (g <=< h) == (f <=< g) <=< h

ダイアグラム表現に興味がある場合は、文字列ダイアグラムで表現する方法について少し書いています。

于 2013-09-21T06:29:40.863 に答える
2

重要なことを省略しているように思えます：

  • その定義に「モノイド」という言葉があります。あなたはあなたの投稿でそれを考慮しませんでした。
  • 正確に言うと「モノイドオブジェクト」に置き換えた方が良いです。モノイドは抽象代数に生き、モノイドオブジェクトは圏論に生きます。異なる種。
    • モノイドはあるカテゴリのモノイド オブジェクトですが、これはここでは関係ありません。
  • モノイド オブジェクトは、モノイド カテゴリでのみ定義できます。

したがって、定義を理解するためのパスは次のとおりです。

  • Haskell の型と関数Hask のカテゴリでエンドファンクタのカテゴリ (それをEと呼びましょう) を考えます。そのオブジェクトは Haskのファンクターであり、F から G への射は、いくつかのプロパティを持つ型 F a -> G a の多相関数です。
  • E上の構造を考えて、それをモノイド圏に変えます。つまり、関手と恒等関手の合成です。
  • ウィキペディアなどから、モノイド オブジェクトの定義を検討します。
  • 特定のカテゴリEでそれが何を意味するかを検討します。M はエンドファンクターであり、μ は「join」と同じ型、η は「return」と同じ型を持つことを意味します。
  • 「(>>=)」は「結合」によって定義されます。

アドバイス。すべてを Haskell で表現しようとしないでください。数学ではなく、プログラムを書くために設計されています。ここでは数学表記の方が便利です。なぜなら、ファンクターの合成を「∘」と書くことができるので、型チェッカーに困ることがありません。

于 2013-09-29T15:04:53.607 に答える