型付け

提供: langdev
移動: 案内検索

構造的部分型のための型推論できる型システム[編集]

RC型システム[編集]

Jonathan Eifrig, Scott Smith, and Valery Trifonov, Sound polymorphic type inference for objects

Tian Zhao, Polymorphic type inference for scripting languages with object extensions

Recursively constrained type system.

古典的な型と、その中の型変数に対する制約(「型変数αはβの部分型である」など)の集合の組として型を表す型システム。制約は再帰的でもよい。

型の和や積や再帰型を表現できる。レコードを作った後にフィールドを追加できる。型は巨大で読み書きしづらくなり、エラーメッセージも複雑になる。関数にエラーがある場合でも定義した時点では検出されず、使おうとしたところでどうやってもエラーになるという形でエラーがわかる場合がある。

多相型レコード計算[編集]

レコード多相性の理論

Atsushi Ohori, A Polymorphic Record Calculus and Its Compilation

型変数がレコード種(record kind)で制約されている。ML風のlet多相性を自然に拡張して型推論できる。

レコードは単相であるが、レコードを引数に取る関数が多相的である。例えば、λr. (r.x + 1)という関数(rを受けとり、そのフィールドxに1を足した値を返す)は∀σ::{{x: int}}. σ → intという型(int型のフィールドxを持つ任意のレコード型σを受け取りintを返す関数)を持つ。

レコードを配列としてコンパイルでき、コンパイル時に計算されたインデックスで配列にアクセスするだけでフィールドにアクセスできるので効率が良い。

レコードを作った後にフィールドを追加できない。

後述するRow型変数と異なり、λf. (f {a: 1, b: 1}) + (f {a: 1, c: 1})という式は二階多相性を導入しないと型付けできない。

SML#では、一階多相性を持つ多相型レコード計算が使われている。

Row型変数[編集]

Didier Rémy, Type inference for records in natural extension of ML

無限個の未知のフィールドを表すRow変数を使う方式。ML風のlet多相性を自然に拡張して型推論できる。

レコードは多相である。例えば{name: "foo"; age: 1}という式は{name: 'u.string; age: 'v.num; abs.α}という型を持つ。これはnameというstring型のフィールドを持つレコードとしても持たないレコードとしても扱えるし、ageについても同様だが、それ以外のフィールドについては存在しないものとしてしか扱えない、という意味である。'u'vpre(フィールドが存在する)かabs(フィールドが存在しない)という状態を代入できる変数で、αはそれ以外のフィールドを表すRow変数である。一方、λr. (r.x + 1)という関数は{x: pre.num; ψ} → numという型(num型のフィールドxを持ち、それ以外についてはなんでもよいレコードを受け取り、numを返す関数)を持つ。

レコードを作った後にフィールドを追加できる。

λf. (f {a: 1, b: 1}) + (f {a: 1, c: 1})という式は({a: 'u.num; b: abs.num; c: abs.num; abs.α} → num) → numという型を持つ。つまり、この関数にfとして渡す関数はnum型のフィールドaを要求してもしなくてもよいが、bやcやその他のフィールドを要求してはならないという制約を表す。型システムの都合上、bやcは存在しないがnum型であるという奇妙な型になっている。

レコードの存在を明示的に忘れる演算子が必要となる場合がある。

OCamlではRow変数を使っている。ただし、上の論文のよりは単純なものを採用している。

型クラス[編集]

型族[編集]

GADTs[編集]

OutsideIn(X)[編集]

http://research.microsoft.com/~simonpj/papers/constraints/jfp-outsidein.pdf

GADTs、型クラス、型族をサポートする型推論アルゴリズム

一意性型と線形型[編集]

Erik Barendsen and Sjaak Smetsers. 1993. Conventional and Uniqueness Typing in Graph Rewrite Systems. In Proceedings of the 13th Conference on Foundations of Software Technology and Theoretical Computer Science, R. K. Shyamasundar (Ed.). Springer-Verlag, London, UK, UK, 41-51.

Edsko Vries, Rinus Plasmeijer, and David M. Abrahamson. 2008. Uniqueness Typing Simplified. In Implementation and Application of Functional Languages, Olaf Chitil, Zoltán Horváth, and Viktória Zsók (Eds.). Lecture Notes In Computer Science, Vol. 5083. Springer-Verlag, Berlin, Heidelberg 201-218. DOI=10.1007/978-3-540-85373-2_12 http://dx.doi.org/10.1007/978-3-540-85373-2_12

一意性型は、ある値に対する参照が1つしかないという性質を保障する。一方、線形型は値がちょうど1回のみ使われるという性質を保障する。これによりガベコレが不要になったり、純粋関数型言語で安全に破壊的更新や入出力ができるようになったり、ファイルの閉じ忘れを防止したりできる。線形型は線形論理に基く。

一意性型を採用した言語としてはCleanMercuryがある。