Erlangの型システムを定式化してみる - 檜山正幸のキマイラ飼育記 (はてなBlog)

Erlangの型記法（type notation）は、言語仕様の外にある規約に過ぎません。しかし、型変数や型構成子が自由に使えるとなると、形式的に割ときれいな型システムを作れそうです。

実際にやってみます。Erlangの型システムを定式化してみます。ここで、型システムとは、型の表現（type expression）に関する構文論と意味論のことだと考えます。次の2つを目標とします。

現状使われている非形式的な型表記（type notation）構文をできるだけ尊重する。
形式的にある程度満足できる定式化を提供する。

内容：

型表現の構文
いろいろな型関数
型演算子
型変数と型環境
新しい型関数の定義
局所的な型束縛
開いた型表現の解釈
圏論的な意味論
まとめ（になってない）

●型表現の構文

型表現（type expression）は、型定数、型関数、型演算子を組み合わせたものです。が、型定数は型関数の特殊なものだし、型演算子は型関数の略記に過ぎません。つまり、本質的には型関数だけしかないのです。

その型関数は、名前と項数（アリティ；引数の個数）を持ちます。ただし名前は英小文字で始まると約束します。Erlangの普通の記法を借りれば、integer/0、list/1、cons/2 などと表現できますね。項数が0の型関数を特に型定数と呼ぶことにします。

一般的な型表現は：

型定数（項数0の型関数）は型表現である。
「名前(型表現1, ..., 型表現N)」の形は型表現である。ただし、「名前」は項数がNの型関数の名前。

と、帰納的（inductive）に定義します。

次は型表現の例です。（次の節以降で詳しく説明します。）

integer()
list(integer())
cons(integer(), list(string()))
cons(integer(), list(list(char())))

●いろいろな型関数

Erlangの基本的な型に対応する型定数（項数0の型関数）は次のものです。

atom(), binary(), float(), function(), integer(), pid(), port(), reference()

bool(), char(), nil(), any(), none()も事前に定義された型定数に入れておきます（「Erlangの型記法（Type Notation）」を参照）。

引数を1個以上取る型関数は、型構成子（type constructor, type composing operator）と呼ばれるものです。総称型とかパラメータ付き型とも呼ばれますね。いろいろな呼び名があっても、本質的にはみんな同じです。

さて、Erlangの型構成子ですが：

list(T) -- 項目の型がTであるリストの型。
cons(S, T) -- 先頭項目の型がS、残りの部分の型がSであるリストの型。あるいは同じことだが、左枝の型がS、右枝の型がTである二分木（二進木）の型。
tuple2(S, T) -- 第1項目の型がS、第2項目の型がSである2項タプルの型。
tupleN(T₁, ..., T_N) -- tuple2の一般化。N項タプルの型。N = 0, N = 1 の場合も考える。
function1(S, T) -- 引数の型がS、戻り値の型がTである1引数関数の型。
functionN(S₁, ..., S_N, T) -- function1の一般化。N個の引数の型がそれぞれS₁、…、S_N、戻り値の型がTであるN引数関数の型。N = 0 の場合も考える。
union(S, T) -- 型Sと型Tのユニオン（選択、バリアント）型。

tuple1, tuple2, ... などはまとめて可変引数のtupleとすればよさそうですが、tuple() が「すべてのタプル」の意味で既に使われています。同じ（functionが既に使われている）理由で、function1, function2, ... などを使います。ちなみに、tuple0() は空タプル{}だけからなる型、function0(T)は“型Tの定数（項数0の関数）”の型です。

●型演算子

前節の型構成子には、演算子／パターンによる略記法が用意されています。

list(T) は [T]
cons(S, T) は残念ながら略記できません。パターン [S|T] を使いたいところですが、角括弧はlist、縦棒はunion演算子に使われているので。
tuple2(S, T) は {S, T}
tupleN(T₁, ..., T_N) は {T₁, ..., T_N}
function1(S, T) は (S) -> T
functionN(S₁, ..., S_N, T) は (S₁, ..., S_N) -> T
union(S, T) は S | T

型演算子を使うと型表現を短く書けます。現状の型記法では、演算子の優先度が曖昧なようです。EDocでは、「->」演算子の優先度が「|」演算子より強いので、(string()) -> integer() | error() は ((string()) -> integer()) | error() の意味になります。manページのドキュメンテーションでは、(string()) -> (integer() | error()) と解釈します。ここでは、EDocの方式に従います。

また、「|」演算子は本来2項演算子ですが、結合律を前提として S | T | U のような書き方も許すことにします。

●型変数と型環境

通常の変数が値により具体化されるのと同様に、型変数は型により具体化されるプレイスホルダーです。構文的には、型変数に大文字で始まる名前を使います。確実に型関数と区別がつきますよ。

型変数を含んだ型表現の例：

list(Item)
cons(atom(), [Other])
[{Key, Value}]
nil() | cons(X, list(Y))
() -> (string() | {error, Reason})
((integer() -> Y), integer(), integer()) -> Y

型変数を含んだ型表現は、そのままでは具体的な型を表しません。そこで、型変数と具体的な型を結びつけたマップを考えます。例えば、{Key => atom(), Value => string()} は、型変数Keyの“値”がatom()で、型変数Valueの“値”がstring()であることを示します。このような「型変数 => 具体的な型」という束縛の集まりを型環境と呼びます。

