パラメトリック多相と型コンストラクタ

前回の記事で

これを書いていて「あれ、多相って関数だけじゃなくて型に対しても使う？型コンストラクタってそれ自体が多相？」とふと疑問を抱いた。この点に関しても別の記事で書きたいが、現在の自分のスタンスとしては、特殊な例を除いて「パラメトリック多相」というのは多相関数を許容する型システムのことで、型コンストラクタの存在は付随的かつ不十分だと考えている

と書いたので、その詳細。

そもそもパラメトリック多相と型コンストラクタを関連付けて考えてる人がいるのか？

このような疑問を持つ人もいるかと思うので、Wikipediaのポリモーフィズムの項を引用：

ja.wikipedia.org

パラメトリック多相（parametric polymorphism）- 詳細化されていない型要素を内包する抽象的な型に記号表現を提供する。ジェネリクスや関数型言語の型構築子など。

なんと関数については何も触れられていない。

私もTaPLを読むまではパラメトリック多相の例としてはlength :: [a] -> Intとかhead :: [a] -> aとかfilter :: (a -> Bool) -> [a] -> aのような関数をイメージしていた。もちろんこれらもパラメトリック多相なのだが、イメージとしては型コンストラクタ関連の関数ばかりを念頭に置いていたわけだ。

しかしここ数日でよく考えると、型コンストラクタとパラメトリック多相は（互いに存在すると便利ではあるが）直交な概念・言語特性ではないかと思うようになった。

型コンストラクタと関係ないパラメトリック多相関数

TaPLではパラメトリック多相に関して

Parametric polymorphism ... allows a single piece of code to be typed "generically", using variables in place of actual types, and then instantiated with particular types as needed. Parametric definitions are uniform: all of their instances behave the same

とある。"a single piece of code"というのはなんだか微妙な物言いだが、これだけ読むと「型コンストラクタ」も定義に含まれてもよさそうだ。

しかし実例を読むと、基本的には「さまざまな型に対して同一に作用できる関数」の話ばかり出てくる。その中にはlistなどの型コンストラクタを使うものもあるのだが、基本的に型コンストラクタが出てこなくてもパラメトリック多相な関数は書ける。

例としては：

id :: a -> a
id x = x

や

double :: (a -> a) -> a -> a
double f a = f (f a)

のような関数である。

つまり型コンストラクタが存在しなくてもパラメトリック多相な型システムはありえる。

型コンストラクタがあってもパラメトリック多相とは呼ばれないケース

型コンストラクタの存在は型システムがパラメトリック多相である必要条件ではないことが確認できた。しかし、もしかすると十分条件だろうか？

つまり型コンストラクタが存在するような型システムは必ず多相的だと言えるのか？

答えはノーである。何故ならば関数の型を構成する->がまさに「なんらかの型をとって別の型を返す」型コンストラクタそのものだからだ。

単純型付きラムダ計算の根本的な要素である「関数型」自体が型コンストラクタなので、型コンストラクタの存在が型システムが多相的であるという十分条件にしてしまうと、多相の概念が広がりすぎて無意味になってしまう。パラメトリック多相はあくまで単純型付きラムダ計算の拡張としての概念であるべきだろう。

また、->以外でもPairやTupleなどの単純型付きラムダ計算に対する拡張は型コンストラクタではあっても、導入することで型システムが多相になるとは言わない。このことも型コンストラクタとパラメトリック多相の直交性を示していると思う。

結論

というわけで型コンストラクタの存在は型システムがパラメトリック多相的であるかどうかとは直交した概念だと言える。

ただし、ユーザ定義可能な型コンストラクタの存在はパラメトリック多相と相性が非常にいいのは確かである。「要素の型に関わらずlistなら何でも受け入れる関数」などは型コンストラクタとパラメトリック多相の両方が存在してはじめて可能になる。

追記：

よく考えると「パラメトリック多相な関数」どころか「型のあるラムダ計算におけるいかなる関数」の存在する条件として型コンストラクタ->が必要、という見方もできるな・・・　ラムダ計算の定義の中に型コンストラクタがあるわけで、やはりパラメトリック多相と関係ないと言ってしまっていいとは思うが。