Arantium Maestum

プログラミング、囲碁、読書の話題

Haskellと圏論ノート：Haskと型と関数と関手

Haskell

Thinking Functionally with Haskellがすこし進んできたので、ちょっと今まで出てきた概念と関連するところまで圏論について調べてみた。まごうことなき私的勉強メモ。

圏Cは以下の三つの要素をあわせた概念：

  • Object（対象）の集まり
  • Cに含まれる対象間のmorphism（射）の集まり
  • 以下の公理が成り立つ、Cに含まれる射を合成する演算の存在
    • (f . g) . h = f . (g . h)　（結合律）
    • 恒等射idの合成に関して、f . id = f, id . g = g　（単位律）

Haskellの型と関数は圏Haskを成す：

  • 対象は型
  • 対象間の射は関数
  • 関数合成演算子.は結合律と単位律を満たす

疑問点としては

  • 関数の型(Int -> Bool)などはHaskのObjectなのか？違うのだと思うが、Haskellにおいて関数は第一級な存在ではないのか？
  • 型クラスはこの体系だとどういう扱いになるのか？（まあ特定の性質を持つ型の集合みたいなものだろう）
  • Haskに含まれる型というのは、あるプログラムで定義された型(preludeなどからimportしたものも含めて）のみなのか？それともHaskellという言語が扱い得る無限の型すべてが含まれるのか？
  • 対象間の射はmorphismやらmappingやらarrowやら別名が多く、Haskellだとarrowは別の意味を持つから云々とか言われると色々と思うところは多くなる。（無意味に難しくしてない？）
  • 律と則ってどう違うんだっけ？

といったところ。疑問があってもとりあえず進んで、理解が深くないと難しそうだったら手戻りを惜しまない、という戦略で続けることにする。

Functor（関手）とは、ある圏{C_1}から別の圏{C_2}への射。

  • {C_1}の対象Xを{C_2}の対象F(X)に対応させる
  • {C_1}の射f:X->Yを{C_2}の射F(f):F(X)->F(Y)に、以下の二つの公理が成り立つように対応させる。
    • F(id) = id
    • F(f) . F(g) = F(f . g)

HaskellにおけるFunctorは型変数を含んだ形で定義される型でfmapが正しく定義されているFunctor型。たとえばList:

  • a型を[a]型に対応づける（たとえばIntと[Int]）
  • 関数fと関数map f`を対応づける
  • map id = id
  • map f . map g = map (f . g)

思うところとしては

  • Functor型はHaskからHaskの部分集合（？）への射
  • Functor型によって形作られるHaskの部分集合は、例えばIntやInt -> Boolは含まないのでHaskの真部分集合である
  • Functor型によって形作られるHaskの部分集合は、すべてのHaskの型と関数に対して1対1の単射でありえる（そうでないこともある）。Listは単射
  • ということはListが存在する場合Haskの型と関数は少なくとも可算無限集合
  • Tupleが存在する場合は多分、非可算集合
  • List IntはHaskに含まれる型、ListはHaskの任意の型aをList aに対応させるFunctor。でもList aもHaskの型。

今のところは、概念はとりあえず納得できたけれども何の役に立つのかはいまいち実感がわかない。TFwHでモナドの話が出てくるのはけっこうあとのほう（たしか１０章）なので、気長にやっていくつもり。