型クラスを用いて部分構造型を表現する
型 Advent Calendar 2019 - Qiita 18日目の記事です。
前回の記事はuhyoさんの TypeScriptはgradual typingシステムか - Qiita でした。
本文はこちら（PDFです）
誤りなどありましたらご指摘ください。
線形ラムダ計算の型システムを実装してみた
はじめに
最近Advanced Topics in Types and Programming Language（ATTaPL）という本を読んでいるのですが、この本のはじめのSubstructural Type Systemの章で解説されているLinear Lambda Calculus（線形ラムダ計算）について、イマイチ理解が進まなかったので、せめて概形でも掴もうと思い、OCamlを使って型システムを実装してみたので、知識の整理も兼ねて今回は実装方法や線形型の仕組みについて簡単に説明していこうと思います。
線形型とは
線形型（linear type）とは、修飾された値が確実に一回のみ使用されることを保証する型です。この、確実に一回のみ使用されるという特性を活かして、メモリが確実に解放される事や、オープンしたファイルが確実にクローズされる事について、型を用いて静的に保証を与える事ができます。
ちなみに、似たような型として修飾した値が導入された順番で使用されていく事を保証するOrdered Typeや、最大で一回修飾した値が用いられる事を保証する（つまり用いられなくてもよい）Affine Typeなどがあります。
線形ラムダ計算の構文とcontainment rule
では、どのように"確実に一回のみ使用される事を保証する"ような型を実装するのでしょうか。これについては、まず線形ラムダ計算の構文を述べ、それに沿って解説する事にします。
線形ラムダ計算の構文は次のように定義されます。idは識別子を表しています。
q ::= lin | un
b ::= true | false
t ::= id
| q b
| if t then t else t （if文）
| q <t,t> （pair作成）
| split t as id,id in t （split構文）
| q λx:T.t （ラムダ抽象）
| t t （適用）
P ::= bool
| T * T
| T -> T
T ::= q P
ではまず、修飾子の定義（q）から解説します。
線形ラムダ計算では2つのlin（linear）、un（unrestricted）という修飾子を用いて、線形型で修飾されるか否かを区別します。
linで修飾された値は前述した使用回数に関する線形型の保証を受ける事ができます。unで修飾された値は使用回数に制限を受けません。
また、型レベルでも値に対応した修飾子が型に現れます、例えばlin trueと定義したならば、この項の型付けはlin boolとなります。
他に修飾子で解説しておかねばならないものに、containment ruleというものがあります。
これはunで修飾された型の中にlinで修飾された型は現れてはいけないと言うものです。
ここでは、ATTaPLでの例を引用してcontainment ruleの必要性について解説します。
例えば次のような関数discardがあるとします
let discard = lin λx:lin bool.
(lin λf:un (un bool -> lin bool).lin true) (un λy:un bool.x)
この関数discardでは最初のλ抽象で束縛されている変数xは線形型を持つにも関わらず、未使用のまま型チェックを通ってしまいます。
これは、unrestrictedで修飾されたラムダ抽象(un λy:un bool.x)の中で線形変数が現れてしまっているからです。
なので実際に適用した先で使用されていなくても、型システムはこのような項をエラーとする事ができません。
containment ruleに従って関数を書き換えてみましょう
(lin λf:lin (un bool -> lin bool).lin true) (lin λy:un bool.x)
(un λy:un bool.x)は線形変数を含む事ができないので(lin λy:un bool.x)という項に書き換え、他の部分もこれに適合する形で書き換えてみました。
この項を型チェックすると、(lin λf:lin (un bool -> lin bool).lin true)内でlinear修飾子によって修飾された項(lin λy:un bool.x)が使用されていない事がエラーとなり、線形変数xが未使用になるような事態を避ける事ができます。
次に、線形ラムダ計算ではq <t,t>とする事で、型q T * Tを持つpairを作る事ができます。
このpairはsplit構文により分割できます。
split構文を使ってpairの一番目の要素を取り出す例を示します。
let spl = split (un <un true,un true>) as x,y in x;
この関数splは型un Boolで型付けされます。
他の項に関しての解説はここでは省略します。
OCamlでの実装
ここでは、前の項で述べた事柄をOCamlでどのように実装したかという事について解説します。また、字句解析、構文解析については省略し、型チェック部分のみ解説することにします。
ただ、全ての項について型チェックの解説を書くのは厳しいので、ラムダ抽象と適用に絞って書きます。他の項についての実装はgithubをご覧ください。
lin λx:lin (lin bool -> lin bool).x (lin true)という項について考えてみます。
最初にラムダ抽象が現れるので本実装では
and t_abs (qual : Type.qual) (name : string) (vtype : Type.ltype) (term_body : Ast.term) (context : Type.context) : checkT = if Type.check_qual_contain_type (Type.get_qual vtype) vtype then () else raise QualError; let (term_body_t,context2) = type_check term_body ((name,vtype) :: context) in if Type.check_qual_contain_type qual term_body_t then () else raise QualError; if Type.get_qual vtype = Type.Lin && List.mem_assoc name context2 then raise (UnUsedError name) else (); if qual = Type.Un then check_equal_context context (List.remove_assoc name context2) else (); (Type.Fn (qual,vtype,term_body_t),List.remove_assoc name context2);;
という関数が呼ばれます。
では、まずこの関数の引数について解説します。
qualはこのラムダ抽象が持つ修飾子に、nameは束縛変数名に、vtypeは束縛変数の型に、term_bodyはλx.tのtの部分に、contextはこの型チェックにおいて用いられる文脈について対応しています。つまり
qual = lin name = x vtype = lin (lin bool -> lin bool) term_body = x (lin true) context = []
となります。
次に
if Type.check_qual_contain_type (Type.get_qual vtype) qual then () else raise QualError;
では、containment ruleをラムダ抽象が持つ修飾子と、束縛変数が持つ修飾子が満たしているかチェックしています。
この例ではcontainment ruleには反していませんね。
let (term_body_t,context2) = type_check term_body ((name,vtype) :: context) in
では束縛変数名を文脈に加えて型チェックした結果として得られる、term_bodyの型（term_body_t）と新しい文脈（linで修飾された値が用いられた場合は文脈から消去されるので変化する）を束縛しています。
ここで束縛した値を用いて更に型チェックを進めます
if Type.check_qual_contain_type qual term_body_t then () else raise QualError;
では、term_bodyの型がラムダ抽象の修飾子との間でcontainment ruleを満たすかチェックしています。
次に
if Type.get_qual vtype = Type.Lin && List.mem_assoc name context2 then raise (UnUsedError name) else ();
という式があります。
これは、束縛変数がlinで修飾されていた場合、term_bodyで確実に使用されていなければいけないので、使用されたか否かに関するチェックをしています。
前にも述べましたが、linで修飾された値は用いられると、文脈から消去されます。なので、term_bodyの型チェックが終わった時点で文脈に残っていた場合は、未使用とみなし、エラーとします。
最後に
if qual = Type.Un then check_equal_context context (List.remove_assoc name context2) else (); (Type.Fn (qual,vtype,term_body_t),List.remove_assoc name context2);;
という式があります。
ここでは、ラムダ抽象がunで修飾されていた場合、束縛変数は文脈から消去されなければいけないので（スコープが閉じる）それを行っています。
また、最後の行（Type.Fn〜で始まるもの）はラムダ抽象に関する型チェックを終えた結果（ラムダ抽象の型と新しい文脈）を返しています。
次にterm_body部分の型チェックについて述べます
let (term_body_t,context2) = type_check term_body ((name,vtype) :: context) in
でterm_body部分の型チェックが行われています。
term_bodyは適用の形になっているので
and t_app (term1 : Ast.term) (term2 : Ast.term) (context : Type.context) : checkT = let (term1_t,context2) = type_check term1 context in check_equal_const term1_t (Type.Fn (Type.Un,Type.Bool Type.Un,Type.Bool Type.Un)); let (term2_t,context3) = type_check term2 context2 in let (Type.Fn (_,t11,t12)) = term1_t in check_equal t11 term2_t; (t12,context3)
という、適用に関する型チェックを行う関数が呼ばれます。
引数には次のようなものが渡されます
term1 = x term2 = lin true context = [x : lin (lin bool -> lin bool)]
let (term1_t,context2) = type_check term1 context in check_equal_const term1_t (Type.Fn (Type.Un,Type.Bool Type.Un,Type.Bool Type.Un)); let (term2_t,context3) = type_check term2 context2 in
では、term1とterm2について、それぞれ型チェックを行っています。term1の型チェックを行った場合にこれも、文脈に変化を及ぼす可能性があるので、新しい文脈に名前をつけて、次の型チェックに利用しています。
最後の行
let (Type.Fn (_,t11,t12)) = term1_t in check_equal t11 term2_t; (t12,context3)
ではterm1を型チェックした結果にterm2を型チェックした結果を適用して、その適用結果を返しています。
x (lin true)において、x : lin (lin bool -> lin bool)なので適用結果はlin boolとなります。
そして、ラムダ抽象についての型チェックを行う関数に戻ってきます。
また、先ほど解説した
(Type.Fn (qual,vtype,term_body_t),List.remove_assoc name context2);;
という部分ですが、要するにこれによってどのような型を返すのかというと、修飾子qualによって修飾された(vtype -> term_body_t)という型を返すことを表しています。
なので、lin λx:lin (lin bool -> lin bool).x (lin true)では、qualがlin、vtypeがlin (lin bool -> lin bool)、term_body_tがlin boolとなるので、lin ((lin (lin bool -> lin bool)) -> lin bool) という型を持つことになります。
