TypeFamilyを型レベル関数として見る
Type Familyは型の族ではあるが、型レベルの関数と解釈することもできる
「関数」として見ることで、全域なのかどうかや、単射なのかどうかなどが重要になってくる
型族とは型の族のことで使った2つの型族を例に話をすすめる
hstype family List x where
List () = Int
List Bool = (Int, Integer)
List Double = [Double]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 == [] のやつとは全く別の概念であることに注意TypeFamilyを「型レベル関数」と見ることもできる
引数が型で、戻り値が型であるような型のことを「型レベル関数」と言っているわけだが、
(型族ではない通常の)genericな型
Maybe a なども型レベル関数であるので、「型族とは型レベル関数のことである」と言うのは正しいが、かなり雑な説明である
通常の「
Maybe a のような型レベル関数」と、「型族のような型レベル関数」の違いはなにかそれはパラメトリック多相な関数と、Ad Hoc多相な関数の違いに似ている
雑に言えば前者はgenericsのことで、後者はoverloadのことである
対応
| 似てる | 今回の例 | |
| 通常のパラメータ化された型コンストラクタ | パラメトリック多相関数(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] になったりと、別の型になりうるとは言え、型族を以下のように定義をすれば、パラメトリック多相関数と同じものになる
無限にこう定義するとか(無理だが)
hstype family Maybe' x where
Maybe' Int = Maybe' Int
Maybe' String = Maybe' String
...こうとか
hstype family Maybe' x where
Maybe' a = Maybe' aと書いた場合、以下と同じ意味になる
hstype Maybe' a = Maybe' aこの場合、type familyで定義する理由は全く無い
寧ろ、プログラムの読者に無駄な意図を与えてしまう
単射かどうか
型関数として見た場合の差異として単射かどうかがある
Maybe のような通常の型関数の場合、これは単射であるhsdata Maybe a = Nothing | Just aつまり、
Maybe a ~ Maybe b ならば a ~ b であるというかまあ全単射だよね
List などの型族な型関数の場合、これは単射で無くても良い例えば以下のような定義もできうる
hstype 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 ならば全て定義されているこれは全域関数の性質である