simple-subをocamlに移植したい

はじめに

この記事は書きかけです。書こうと思っていたのですが大幅に遅れているうちに OCaml に移植されてしまいました:

simple-sub を OCaml に移植してみると Scala の implicit や Object を使ったテクニックが削除され、プログラムの依存関係がはっきりするのでより理解しやすいものとなります。

simpler-sub はより simple-sub を単純化したものです。これを OCaml に移植したものは公開されていないように思うので OCaml に移植してみました:

simpler-sub は 500行ほどで実装できているのでより簡単なはずです。

TypeScriptなどの言語にはunion型やintersection型が含まれ便利に利用されています。しかしながらunion型やintersection型が含まれている言語の実装は複雑で難しいと言えるでしょう。そこで、その型システムの本質的な部分を抽出した言語がsimple-subです。simple-subはlet多相な型推論に加えてレコード、部分型、再帰再帰型、union型、intersection型を加えた強力な型システムを持ちます。

実装は小さくまとめられており、高速に動作するよう設計されています。高速化のポイントは1)レベル付きの多相型推論、2)破壊的な型変数による型制約の保存、3)型推論時に正規化なし型計算と4)表示用型計算です。レベル付きの多相型推論は単純な型スキームを用いた型推論を高速化するための技術でMilnerによって導入されました。型制約を環境に保存し持ち回ることもできますが、表の検索には時間がかかるので直接型変数を破壊的に書き換えたほうが高速になります。union型やintersection型は正規化することで計算できますが重い処理なので型推論時には正規化せずに直接計算したほうが高速になります。型推論で求められた型は表示時に見やすい形に書き換えることで可読性を増します。

1. 構文

p ::= (let rec? x x* = e ;?)*    プログラム
e ::=
    | x                          変数
    | λx. e                      関数
    | e e                        関数適用
    | i                          整数
    | let rec? x x* = e in e     let式
    | if e then e else e         if式
    | {x=e;...;x=e}              レコード
    | e.x                        選択

simple-sub は変数、関数、関数適用のラムダ計算に加え整数とifとlet と let rec式レコードと選択があり型指定のない言語です。
この言語の型システムには多相的で部分型、再帰型、union型とintersection型があります。

2. 型推論

simple-sub はシンプルと言いつつかなり難しいので型推論のみをまず考えます。
1)型推論と言ってもlet多相型推論2)部分型3)再帰再帰型4)union型5)intersection型を扱います。
5つの型システムのサブタイプ関係はやはり複雑です。
let多相型推論については Oleg の説明が簡単です。
再帰型についてはTAPLを読むと良いでしょう。
union型およびintersection型のリアルタイム計算は香港の女性の論文が良いでしょう。
それをまとめ上げるのは難しいのでsimpler-subをまず参考にすると単純なところからのステップアップができるはず。
しかしsimpler-sub は Scala で書かれているのでOCaml版が欲しいところです。
できれば、全ての説明が載っているような文献があると嬉しいわけですが、長くなるので困ります。TODO:文献。

3. 表示部

型を表示する場合はそれなりに型をまとめ単純化して表示する必要があります。

型の正規化をする例は以下のソースが参考になります:

4. simpler-sub

simple-sub は、やはり複雑で難しかった。そこで simple-subをより単純化したものがsimpler-subです。

Simpler-sub は Simple-sub の代替アルゴリズムで、理解しやすい反面、制限が多くなりますが、
おそらく多くの実用的なケースで十分なものです。

オンラインデモはこちら: https://lptk.github.io/simpler-sub/

Simplifications

Simple-subとは対照的に、Simpler-subは以下をサポートしていません:

• (1) 再帰型: 再帰制約があるとエラーになります。

  もしあなたの言語が外部で定義された再帰的データ型（例えば代数的データ型）を持っているならば、
  いずれにせよ厳密には再帰的な型は必要ないのです。

  しかし、 let foo x = ... foo x.f ... のようなフィールド再帰的な定義をサポートするためには、この foo がどの再帰的なデータ型の f フィールドを再帰するのかを型チェッカに明らかにする方法が必要でしょう。
  (そうでなければ、推論されたレコード型間の再帰的制約エラーが発生します）。
  そのための1つの方法は、オーバーロードされたフィールド名の使用を拒否することです（Haskell 98のように）。
  または、（最近のHaskellのように）部分型の代わりに型クラスを使ってフィールドを選択する。
  または、（OCamlのように）可能な限りフィールド選択の曖昧さをなくすために文脈情報を使用します。

  再帰的な型がないため、いくつかの型推論アルゴリズムがより単純で効率的になります。
  なぜならばキャッシュを持ち運ぶことなく、自由に帰納的に型を分解できるようになったからです。

• (2) 入れ子のlet多相性：このプロトタイプでは，ローカルな（つまり入れ子の） let ... in ... バインディングには決して多相型が割り当てられません。

  これは，レベルを扱う必要がないという点で，アプローチをさらに単純化するものです．
  そして、これには前例があります。
  例えば、Dimitrios Vytiniotis, Simon Peyton Jones, and Tom Schrijversによる論文 Let Should not be Generalised を参照してください。

• (3) 型変数間制約の精密化：2つの型変数間の制約は、即座に2つの変数を単一化する。

  この結果は、人が考えるほど悲惨なものではありません。
  ポリモーフィズムが浸透しているおかげです（ただし、制約2も参照）。
  このアプローチで精度の低下が問題となるのは、以下のようなプログラムです。
  let test f x y = if f x then x else y,
  これは Simple-sub で ('a -> bool) -> 'a ∧ 'b -> 'b として型付けされています。
  しかし、Simpler-sub では ('a -> bool) -> 'a -> 'a と型付けされています。

  • y は f に流入することはなく、実際には何の関係もないにもかかわらず、
    f が受け取るパラメータの型である 'a として型付けされることに注意してください。

  Simple-subや一般的な代数的サブタイピングでは、
  型変数不等号の正確なグラフが記録され、
  ユーザに表示する前に積極的に簡略化する必要があります。
  一方、積極的に型変数を単一化することで、
  推論される型グラフは従来のHindley-Milner型推論とほぼ同等に単純化され、
  推論型単純化が非常に容易になります。

制限(3)は主要型推論を破壊します:
型推論のアプローチでは拒否される、よく型付けされた項が存在する可能性があります。

制限(1)は主型特性を破壊します:
最も正確な型が与えられない項が存在します。

• これらは、再帰的な型を通して Simple-sub によって型付けされたはずです。
  しかし、より精度の低い非再帰的な型を与えることは可能です。
  Simpler-sub は、実際、そのような項を明確に拒絶します。

これらの単純化はそれぞれ独立して Simple-sub から行うことができます。
このプロジェクトでは、結果がいかに単純に見えるかを示すために、これらをまとめて実装することにしました。
部分型のある言語における型推論の基礎となりうるものでありながら、非常に有用なものです。