エントリー
この短い記事では、Haskell型システムの文脈におけるカテゴリー理論について説明します。 ザミ、トリックはありません-私はすべてを明確に説明しようとします。 私は、プログラミング言語と数学の密接な関係を示して、読者が他の人を介して、またはその逆を認識できるようにします。
すでにハブにあるこのトピックの翻訳を繰り返したくありません：
カテゴリー理論の観点からのモナドですが、記事の完全性のために、私はまだ基本的な定義を与えます。 同時に、その記事とは異なり、数学に焦点を合わせたくありません。
この記事は、英語の
Haskell Wikibookからのセクション（図の借用を含む）の大部分を繰り返していますが、それでも直訳ではありません。
カテゴリとは何ですか？
例
わかりやすくするために、最初に単純なカテゴリを描いたいくつかの写真を考えます。 赤い丸と矢印があります：
赤い丸は「オブジェクト」を表し、矢印は「射」を表します。
オブジェクトと射の性質についての直観的なアイデアを提供する実生活の実例を1つ挙げたいと思います。
都市は「オブジェクト」と見なされ、都市間の動きは「形態」です。 たとえば、フライトのマップ（どういうわけか私は良い写真を見つけられませんでした）や鉄道のマップを想像できます-それらは上の写真のように見えますが、より複雑です。 現実には当たり前のように見える2つのポイントに注意を払う必要がありますが、将来的には重要です。
- ある都市から別の都市に電車や飛行機で行くことはできません。これらの都市の間には形態がありません。
- 同じ都市内を移動する場合、これも射であり、都市から都市への移動です。
- サンクトペテルブルクからモスクワへの列車があり、モスクワからアムステルダムへのフライトがある場合、列車のチケットと飛行機のチケットを購入し、それらを「組み合わせて」サンクトペテルブルクからアムステルダムに行くことができます-つまり、マップ上で、サンクトペテルブルクからアムステルダムへの矢印を描画して、この複合型の形態を描写します。
この例ですべてが明確になることを願っています。 そして今、明確にするために少し形式主義。
定義
そのため、カテゴリはオブジェクトと射で構成されていることがすでにわかっています。
- オブジェクトのクラス（セット）があります 。 オブジェクトは任意のエンティティにできます。
- 任意の2つのオブジェクト
AとBについて、 射影 Hom(A,B)のクラス Hom(A,B)定義されています。 このクラスの射f場合、オブジェクトAは領域と呼ばれ、 Bは共領域と呼ばれます。 次のように書かれています。
f ∈ Hom(A,B)またはf : A → B - 任意の2つの射
f : A → Bおよびg : B → C 、それらの構成が定義されます-射h = g ∘ f
h : A → C 領域gと共領域f一致することが重要です。 - 合成は連想的です 。つまり、すべての射
f : A → B 、 g : B → Cおよびh : C → D 、等式
(h ∘ g) ∘ f = h ∘ (g ∘ f) - すべてのオブジェクト
Aには、 id A : A → A示される「単位」射があり、構成に関して中立です。つまり、射f : A → Bに対して、次のことが成り立ちます。
id ∘ f = f = f ∘ id A
将来、インデックスは私を悩ませ、そのリージョン/コリージョンはコンテキストから復元されるので、ちょうど
idを書きます。
上記の例では、すべての特性が満たされていることが確認できます。必要に応じて、構成は連想的であり、対応する単位射はそれに関して中立です。 唯一の問題は、都市間を移動する例の関連性で発生します。ここでは、特定の人の連続した動きだけでなく、「合成チケット」として構成を考える必要があります。
自習問題：次の画像がカテゴリかどうかを確認します
Haskカテゴリ
そして今、主要な例、記事の主要なトピック。
Haskカテゴリは、Haskell言語タイプとそれらの間の機能で構成されます。 より厳密に：
- Haskオブジェクト： 1
*データ型。 たとえば、プリミティブ型： Integer 、 Bool 、 Charなど。 「タイプ」は種類* → *持っているMaybeが、 Maybe Bool型は種類*を持っているため、 Haskのオブジェクトです。 パラメーター化された型でも同じですが、後で説明します。 指定： a ∷ * ≡「タイプaは種類*があります」object「 aはHaskのオブジェクトです」。 - Hask射 ：1つのオブジェクト（タイプ）から別のオブジェクトへのHaskell関数。
a, b ∷ *場合、関数f ∷ a → bは領域aと共領域f ∷ a → bを持つ射である。 したがって、オブジェクトaとb間の射のクラスは、タイプa → b示されます。 数学表記で類推を完了するには、次の同義語を入力できます。
type Hom(a,b) = a → b
しかし、私の意見では矢印がより明確なので、私はそれを使い続けません。 - 構成：標準機能
(.) ∷ (b → c) → (a → b) → (a → c) 。 任意の2つの関数f ∷ a → bおよびg ∷ b → c合成g . f ∷ a → c g . f ∷ a → cは自然に定義されます：
g . f = λx → g (fx)
- 構成の結合性は、この定義から明らかです。
f ∷ a → b 、 g ∷ b → cおよびh ∷ c → d
(h . g) . f ≡ h . (g . f) ≡ λx → h (g (fx))
直接確認： (h . g) . f ≡ λx → (h . g) (fx) ≡ λx → (λy → h (gy)) (fx) ≡ λx → h (g (fx)) h . (g . f) ≡ λx → h ((g . f) x) ≡ λx → h ((λy → g (fy)) x) ≡ λx → h (g (fx))
- 任意の型
a ∷ *関数id ∷ a → aも自然に定義されます。
id = λx → x
この定義から、必要なプロパティが満たされていることは明らかです。 f ∷ a → b
f . id ≡ λx → f (id x) ≡ λx → fx ≡ f id . f ≡ λx → id (fx) ≡ λx → fx ≡ f
この関数は多態的であるため、1つだけですが、単一の射の観点からは、特定の型ごとに個別の射として認識されます。たとえば、
Charオブジェクトの場合、単
id ∷ Char → Charます。 そのため、以前にインデックスについて話しました。Haskellでは、必要な
idを正確に記述する必要はありません。そのタイプはコンテキストから自動的に推測されるためです。
したがって、見てのとおり、必要なすべてのエンティティが存在し、それらの関係が表示され、必要なプロパティが満たされているため、
Haskは本格的なカテゴリです。 最小限の構文変更で、すべての概念と構造が数学表記からHaskellにどのように転送されるかに注意してください。
さらに、ファンクターとは何か、
Haskカテゴリでどのように具体化されるのかを説明します。
ファンクター
ファンクターは、あるカテゴリーから別のカテゴリーへの変換です。 各カテゴリはオブジェクトと射で構成されているため、ファンクターはマッピングのペアで構成されている必要があります：1つは最初のカテゴリのオブジェクトを2番目のオブジェクトにマッピングし、もう1つは最初のカテゴリの射にマッピングします-2番目の射
最初に数学的な定義を示し、次にHaskellの場合にそれがいかに単純になるかを示します。
数学的定義
Cと
D 2つのカテゴリー
Cと
Dとファンクター
Fを考えます
D 表記法は射の場合と同じです。ファンクターだけが大文字で示されます：
F : C → D この
Fは2つの役割があります。
- カテゴリ
C各オブジェクトAは、カテゴリDオブジェクトに関連付けられ、 F(A)示されます。 - 各射
g : A → BカテゴリーC g : A → BはカテゴリーD射に関連付けられ、 F(g) : F(A) → F(B)表されます。
ここでも、ファンクターはマッピングのペアです。
A ↦ F(A) g : A → B ↦ F(g) : F(A) → F(B)
図では、最初のディスプレイが黄色の破線の矢印で示され、2番目のディスプレイが青で示されています。
ファンクターは、2つの完全に自然な要件を満たす必要があります。
- 与えられたオブジェクトのすべての単射をその画像の単射に変換する必要があります。
F(id A ) = id F(A) - 彼は射の合成を画像の合成に変換しなければなりません：
F(h ∘ g) = F(h) ∘ F(g)
Haskのファンクター
ここで、
Haskカテゴリーから
Haskへのファンクターを見てみましょう。 ところで、カテゴリをそれ自体に変換するそのようなファンクターは、
endofunctorsと呼ばれ
ます 。
したがって、型を型に変換し、関数を関数に変換する必要があります-2つのマッピング。 そして、Haskell言語の最初の構造は何ですか？ そうです、種類が
* → *です。
たとえば、前述のタイプ
Maybe ∷ * → * 。 これは、任意のオブジェクト
a ∷ *同じカテゴリのオブジェクト
(Maybe a) ∷ *マップするマップです。 ここで
Maybe aは、与えられたパラメータ
a持つパラメータ化された型のコンストラクタとしてではなく、数学的な定義からの
F(A)似た単一の文字として理解さ
Maybe aべきです。
したがって、最初のマッピングは無料で提供されます。これは、パラメータを持つ型コンストラクタです。
data Maybe a = Nothing | Just a
しかし、2番目のマッピングを取得する方法は？ Haskellはこのための特別なクラスを定義しています：
class Functor f where fmap ∷ (a → b) → (fa → fb)
ここで
f ∷ * → * 。 つまり、
fmapは、
a → bの射を取り、
fa → fb射を返す多相関数です。 これに基づいて、関数を定義することで、
Maybe本当のファンクターにします。
instance Functor Maybe where fmap g = fg where fg Nothing = Nothing fg (Just x) = Just (gx)
そこで、2つのマッピングを取得しました。
a ∷ * ↦ Maybe a ∷ * g ∷ a → b ↦ fmap g ∷ Maybe a → Maybe b
数学表記とは異なり、名前が異なることは何もありません。言語の特異性はそのようなものですが、意味にはまったく影響しません。
さて、要件を満たすのはどうですか？
fmapは
idを保存し、構成を構成に変換する必要があります。
fmap id ≡ id fmap (h . g) ≡ (fmap h) . (fmap g)
簡単に確認できます。これは、上記の
Maybeの
fmap定義の場合です。
パラメーターを使用して型コンストラクターを宣言するだけで、最初のマッピングが取得されることに注意してください。 彼にとって、オブジェクト間の表示に関しては、
Maybeタイプがどのように機能するかは問題ではありません
Maybe aオブジェクトをオブジェクト
Maybe aにマッピングするだけです。
射のマッピングの場合、すべてがそれほど単純ではありません
fmap型の構造が与えられた場合、
fmapを手動で決定する必要があります。 一方で、これにより柔軟性が得られます。特定のデータ構造をどの関数が変換するかを決定します。 しかし、一方で、この定義を自然な方法で配置したい場合は、この定義を無料で受け取ることが便利です。 たとえば、タイプ
data Foo a = Bar a Int [a] | Buz Char Bool | Qux (Maybe a)
関数
g ∷ a → bは、すべてのデータコンストラクターを再帰的に走査し、タイプ
aパラメーターがある場合は、
gを使用して変換する必要があります。 さらに、
[a]または
Maybe a場合、それらの
fmap gが機能するはずです。これにより、再び構造がバイパスされ、変換されます。
そして見よ、それは可能である！ GHCには
対応する拡張子があります。 コードを記述します。
{-# LANGUAGE DeriveFunctor #-} … data Foo a = … deriving Functor
そして、対応する
fmap持つ
Haskカテゴリの本格的な
エンドファンカー Fooをすぐに取得します。
ところで、これらのファンクターは、実際にはその
サブカテゴリ 、つまりオブジェクトと射のより小さなクラスを持つカテゴリに
Haskカテゴリを表示していると言う価値があります。 たとえば、
a ↦ Maybe aをマッピング
a ↦ Maybe aにより、単純なタイプの
Int取得することはできません。 それでも、結果として生じるオブジェクトのサブクラスと、射としてのそれらの関数のクラスもカテゴリを形成します。
Functorクラスの
ドキュメントでは、実施形態が最初に定義されているタイプのリストも見ることができます。 しかし、それらは主に、後でこのタイプがモナドであると言うために作られています。
おわりに
それで、
Haskカテゴリーとその中のファンクターについて話しました。これがHaskell型システムを新しい視点で理解するのに役立つことを願っています。 おそらく誰もが
fmapの意味を、ファンクターとは何かを知らずに独自の方法で理解しているため、実用的な観点からはおそらく役に立たないようです。 しかし、その後、
Haskカテゴリ
キーの自然な変換、モナド、およびその他のカテゴリ構造について記述し
ます。そして、数学的な類推がより有用になり、これらの言語構造の内部の性質をよりよく理解し、将来より意識的に適用できるようになると思います。
- 誰かが以前に種類の種類に会ったことがない場合、簡単に説明します。 種類は、通常の型に対する型システムの一種です。 種類には次の2種類があります。
* -これは、単純なパラメーター化されていないタイプの種類です。 たとえば、 Bool 、 Charなど。 カスタムdata Foo = Bar | Buz (Maybe Foo) | Quux [Int]タイプdata Foo = Bar | Buz (Maybe Foo) | Quux [Int] data Foo = Bar | Buz (Maybe Foo) | Quux [Int] data Foo = Bar | Buz (Maybe Foo) | Quux [Int]もシンプルになります： data Foo = Bar | Buz (Maybe Foo) | Quux [Int] Foo ∷ * 、 型コンストラクターにはパラメーターがないため（ データコンストラク ターにはありますが）… → …これはより複雑な種類で、楕円の場所に*と→で構成される他の種類を含めることができます。 例： [] ∷ * → * 、または(,) ∷ * → (* → *)またはさらに複雑なもの： ((* → *) → *) → (* → *) 。
このすべての意味は簡単です。型コンストラクターは型の一種の関数であり、種類はこれらの関数が正しく相互作用する方法を記述します。 たとえば、 [Maybe] write [] ∷ * → * 、つまりブラケットの引数にはkind *必要であり、 Maybe * → * 、つまりMaybeも関数であり、引数Int ∷ *指定する必要があるため、 Maybe Int ∷ * get Maybe Int ∷ *を取得し、既にブラケットに渡すことができます： [Maybe Int] ∷ * 。 この種の制御には、カインドが存在します。