簡単な型システムを実装していく９ STLC+...+Variant+Fix+Ref

MLの一つの特徴として、デフォルトではほとんどの変数やデータ構造に破壊的代入が不可だが、破壊的代入が可能なデータ構造を明示的に選択することが可能、という非純粋な関数型プログラミング言語であることが挙げられる。そういった非純粋性を支える一つの重要なデータ型がrefである。

ref型を作るためのオペレータref（ここら辺OCamlだと型とオペレータの名前が被ったりしてややこしい）、ref型からデータを取り出すderef、そしてref型に破壊的代入をするassignの三つの式を用意する。

gist.github.com

型

新しい型はref型のみ：

type ty =
...
| TRef of ty

保持する値の型でパラメトライズされている。

式

前述のとおり三種の式を用意：

type exp =
...
| ERef of exp
| EDeref of exp
| EAssign of exp * exp

• ERefはなんらかの式をとり、その評価結果を保持するref型の値を作る
• EDerefはref型の式をとり、そのrefが保持する値を返す
• EAssignはref型の式とそのrefに代入する式をとり、後者の評価結果を前者に代入する（元々入っていた値は破棄される）

typeof関数

refを作るERefに対するケース：

let rec typeof env = function
...
| ERef e -> TRef (typeof env e)

保持する式が'a型ならERef全体はTRef 'a型になる。

refから値を取り出すEDeref：

| EDeref e -> (match typeof env e with
    | TRef t -> t
    | _ -> failwith "non-ref passed to deref")

derefする対象がTRef 'a型ならderefした結果は'a型。TRef出ないなら型エラー。

refに値を代入するEAssign：

| EAssign(e1,e2) -> (match typeof env e1 with
    | TRef t when t = typeof env e2 -> TUnit
    | TRef _ -> failwith "type mismatch between ref and value"
    | _ -> failwith "ref type expected")

もし代入先がTRefで保持する型と代入される値の型が合致している場合は型検査に成功。式全体の型はTUnitとなる。もしTRefだけどrefの型と値の型が合わない、あるいは代入先がTRefではない場合は型エラー。

次回

次から何回かにわけてエラーの型システムを見ていく。