GHC 拡張を使って直積っぽい型の表記とかしてみる

型族とかよくわからないから少し勉強した．
※ GHC 7.8.1 から追加された機能を用いています．

直積

二つの集合 $A$, $B$ に対し，

A \times B = \{(a, b) \mid a \in A, b \in B\}

によって定義される集合を直積 (デカルト積，カルテシアン積) という．

例えば $ A = \{ 1, 2 \} $, $ B = \{ a, b, c \} $ とすると
$ A \times B = \{ (1, a), (1, b), (1, c), (2, a), (2, b), (2, c) \}$ となる．要するに，二つの集合から一つずつ要素をとってきて作ったペア (順序対)¹ の集まりである．

ところで Haskell の型は集合と考えられる (Integer は整数の集合，Char は文字の集合とか) ．Haskell には順序対をタプルで表せるから，例えば $ Integer \times Char $ は (Integer, Char) のように表せる．

ということで次のようなことができるはずである．

type a >< b = (a, b)

test1 :: Integer >< Char
test1 = (10, 'a')

しかしこれはコンパイルが通らない．演算子チックな型²や型シノニムをつくる場合は TypeOperators 拡張が必要である．

{-# LANGUAGE TypeOperators #-}

type a >< b = (a, b)

test1 :: Integer >< Char
test1 = (10, 'a')

test2 :: String >< String -> String
test2 (x, y) = x ++ y

三つの集合の直積

三つの集合に対しての直積も同様に定義される．

A \times B \times C = \{ (a, b, c) \mid a \in A, b \in B, c \in C \}

だがちょっと待ってほしい．二つの集合の直積の定義から考えると， $A \times B$ を先に計算すると

(A \times B) \times C = \{ ((a, b), c) \mid a \in A, b \in B, c \in C \}

となり，$B \times C$ を先に計算すると

A \times (B \times C) = \{ (a, (b, c)) \mid a \in A, b \in B, c \in C \}

となることが考えられないだろうか．

実際，次のコードはコンパイルを通る．

{-# LANGUAGE TypeOperators #-}

type a >< b = (a, b)

test3 :: (Integer >< Char) >< String
test3 = ((10, 'a'), "Hello")

test4 :: Integer >< (Char >< String)
test4 = (10, ('a', "Hello"))

また，単に Integer >< Char >< String と書くと (Integer >< Char) >< String のように前から結合されて解釈される．

{-# LANGUAGE TypeOperators #-}

type a >< b = (a, b)

test5 :: Integer >< Char >< String
test5 = ((10, 'a'), "Hello")

しかし，集合論では $(a, b, c)$ の定義を $((a, b), c)$ や $(a, (b, c))$ としたり，これらを同一視して扱うことが多い．そのため，

A \times B \times C = (A \times B) \times C = A \times (B \times C) =  \{ (a, b, c) \mid a \in A, b \in B, c \in C \}

という定義で問題ない (ということにしておく)．

さて，Haskell でもこの定義に倣って Integer >< Char >< String が (Integer, Char, String) を表すようにしたい．しかし，先ほどの挙動から考えて type でどうにかなりそうな感じではない．そこで，型族 (Type Families) という GHC 拡張を導入する．

型族 (Type Families)

型族は，簡単に言うと型レベル函数，つまり型を返す"函数のようなもの"である．

例えば通常の函数は「Int 型の数値をとって 2 倍して返す」とか「Double 型のリストをとって String に変換して返す」とかであるのに対して，型族を使うと「Int 型をとって Double 型を返す」のようなことが出来る．

簡単な例

{-# LANGUAGE TypeFamilies #-}

type family Test1 t :: *
type instance Test1 Int = Double

まず，型族を使うには TypeFamilies 拡張が必要である．

上のコードでは，Test1 という型族を定義した．(型族の名前は大文字で始めなければならない．) 一行目の type family Test1 t :: * は，函数における函数宣言のようなもの (型族宣言) であり，二行目の type instance Test1 Int = Double が本体のようなもの (型インスタンス宣言) である．

一行目はとりあえずおいておいて，二行目を見てみると Test1 は引数 Int をとり Double を返しているように見える．

実際，次のようなコードが書ける．

{-# LANGUAGE TypeFamilies #-}

type family Test1 t :: *
type instance Test1 Int = Double

test6 :: Double
test6 = 3.14159

test7 :: Test1 Int
test7 = 2.71828

{- コンパイルエラー
test8 :: Test1 Char
test8 = False
-}

Test1 自体は型ではないが，Int をとることで Double という型になっている．
しかしもちろん Test1 に Int 以外のものを与えるとエラーとなる．

Test1 が Char を取ることを許したければ，Test1 Char に対する実装をしてあげればよい．

{-# LANGUAGE TypeFamilies #-}

type family Test1 t :: *
type instance Test1 Int = Double
type instance Test1 Char = Bool

test6 :: Double
test6 = 3.14159

test7 :: Test1 Int
test7 = 2.71828

test8 :: Test1 Char
test8 = False

さて，このままでは全くつまらない．例えば思いつくのは，多相的にすることである．

{-# LANGUAGE TypeFamilies #-}

type family Test2 t :: *
type instance Test2 a = String

test9 :: Test2 Double
test9 = "2.71828"

test10 :: Test2 Char
test10 = "a"

test11 :: Test2 [Bool]
test11 = "Boolean list."

Test2 は a という型をとっているが，この a にどんな型でもつっこめるらしいことがわかる．

次のようなこともできる．

{-# LANGUAGE TypeFamilies #-}

type family Test3 t :: *
type instance Test3 a = [a]

test12 :: Test3 Double
test12 = [0.0, 0.3010, 0.4771, 0.6021]

test13 :: Test3 Char
test13 = "Hi."

しかし残念ながら，次のようなことはできない．

{-# LANGUAGE TypeFamilies #-}

type family Test4 t :: *
type instance Test4 Int = Double
type instance Test4 Char = Bool
type instance Test4 a = a

このコードはコンパイルエラーとなる．
これは函数のパターンマッチのようにはいかない．型族のインスタンス宣言では，型引数 ( 上の例だと a) を適当に替えたとき他のインスタンス宣言とぶつかってしまうことがあってはならない³．(パターンマッチのように，上から順次見ていくということはしない．)

例えば上の例では，type instance Test4 a において a が Int または Char のとき，type instance Test4 Int, type instance Test4 Char と宣言がぶつかってしまうのでダメである．

次のコードも同様の理由でコンパイルエラーとなる．

{-# LANGUAGE TypeFamilies #-}

type family Test5 t :: *
type instance Test5 (a, a) = [a]
type instance Test5 a = a

しかし，次のコードはコンパイルを通る．a に何を入れても宣言がぶつからないためである．

{-# LANGUAGE TypeFamilies #-}

type family Test6 t :: *
type instance Test6 Int = Int
type instance Test6 [a] = a

複数の型を受け取る

今までのコードでは型族は一つしか型を受けとらなかった．しかし，受け取る型の数は一つに限らない．
例えば型を二つ受け取りたい場合次のように記述する．

{-# LANGUAGE TypeFamilies #-}

type family Test7 s t :: *
type instance Test7 Int Int = Int
type instance Test7 Int Double = Char
type instance Test7 Double a = Double

test14 :: Test7 Int Double
test14 = '1'

test15 :: Test7 Double Int
test15 = 1.5

さらに多くなっても同様である．

{-# LANGUAGE TypeFamilies #-}

type family Test8 s t u :: *
type instance Test8 a b c = (a, b, [c])

test16 :: Test8 Int Double Char
test16 = (100, 0.5, "AH^~ My heart will be hopping^~")

逆に次のように一つも型を受け取らないこともできる．

{-# LANGUAGE TypeFamilies #-}

type family Test9 :: *
type instance Test9 = Bool

test17 :: Test9 -> String
test17 True = "Ja."
test17 _    = "Nej."

カインド

型族宣言中に登場する * はカインドである．(あとでかく)

閉じた型族 (Closed Type Families)

型族は函数のようなパターンマッチングはできなかったが，実は閉じた型族 (Closed Type Families) を用いるとパターンマッチングを行うことができる．

Closed Type Families は，type instance の代わりに where を用いて次のように記述する．

{-# LANGUAGE TypeFamilies #-}

type family Test10 t :: * where
  Test10 Int = Double
  Test10 Char = Bool
  Test10 a = a

test18 :: Test10 Int
test18 = -5

test19 :: Test10 Char
test19 = True

test20 :: Test10 (Maybe String)
test20 = Just "Nyaa"

先ほどと異なり，上のコードはコンパイルを通り，想定通り動く．

Closed Type Families では函数のパターンマッチと同様，上から順に合致するパターンを探す．そのため，type instance を用いて記述する場合 (開いた型族, Open Type Families) と比べて少し制約がある．

Open Type Families の場合は，型族のインスタンス宣言 (本体の定義) は離れた場所で行うことができる．極端な例を挙げれば，モジュールをまたがってもよい．

{-# LANGUAGE TypeFamilies #-}

type family Test11 t :: *

test21 :: Test11 Char
test21 = getChar

type instance Test11 Int = [Int]

test22 :: Test11 Double
test22 = Nothing

type instance Test11 Double = Maybe Double

test23 :: Test11 Int
test23 = [0..100]

type instance Test11 Char = IO Char

それに対して，Closed Type Families の場合は型族宣言と本体の定義が同じ場所で行われる必要がある．従って，次のようなコードはコンパイルエラーとなる．

{-# LANGUAGE TypeFamilies #-}

type family Test12 t :: * where
  Test12 Char = IO Char

test24 :: Test12 Char
test24 = getChar

  Test12 Int = [Int] -- コンパイルエラー

また次のように Open と Closed を混ぜるのもダメである．

{-# LANGUAGE TypeFamilies #-}

type family Test13 t :: * where
  Test13 Char = IO Char

test25 :: Test13 Char
test25 = getChar

type instance Test13 Int = [Int] -- コンパイルエラー

本題

では，型族を用いて (><) を書きなおしてみる．
とりあえず二つの集合の場合のみを考えた実装は次のようになる．

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}

type family s >< t :: * where
  a >< b = (a, b)
  
test26 :: Integer >< Char
test26 = (10, 'a')

test27 :: String >< String -> String
test27 (x, y) = x ++ y

この時点では type を用いた場合とほとんど同じであり，a >< b >< c は ((a, b), c) となってしまう．

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}

type family s >< t :: * where
  a >< b = (a, b)

test28 :: Integer >< Char >< String
test28 = ((10, 'a'), "Hello")

そこで，(><) の定義に次のように加える．

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}

type family s >< t :: * where
  a >< (b, c) = (a, b, c)
  (a, b) >< c = (a, b, c)
  a >< b = (a, b)

こうすることにより，$ A \times B \times C = (A \times B) \times C = A \times (B \times C) = \{ (a, b, c) \mid a \in A, b \in B, c \in C \} $ が実現できる．

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}

type family s >< t :: * where
  (a, b) >< c = (a, b, c)
  a >< (b, c) = (a, b, c)
  a >< b = (a, b)

test29 :: Integer >< Char >< String
test29 = (10, 'a', "Hello")

test30 :: (Integer >< Char) >< String
test30 = (10, 'a', "Hello")

test31 :: Integer >< (Char >< String)
test31 = (10, 'a', "Hello")

めでたしめでたし．

n 個の集合の直積

n 個の集合に対しての直積も同様に定義される．

X_1 \times X_2 \times \cdots \times X_n = \{ (x_1, x_2, \cdots , x_n) \mid x_1 \in X_1, x_2 \in X_2, \cdots , x_n \in X_n \}

たとえば 4 個の集合の積に対応するには，(><) の定義を以下のようにすればよい．

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}

type family s >< t :: * where
  (a, b, c) >< d = (a, b, c, d)
  (a, b) >< (c, d) = (a, b, c, d)
  a >< (b, c, d) = (a, b, c, d)
  (a, b) >< c = (a, b, c)
  a >< (b, c) = (a, b, c)
  a >< b = (a, b)

test32 :: Integer >< Char >< String >< Bool
test32 = (10, 'a', "Hello", True)

test33 :: (Integer >< Char) >< String >< Bool
test33 = (10, 'a', "Hello", True)

test34 :: (Integer >< Char >< String) >< Bool
test34 = (10, 'a', "Hello", True)

test35 :: Integer >< (Char >< String) >< Bool
test35 = (10, 'a', "Hello", True)

test36 :: Integer >< (Char >< String >< Bool)
test36 = (10, 'a', "Hello", True)

test37 :: Integer >< Char >< (String >< Bool)
test37 = (10, 'a', "Hello", True)

test38 :: (Integer >< Char) >< (String >< Bool)
test38 = (10, 'a', "Hello", True)

デカルト冪

気が向いたら書く

考察

今回の実装では掛ける集合の数が増えるほど (><) の定義を増やさなければならなかった．n 個の直積にジェネリックに対応させることもできるのかもしれないが ここに書くには余白が狭すぎる 勉強不足でそこまではできなかった．(知っている人がいたらコメントでこっそり教えてください ><)

参考

GHC 7.4.1 の型レベル新機能を使い倒す 〜GADTs、型族 と DataKinds、ConstraintKinds の円環〜 - これは圏です
7.7. 型の族
直積集合 - Wikipedia
GHC/Type families - HaskellWiki

斎藤 毅 著，「集合と位相」 (東京大学出版会) 2009

注釈

1. 順序対では $ (a, b) \neq (b, a) $ である．他に非順序対 $ \{ a, b \} $ があり，こちらは $ \{ a, b \} = \{ b, a \} $ ↩

2. 型演算子と呼ぶらしい． ↩

3. 特定の条件を満たしていればそのような重複が許されることがある．参考 → 7.7.2.3. 型シノニムインスタンスの重複 ↩