Haskell Language
カテゴリ理論

抽象化を構成するシステムとしてのカテゴリ理論

カテゴリ理論は近代的な数学的理論であり、接続性と関係の性質に焦点を当てた抽象代数の枝である。高度な再利用可能なプログラミング抽象概念の多くに、強固な基盤と共通言語を提供するのに便利です。 Haskellは、標準ライブラリといくつかの一般的なサードパーティ製ライブラリの両方で利用可能ないくつかのコア型式のインスピレーションとしてカテゴリ理論を使用しています。

例

Functor型クラスは、入力した場合と言うFインスタンス化Functor （そのため私たちは書くFunctor F ）我々は、一般的な操作を持っています

fmap :: (a -> b) -> (F a -> F b)

私たちはF上に「マップ」することができます。標準（しかし不完全な）直感は、 F aがタイプaの値でいっぱいのコンテナでa 、 fmapはこれらの含まれた要素のそれぞれに変換を適用できるということです。一例はMaybe

instance Functor Maybe where
  fmap f Nothing = Nothing     -- if there are no values contained, do nothing
  fmap f (Just a) = Just (f a) -- else, apply our transformation

この直感を考えると、一般的な質問は、「なぜ呼んでないFunctorのような明白な何かMappable ？」。

カテゴリ理論のヒント

その理由は、Functorがカテゴリ理論の一般的な構造のセットに適合しているため、 Functor "Functor"と呼ぶことによって、この深い知識体系にどのようにつながるかを見ることができます。

特に、カテゴリー理論は、ある場所から別の場所への矢のアイデアに非常に関心があります。ハスケルでは、最も重要な一連の矢印は機能矢印a -> bです。カテゴリ理論で研究する共通のことは、矢印のセットが別のセットとどのように関連しているかです。特に、任意のタイプのコンストラクタFについて、形状F a -> F bの矢印の組も興味深い。

したがって、Functorは、通常のHaskellの矢印a -> bとF固有の矢印F a -> F bとの間に接続があるような任意のFです。接続はfmapによって定義され、また、保持する必要があるいくつかの法律も認識しています

forall (x :: F a) . fmap id x == x

forall (f :: a -> b) (g :: b -> c) . fmap g . fmap f = fmap (g . f)

これらの法則はすべてFunctorカテゴリ理論的解釈から自然に生じ、 Functorを「要素上のマッピング」に関連して考えると明らかに必要ではありません。

カテゴリの定義

カテゴリCは、

• Obj(C)と呼ばれるオブジェクトの集合。
• これらのオブジェクト間のモーフのコレクション（ Hom(C)と呼ばれるHom(C) 。場合及びa bであるObj(C)次いで射fにおけるHom(C) 、典型的に表されるf : a -> bとの間のすべての射の収集及びa bで示されるhom(a,b) 、
• 特別射は、 アイデンティティ射と呼ば-ごとにa : Obj(C)射が存在するid : a -> a 。
• 組成演算子（ . 、2射取る） f : a -> b 、 g : b -> cと射製造a -> c

以下の法律に従います。

For all f : a -> x, g : x -> b, then id . f = f and g . id = g

For all f : a -> b, g : b -> c and h : c -> d, then h . (g . f) = (h . g) . f

言い換えれば、恒等写像（左または右のいずれか）を持つ構図は他の写本を変えず、構図は連想である。

Haskellでは、 Category内型クラスとして定義されControl.Category ：

-- | A class for categories.
--   id and (.) must form a monoid.
class Category cat where
    -- | the identity morphism
    id :: cat a a

    -- | morphism composition
    (.) :: cat b c -> cat a b -> cat a c

この場合、 cat :: k -> k -> *は、モルフォリズムの関係を客観化します - cat abが住んでいる（つまり価値がある）場合に限り、モルフィスcat abが存在します。 a 、 b 、 cはすべてObj(C)ます。 Obj(C)自体は種類 k表されます。たとえば、通常はk〜 k ~ *のように、オブジェクトは型です。

HaskellのCategoryの標準的な例は関数カテゴリです：

instance Category (->) where
  id = Prelude.id
  (.) = Prelude..

別の一般的な例は、 Monad Kleisli矢印Categoryです。

newtype Kleisli m a b = Kleisli (a -> m b)

class Monad m => Category (Kleisli m) where
  id = Kleisli return
  Kleisli f . Kleisli g = Kleisli (f >=> g)

カテゴリとしてのHaskell型

カテゴリの定義

