はじめに
前の記事でHaskellを使ってみました。
今回から、Haskellを使って圏論を学んでいきたいと思います。
初回の今回は、圏論の基本的な概念についてHaskellで実装してみます。
こちらのリポジトリに、コードをアップロードしています。
圏とは
圏とは、対象と射からなる数学的構造です。
対象とは、何らかの数学的対象のことです。
射とは、対象から対象への矢印です。
たとえば、集合を対象、写像を射とする圏があります。
Haskellでの実装
こちらを参考にしました。
あくまでも抽象的な定義が紹介されています。
圏と関手の定義はこんな感じになります。
-- 型クラスを使った圏の定義
class Category cat where
-- 恒等射。圏クラスのメソッド
id :: cat a a
-- 射の合成。圏クラスのメソッド
(.) :: cat b c -> cat a b -> cat a c
-- 関手の定義
class (Category c, Category d) => Functor c d f where
-- 関手の射に対する作用。関手クラスのメソッド
fmap :: c a b -> d (f a) (f b)
この後関手圏や自然変換を定義しようかと思ったのですが、ここで圏の定義に物足りなさを感じました。
というのも、関手圏を定義するならば対象が圏であることを考慮する必要があります。
しかし、上の定義では対象についての情報がありません。
確かに圏論の主要な概念は射ですが、その射を適切かつ具体的に定義するためには対象についての情報も必要だと思います。
圏の対象を扱う
こちらのページでは、より具体的な圏の定義がされています。
-- 対象：集合：型
data C = A | X | Y | Z deriving (Show, Eq)
-- 射：関数
f :: C -> C
f A = X
g :: C -> C
g A = Y
h :: C -> C
h X = Y
h' :: C -> C
h' Y = Z
-- 恒等射
idA :: C -> C
idA a = a
idX :: C -> C
idX x = x
idY :: C -> C
idY y = y
idZ :: C -> C
idZ z = z
-- 以下，恒等射にはデフォルトで搭載されているidを用いる．
-- 射の合成
--- 以下，===で同じという意味を表すことにする
-- テスト(h.f) A === 結果Y
-- 結合律
-- (h'.h.f) A === ((h'.h).f) A === (h'.(h.f)) A === Z
-- 可換かどうか
result1 = (h.f) A
result2 = g A
kakan = (result1 == result2) -- Trueなので可換 h.f=g
この定義での対象はA, X, Y, Zの4つの集合です。
射は関数として定義されています。
たしかに、この定義であれば、対象についての情報も扱うことができます。
しかしながら、関手圏との関係性を考えると、対象についての情報を型クラスで扱う方が適切かもしれません。
だいぶ長くなりそうなので、今回はここまでにします。