通常の変数が入った式（expression）が、環境（束縛）のなかで値に評価されるのと同様に、型表現（type expression）は型環境のなかで具体的な型に評価されます。

●新しい型関数の定義

型変数を含む型表現を使うと、既にある型関数から新しい型関数を定義することができます。やってみましょうか。



 pair(S, T) = {S, T}

 list_of_pairs(S, T) = list(pair(S, T))

 vector_2d(Scalar) = {vector, Scalar, Scalar}

もちろん、型変数がなくてもかまいません。Erlangでよく使われる型定数（引数が0個の型関数）も次のように定義できます。



 term() = any()

 number() = integer() | float()

 iolist() = [char() | binary() | iolist()]

 string() = [char()]

 deep_string()= [char() | deep_string()]

iolist(), deep_string() は再帰的定義を使っています。再帰的定義を使えば、list(X) も nil()とcons(S, T)から定義できます。



 list(X) = nil() | cons(X, list(X))

現在の慣例では、tuple() はすべてのタプルからなる型です。これは次のように表現できます。



 tuple() = tuple0() | tuple1(any()) | tuple2(any(), any()) | ...

list(X)やtuple()の定義を見てクリーネ・スターを思い起こす人もいるでしょう。

すべての関数を表すfunction()なら次のようになります。



 function() = function0(any()) | function1(any(), any()) | ...

●局所的な型束縛

式と環境を一緒にしたのがクロージャ（「結局、クロージャって」参照）でした。そうであるなら、型表現と型環境を一緒にしたものは型クロージャとでも呼ぶべきでしょう。ここでは、型クロージャに相当するものを再び型表現と考えることにします。普通の言葉使いだと let式とかwhere式とかいうヤツです。

キーワードはwhereを使うことにして、例を挙げます。



 {Key, Value}

   where Key = atom(), Value = string()

これは {atom(), string()} と同じです。

whereの後ろには型変数の束縛（具体化）を書きましたが、型関数の束縛（つまり、型関数定義）を書いてもかまいません。



 list(pair(Key, Value))

   where

     pair(S, T) = {S, T},

     Key = atom(), 

     Value = string()

whereを含んだ式を型関数定義の右辺（ボディ）に使ってもよいので、次の書き方もできます。



 list_of_pairs(Key, Value) =

   list(pair(Key, Value)) where pair(S, T) = {S, T}

whereの後に書かれた束縛（型変数、型関数の定義）は局所的なものです。つまり、whereの前にある型表現の解釈に使われるだけで、それより広いスコープは持ちません。

●開いた型表現の解釈

束縛されていない型変数を含む型表現を開いた型表現と呼ぶことにします。例えば、list({atom(), X, Y}) は型変数X, Yを持つので開いた型表現です。でも、list({atom(), X, Y}) where X = integer(), Y = string() は開いてません（閉じてます）、X, Yが束縛されているから。

閉じた型表現の解釈はハッキリしてますが、開いた型表現はどう解釈すべきでしょう。「解釈しない」というのがひとつの答ですが、それじゃつまらないので次のようにします。

開いた型表現に出現する型変数をアルファベット順に並べる。
上の手順で得られたリストを型変数リストとして、typefunc(型変数リスト) = 型表現 という型関数定義を考える。
型関数typefuncをもとの型表現の“意味”と考える。

アルファベット順に並べるあたりがイイカゲンそうですが、この解釈はけっこううまく働きます。つまり、開いた型表現は、束縛されてない型変数を型パラメータとする総称型とみなすことになります。

●圏論的な意味論

僕の好みから言えば、型関数や型表現の解釈には圏論を使うことになります（当然！）。しかしここで、カテゴリカル・セマンティクスを真面目にやるんは面倒なので、雰囲気だけ急ぎ足で。

引数をN個持つ型関数、または束縛されてない（自由な）型変数をN個持つ型表現は、C^N→C という関手になります。ここで、Cは適当なデカルト閉圏です。だいたいの感じを次の表に示します。

型表現	圏論の対応物
型定数	1→C という関手
型定数の領域	関手による単一対象の“値”
1引数型関数	C→C という自己関手
2引数型関数	C×C→C という2項関手（双関手）

ここで、1は単一対象単一射の自明圏です。自明圏からの関手とは、圏Cの対象と同じことです。list(X)は1引数型関数なので、自己関手に対応しますが、これはモナドですね。{X, Y}、(X)->Y、X | Y はどれも2引数型関数ですから、双関手に対応しますが、それぞれ直積、指数、直和とみなせます。

総称型のあいだの総称関数、例えば、終対象term : X→nil() や射影proj1 : {X, Y}→X は自然変換になります。実際のプログラムでは、自然性を満たさないこともありますが、タチの良い総称関数はたいてい自然です。

●まとめ（になってない）

Erlangのデータと型システムはかなり素朴なので、"types as sets"の流儀でだいたい解釈できます。まっ、リストとタプルの違いを説明したりするには、もっと代数的構造が必要ですけどね。型階層は真面目に考えなかったんですが、集合の包含みたいなもんで済むんじゃなかろうか（よく分からんが）。

型関数（型構成子、総称型）を関手だと思う立場を徹底しようとすると、関手に対するラムダ計算が必要になって、そのモデルは“圏の圏”のデカルト閉構造を使ったりするんだと思うけど、それもよくは分かりませーん。気が向いたときに考えます。