TypeFamilyを型レベル関数として見る
Type Familyは型の族ではあるが、型レベルの関数と解釈することもできる
「関数」として見ることで、全域なのかどうかや、単射なのかどうかなどが重要になってくる
型族とは型の族のことで使った2つの型族を例に話をすすめる
code:hs
type family List x where
List () = Int
List Bool = (Int, Integer)
List Double = Double
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は自作した型族のことであって
GHC.Typesで提供されるList == []のやつとは全く別の概念であることに注意mrsekut.icon
TypeFamilyを「型レベル関数」と見ることもできる
引数が型で、戻り値が型であるような型のことを「型レベル関数」と言っているわけだが、
(型族ではない通常の)genericな型Maybe aなども型レベル関数であるので、
「型族とは型レベル関数のことである」と言うのは正しいが、かなり雑な説明である
通常の「Maybe aのような型レベル関数」と、「型族のような型レベル関数」の違いはなにか
それはパラメトリック多相な関数と、Ad Hoc多相な関数の違いに似ている
雑に言えば前者はgenericsのことで、後者はoverloadのことである
table: 対応
似てる 今回の例
通常のパラメータ化された型コンストラクタ パラメトリック多相関数(generics) Maybe型
型族コンストラクタ アドホック多相関数(overlaod) List型族
前者の方は、例としてMaybe aなどがあるが、
aに任意の型Hogeを代入することで、Maybe Hogeという型が作られる
型表記っぽく書くとMaybe :: a -> Maybe a
これは単一の型の実装Maybe _が、複数の引数に対応していることを表す
つまり、全ての型aに対して同じデータ表現を示す
後者の方は、例として上で定義したようなListがあるが、
() -> IntだとかBool -> (Int, Integer)だとかで定義される異なる型関数を、
Listという同じ名前で呼んでいる
つまり、雑に言えば、
前者の型関数Maybeの返り値は、必ずMaybe型となるが、
後者の型関数Listの返り値は、Intになったり、[Double]になったりと、別の型になりうる
とは言え、型族を以下のように定義をすれば、パラメトリック多相関数と同じものになる
無限にこう定義するとか(無理だが)
code:hs
type family Maybe' x where
Maybe' Int = Maybe' Int
Maybe' String = Maybe' String
...
こうとか
code:hs
type family Maybe' x where
Maybe' a = Maybe' a
と書いた場合、以下と同じ意味になる
code:hs
type Maybe' a = Maybe' a
この場合、type familyで定義する理由は全く無い
寧ろ、プログラムの読者に無駄な意図を与えてしまう
適切な抽象度の道具を使って意図を明示する
単射かどうか
型関数として見た場合の差異として単射かどうかがある
Maybeのような通常の型関数の場合、これは単射である
code:hs
data Maybe a = Nothing | Just a
つまり、Maybe a ~ Maybe bならばa ~ bである
というかまあ全単射だよねmrsekut.icon
Listなどの型族な型関数の場合、これは単射で無くても良い
例えば以下のような定義もできうる
code:hs
type instance List Int = Bool
type instance List Char = Bool
つまり、List a ~ List bであってもa ~ bとは限らない
全域関数か部分関数か
型関数として見た場合にListとAddの差異はどこにあるか
Listは、3つのtype indexを持っていて、
Addは、無限個のtype indexを持っていた
この関係を関数として見ると、
Listは、部分関数* -> *であり、
Addは、全域関数Nat -> Nat -> Natである
つまり、
Listの引数は「kindが*な型」だが、「kindが*何でも良い」わけではない
実際、List Stringもkind的にはokなはずだが、未定義なためerrorになる
これは部分関数の性質である
Addの引数は「kindがNatな型であり、kindがNatならば全て定義されている
これは全域関数の性質である