ハスケル型と型間関数は、カテゴリを形成します（ほぼ†）。すべてのオブジェクト（型） aに対して恒等写像（関数）（ id :: a -> a ）がaます。カテゴリの法律に従うモチズム（ (.) :: (b -> c) -> (a -> b) -> a -> c ::（ (.) :: (b -> c) -> (a -> b) -> a -> c ）

f . id = f = id . f
h . (g . f) = (h . g) . f 

私たちは通常このカテゴリをハスクと呼んでいます。

同型異性

カテゴリー理論では、逆行列を持つモプリズムを持つと同型写像があります。言い換えれば、同一性を作るためにそれと合成できるモプリズムがあります。 Haskでは、これは、以下のような一対の変量f 、 gを有する。

 f . g == id == g . f

2つの型の間にこのような変形を見つけると、それを互いに同形的と呼びます。

2つの同型タイプの例は((),a)ありaはa 。 2つのモーフを構築することができます：

f :: ((),a) -> a
f ((),x) = x

g :: a -> ((),a)
g x = ((),x)

そしてそれを確認することができf . g == id == g . f 。

Functors

カテゴリ理論のファンクタは、カテゴリから別のものにマッピングし、オブジェクトとモーフをマッピングします。私たちは、1つのカテゴリ、Haskellの種類のカテゴリHaskに取り組んでいるので、我々はHaskから出発地と目的地のカテゴリと同じ、と呼ばれているendofunctorsがあるHask、それらのファンクタにのみファンクタを見に行くされています。私たちのendofunctorは型を取って別の型を返す多相型です：

F :: * -> *

カテゴリのファンクタの法則（アイデンティティと構成を保持する）に従うことは、ハスケルファンクタ法に従うことと等価です。

fmap (f . g) = (fmap f) . (fmap g)
fmap id = id

そこで、我々はそれを、例えば、持っている[] Maybeまたは(-> r) Haskでファンクタです。

モナド

カテゴリ理論のモナドは、内師のカテゴリーのモノイドです 。このカテゴリには、オブジェクトF :: * -> *および自然な変換（すべてのa。F forall a . F a -> G a間の変換）としての内部フュージョンがモーフィングとしてあります。

モノイドオブジェクトはモノイドカテゴリで定義することができ、2つのモーフを持つタイプです。

zero :: () -> M
mappend :: (M,M) -> M

これをHask内フュージョン師のカテゴリに大まかに変換することができます：

return :: a -> m a
join :: m (m a) -> m a 

そして、モナド法に従うことは、カテゴリーモノモノオブジェクト法に従うことと等価です。

†実際には、タイプ間で関数のクラスと一緒にすべてのタイプのクラスは、厳密に起因するのexistanceに、Haskellのでカテゴリを形成しない undefined 。通常これは、単純にHaskカテゴリのオブジェクトを、終了しない関数と無限の値（コーダ）を除外した、ボトム値のない型として定義することで解決されます。このトピックの詳細については、 こちらを参照してください 。

ハスクのタイプの製品

カテゴリ製品

カテゴリ理論では、2つのオブジェクトX 、 Yの積は、 π1：Z→ Xとπ2：Z→Yの 2つの投影を持つ別のオブジェクトZです。別のオブジェクトからの他の2つのモーフがそれらの投影を通して一意的に分解する。つまり、 f1：W→Xとf2：W→Yが存在する場合、 π1→ g = f1とπ2 → g = f2となるような固有の写像g：W→Zが存在する。

ハスクの製品

これは、以下のようなHaskell型のHaskカテゴリに変換されますZはA 、 B積であり、

-- if there are two functions
f1 :: W -> A
f2 :: W -> B
-- we can construct a unique function
g  :: W -> Z
-- and we have two projections
p1 :: Z -> A
p2 :: Z -> B
-- such that the other two functions decompose using g
p1 . g == f1
p2 . g == f2

上記の法則に従う2つのタイプ A 、 Bの製品タイプは 、2つのタイプ(A,B) のタプルであり、2つの予測はfstとsndです。 f1 :: W -> Aとf2 :: W -> Bという2つの関数がある場合、次のように一意にそれらを分解することができることを確認することができます。

decompose :: (W -> A) -> (W -> B) -> (W -> (A,B))
decompose f1 f2 = (\x -> (f1 x, f2 x))

そして分解が正しいことを確認することができます：

fst . (decompose f1 f2) = f1
snd . (decompose f1 f2) = f2

同型異性までの一意性

AとB積としての(A,B)の選択は一意ではありません。論理的にも同等の選択肢もあります：

data Pair a b = Pair a b

