intro

最近、五十嵐先生のプログラミング言語の基礎概念を読んでいました。コンパクトにlet多相までの知識がまとまっており非常に読みやすかったです。

OCamlの学習がてら実際に言語を実装してみようと思い、 筑波大学の講義資料を参考にさせていただきました。

環境構築・実装にあたってはいくらか大変だった部分があるのですがこれらは気が向いたら別途記事にします。

  • duneの使い方
  • OCamlでのテストの仕方
  • OCamlのCI環境の構築 on GitHub Actions
  • OCamlでのパーサーコンビネータの作り方・使い方
    • Menhirやocamlyaccなどは意図的に使いませんでした

今回作ったもの自体はこちらにあります。watiko/minicaml

振り返り

さて、参考書では最終的にlet多相を有した言語としてPolyTypingML4というものを扱います。文法や型についての定義は以下の通りです。評価規則や推論規則などについては書籍の方を確認してください。

// 文法
e <- 
   | i
   | b
   | "[]"
   | e "::" e
   | x
   | e op e
   | "if" e "then" e "else" e
   | "fun" x "->" e
   | e e
   | "let" x "=" e "in" e
   | "let" "rec" x "=" "fun" y "->" e "in" e
   | "match" e "with" "[]" "->" e "|" x "::" y "->" e

i    <- int
b    <- bool
x, y <- var
op   <- "+" | "-" | "*" | "<"

// 型関連
/// 型変数
α <- { 'a, 'b, ... }
/// 型
τ <- int | bool | τ -> τ | τ list
/// 型スキーム
σ <- τ | α...α.τ
/// 型環境
Γ <- ● | Γ, x: σ

2020/08/22 追記:

現時点の理解では結局unifyは型引数同士の場合を処理できる、という形に落ち着いています。 (間違った例をベースに考え)問題がありそうだという前提でみていたから、定義の読み取り間違いがおきたのではないかと思います。

unifyは得られた解(型代入)を残りの方程式に適用してから再帰的に処理を進めていきます。この結果複数の型変数が方程式に含まれていてもおかしなことが起きないようになっています。そして、一番重要なのがunifyを使う側で複数の型代入を合成した際、その型代入を方程式と見立ててunifyを適用するということです。この結果ある型変数から複数の結果に代入が行われるということが避けられるようになっています。

また、gfnさんが有益情報を呟いていたのでこちらに貼っておきます。

ここからしたは当時の間違った認識に基づき記載がありますので話半分にみてください。

このあたりまで実装するとOCamlのList.hdのような関数が定義できないことに気がつきました。

let rec hd l = match l with
  | []     -> failwith "hd" (* 言語の中にfailwithがない *)
  | x :: _ -> x

本物のfailwith(というか例外機構)は明らかに参考書の範囲を超えていたので諦め気味でした。しかし、インタプリタで実行している関係上この言語のプリミティブとしてfailwithを定義し、実行時にOCaml側のfailwithを呼んであげるとどうとでもなるのではというアイディアを思いつきました。

実装している途中で言語に定義されていない文字列を扱う必要があることに気がつき、それはそれで大変でしたがまた別のお話。型付けも 'a. string -> 'a のような型をつけるだけだったので実装は可能でした。

後々テストを拡充していくと型変数周りの問題(上記の拡張とは無関係)が出始めました。型変数の内部実装はカウンターを用いて重複のない型変数を作るような形になっていたため、処理の途中で何度も型変数が出現するような場合に型変数の値を予期するのが難しくなるというものでした。

let%test _ =
  let t1 = TArrow (TVar "'a1", TVar "'a6") in (* この行を書くのが難しい *)
  let t2 = infer (parse "... snip ...") in
  t1 = t2
;;

inferの内部ではunifyと呼ばれる型の制約を集めた方程式から型代入を求める関数が使われており、 今回実装した型推論アルゴリズムの中核を占めています。unifyを使うと上記のテストが書きやすくなるのではないかと考え次のようなものを作りました。実際のコード

