型族とは型の族のこと
型族のdocsを読んでると、新出単語がたくさん出てきて大変だが、数学用語と併せて見れば理解しやすい 以下、「Type Family」と呼んだり、「型族」と呼んだりすることがあるが同じものを指すmrsekut.icon
Type Family周辺の用語
初見でここだけ見てもわからないと思うので、そのときはこの節をスルーすると良いmrsekut.icon
ここだけ見て理解できるならこのノートの存在意義があまりない
「型の集合」を表す型コンストラクタ
型コンストラクタのことだが、型族を構成するものなので「型族コンストラクタ」とも言えるmrsekut.icon
Type Familyの別の言い方
Type Familyと全く同じものを指す
日本語で言えば「添字付けられた型族」となる
docs内では、「indexed type family、別名type familyは~~である」みたいな書き方をされている
型パラメータ
日本語で言えば「型添字」
ちなみに複数形は2種類ある
type indices
type indexes
docs内では前者が使われているmrsekut.icon
具体的な定義と併せて見る
ここから拝借して以下のようなType Familyの定義を考える 若干表記を変えているが、例としての意味は同じである
code:hs
type family List x where
List () = Int
List Bool = (Int, Integer)
書いたあとでミスったなと思ったが、
このノート内に登場するListは自作した型族のことであって、
GHC.Typesで提供されるList == []のやつとは全く別の概念であることに注意mrsekut.icon
紛らわしいので別の名前を用いれば良かったmrsekut.icon
上の用語との対応はこうなる
https://gyazo.com/ba5e0c2460d86c2c30c542d1e9946300
Type Familyと数学用語の照らし合わせ
上の話を数学における族や添字集合などと照らし合わせる 添字集合の簡単な例として、以下のようなテンプレで表現できる
添字集合$ I=\{1,2,\dots n\}があったとき
$ \{O_i\}_{i\in I}は有限個の開集合$ \{O_1, O_2,O_3,\dots,O_n\}のことを表す
また、こういう集合$ \{O_i\}_{i\in I}のことを族と言う これを上の例で言うなら
添字集合I = {(), Bool, Double}があったとき
$ \{\mathrm{List}_i\}_{i\in I}は集合{Int, (Int, Integer), [Double]}のことを表す
また、こういう集合$ \{\mathrm{List}_i\}_{i\in I}のことを族と言う
こうやって照らし合わせて見ると、このListがなぜ「型族」と言われるのかが理解できるmrsekut.icon
別の具体例
こういう型族Addを考える
code:hs
{-# LANGUAGE DataKinds #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE UndecidableInstances #-} data Nat = Zero | Succ Nat
type family Add n m where
Add 'Zero n = n
Add ('Succ n) m = Add n ('Succ m)
先程のListとの大きな違いは、再帰的に定義されている点である
Listの場合はtype indexが3種類しかなかったが、こちらの場合は無限個ある
こんな具合にAddから無限に型を生成できる
code:hs
type A0 = Add Zero Zero
type A1 = Add Zero (Succ Zero)
type A1' = Add (Succ Zero) Zero
type A3 = Add (Succ (Succ Zero)) (Succ Zero)
..
つまり、無限個のtype indexと、無限個の元が存在する