また、我々はまた、選択されたかもしれない(B,A)生成物として、あるいは(B,A,())と我々はまた、規則に従って、上記のような分解関数を見つけることができます。

decompose2 :: (W -> A) -> (W -> B) -> (W -> (B,A,()))
decompose2 f1 f2 = (\x -> (f2 x, f1 x, ()))

これは、製品が一意ではなく、同型異性まで独特であるためです。 AとB 2つの積は等しい必要はありませんが、同形である必要があります。一例として、 (A,B)と(B,A,())定義した2つの異なる積は同型である：

iso1 :: (A,B) -> (B,A,())
iso1 (x,y) = (y,x,())

iso2 :: (B,A,()) -> (A,B)
iso2 (y,x,()) = (x,y)

分解の一意性

分解関数も一意でなければならないことに注意することが重要です。製品に必要なすべてのルールに従うタイプがありますが、分解は一意ではありません。たとえば、 (A,(B,Bool))を投影fst fst . snd使用することができfst . snd AとB積としてのfst . snd ：

decompose3 :: (W -> A) -> (W -> B) -> (W -> (A,(B,Bool)))
decompose3 f1 f2 = (\x -> (f1 x, (f2 x, True)))

我々はそれが動作することを確認することができます：

fst         . (decompose3 f1 f2) = f1 x
(fst . snd) . (decompose3 f1 f2) = f2 x

しかし、ここでの問題は、別の分解を書くことができたことです。

decompose3' :: (W -> A) -> (W -> B) -> (W -> (A,(B,Bool)))
decompose3' f1 f2 = (\x -> (f1 x, (f2 x, False)))

分解は一意ではないので 、 (A,(B,Bool))はHaskの AとB積ではありません

ハスクのタイプの共産品

直感

AとBの 2つのタイプのカテゴリ製品には、タイプAまたはタイプBのインスタンスの内部に含めるために必要な最小限の情報が含まれていなければなりません。今、2つのタイプの直観的な共生成物がEither abべきであることがわかります。 Either a (b,Bool)ような他の候補は、不必要な情報の一部を含んでいて、最小限ではありません。

正式な定義は、副産物のカテゴリー的な定義に由来します。

カテゴリの副産物

カテゴリコプロダクトは、カテゴリ型プロダクトの二重の概念です。これは、製品定義のすべての矢印を逆にすることによって直接得られます。 2つのオブジェクトX 、 Yの共生成物は、 i_1：X→Zとi_2：Y→Zの 2つの包含物を有する別のオブジェクトZである。 XおよびYから他の物体への他の2つのモーフィングが、これらの包含物を介して一意に分解する。換言すれば、2射f₁ある場合：X→Wとf₂：Y→W、ユニーク射gが存在する：Z→W例えばG○i₁=f₁およびg○i₂=f₂すなわち

ハスクのコプロダクト

Haskカテゴリへの翻訳は、製品の翻訳と似ています。

-- if there are two functions
f1 :: A -> W
f2 :: B -> W
-- and we have a coproduct with two inclusions
i1 :: A -> Z
i2 :: B -> Z
-- we can construct a unique function
g  :: Z -> W
-- such that the other two functions decompose using g
g . i1 == f1
g . i2 == f2

HaskのAとB 2つのタイプA 共生成型はEither abかそれと同型の他の型である：

-- Coproduct
-- The two inclusions are Left and Right
data Either a b = Left a | Right b

-- If we have those functions, we can decompose them through the coproduct
decompose :: (A -> W) -> (B -> W) -> (Either A B -> W)
decompose f1 f2 (Left x)  = f1 x
decompose f1 f2 (Right y) = f2 y 

カテゴリ理論の観点からのハスケル応用

HaskellのFunctorは任意の型a （ Haskのオブジェクト）を型F aに写像することができ、型a -> b （型のHask ）を型F a -> F b関数に写像することもできます。これは、ファンクタが基本的なカテゴリ構造を保持しているという意味で、カテゴリ理論の定義に相当します。

monoidalカテゴリは、いくつかの追加の構造を持つカテゴリです。

• テンソル積（ Haskの型の積を参照）
• テンソル単位（単位オブジェクト）

ペアを製品として使用する場合、この定義は次のようにHaskellに変換できます。

class Functor f => Monoidal f where
    mcat :: f a -> f b -> f (a,b)
    munit :: f ()

ApplicativeクラスはこのMonoidalクラスと同等であるため、このクラスで実装できます。

instance Monoidal f => Applicative f where
    pure x = fmap (const x) munit
    f <*> fa = (\(f, a) -> f a) <$> (mcat f fa)