let unify_success t1 t2 =
  try
    (* unify失敗時に例外が発生 *)
    let subst = unify [ t1, t2 ] in
    (* 得られた型代入を片方の型に適用 *)
    let t1 = subst_ty subst t1 in
    t1 = t2
  with
  | _ -> false
;;

ところがこの目論見は失敗してしまいました。

let () =
  let t1 = TArrow (TVar "a", TVar "b") in
  let t2 = TArrow (TVar "x", TVar "y") in
  let t3 = TArrow (TVar "x", TVar "x") in
  let _ = uninfy_success t1 t2 (* true: 期待通り *) in
  let _ = uninfy_success t1 t3 (* true: 期待通りではない *) in
  ()
;;

(最終的には型変数の生成順でいい感じになるようにして比較しました: コード)

上記のコメントのように思っていたような動作はしませんでした。改めてunifyの定義を確認すると、参考書でのunifyは型変数と型変数の比較をエラーとしていました。(私の実装ではパターンマッチの書き方でそのように実装されていなかったので上記でfalseになっていません)

そもそも(unifyが生成する)型代入というものは 相異なる 型変数から型への写像のようなものです。上記の人為的な例では相異なるという部分を満たせない場合もあるためそもそもよろしくなさそうです。

t1 : 'a0 -> 'a0
t2 : 'a  -> 'b

subst = unify [(t1, t2)] # => ['a0/'a; 'a0/'b] # OK
subst_ty subst t1 # => 'a0 -> 'a0
subst_ty subst t2 # => 'a0 -> 'a0

----

t1 : 'a  -> 'b
t2 : 'a0 -> 'a0

// 下の行は修正前
// subst = unify [(t1, t2)] # => ['a/'a0; 'b/'a0] # NG
subst = unify [(t1, t2)] # => ['a/'a0; 'b/'a] # OK
subst_ty subst t1 # => 'b -> 'b
subst_ty subst t2 # => 'b -> 'b

さて、改めて型変数同士のunifyをエラーとなるように実装するとfailwithの型付けは容易に失敗しうるということがわかりました。

(failwith "test") :: []

上記の式に型を付けようとするとすぐに型変数同士のunifyが発生してうまくいきません。

さて、与えられた定義では型変数同士のunifyができないことはわかりました。ではunifyを型変数同士の場合も動作可能なように拡張できるでしょうか。結論から述べると私には拡張できませんでした。

  • [a -> z; z -> a] のような循環している場合
    • これは片方を除去すると解決可能
  • [a -> b; b -> c] のような推移的な制約が存在する場合
    • 複数回代入を行う必要がある
    • [a -> c; b -> c] にすると解決可能
  • [a -> b; a -> c] のようなドメイン側が複数回出現する場合
    • [b -> a; c -> a] のように方向を逆転すれば良い

上記のような単純な場合はそれで良さそうですが、複雑だし計算量のオーダーもすごいことになりそう、何より必ず解けるかどうかというのを証明する作業などが必要でこの方向の拡張は諦めてしまいました。

識者にOCamlの実装について聞いてみるとどうやらunify相当の処理で型代入を返したりせず、関数内で破壊的に型代入相当の操作を行なっているようでした。この方針の場合確かに方程式をいい感じにほぐす必要もなくそのまま実装できそうでした。

実は参考書のみならず、大堀先生のプログラミング言語の基礎理論のunify定義やTAPLのunify定義なども確認しましたが型変数同士の比較はエラーとなるようになっていました。例外についての拡張を扱っているような論文を探したりもしましたが、大概継続と絡めていたり、依存型と絡めていたり、知りたいことから飛躍がある物しか見つかりませんでした。割と世間の人はその辺りに興味がないのでしょうか。

パフォーマンスも上がるし、余計なことに気を取られなくて良いし、破壊的代入は最高だな！ということでこの記事の結びとしたいと思います。