Zenn
🐥

LunarMLの型推論と今後に向けたアイディア

2023/12/25に公開
#
型推論
#
sml
#
standardml
tech

この記事は言語実装 Advent Calendar 2023の25日目の記事です。

この記事では、私が開発しているStandard ML処理系 LunarML の型推論処理の変遷と、将来導入するかもしれない型に関する機能の案を提示します。

変遷

私が書いた当初の型検査器は、いかにも教科書的な感じでした。単一化に使う変数は番号で管理し、置き換えはテーブルで管理し、という感じです。式の型を検査する関数の型はこんな感じでした。

val typeCheckExp : Context * Env * S.Exp -> T.Ty * T.Exp

与えられた式の型と、型注釈をつけた後の式を返す感じですね。素直です。

2022年2月、型検査がコンパイル処理のボトルネックになっていることが発覚します。その時は「期待される型を伝播させることで生成される型変数を減らす」方針で対処しました。当時の記事はこれです：

型検査する関数の型は次のようになりました。「期待される型」があればそれを渡すようにします。これはあくまでヒントで、受け取った方はそれを無視しても構いません。

val typeCheckExp : InferenceContext * Env * S.Exp * (* type hint *) T.Ty option -> T.Ty * T.Exp

6月、型検査がやっぱり遅いので、単一化に破壊的更新を使うようにしました。以下の記事に従って、レベルも導入しました。

その時の経緯はこの記事に書いています：

最近（2023年12月）、bidirectional typingというものに感化されました。型付け規則を「型を生成するもの」「期待される型を受け取り、検査するもの」に分けるのです。すでに「期待される型」を伝播させているのでbidirectional typing風味はあったのですが、それをさらに濃くしてみました。式を型検査する関数は次のようになりました。

val synthTypeOfExp : InferenceContext * Env * S.Exp -> T.Ty * T.Exp
and checkTypeOfExp : InferenceContext * Env * S.Exp * T.Ty -> T.Exp

パターンの型検査も、「型を生成するもの」と「期待される型を受け取り、検査するもの」に分けました。

Standard MLにbidirectional typingを適用するには、いくつか考えることがあります。これらはまだ実装していません。

  • レコードの射影：関数適用 f x はbidirectional typingでは先に f の型を調べて、引数の型で x を検査するのが普通かと思います。しかし、それではレコードの射影 #label record で先に #label の型を調べる必要が出てきます。SMLの射影式 #label では単一化をしないと型を決定できないので、これはあまり嬉しくありません。関数適用の関数部分が射影の場合は、引数の型を先に調べてそれがレコード型ならフィールドの型を返す、という風なアドホックな規則を入れた方が良さそうです。

  • 二項演算：SMLには = や + など、両辺で同じ型を受け取る多相関数が何個かあります。そして、42 のようなリテラルは（int に限定されず）複数の型を取ることができます。すると、x + 42 のような二項演算では、x の型が既知であっても単一化を行なってリテラルの型を決定する必要があります。これは非効率的なので、適用される関数の型が 'a * 'a -> ... の形の場合は、最初の引数の型を調べて、残りの引数はそれに対して検査するのが良さそうです。

  • 型注釈付きの val 宣言：val pat = exp では、先に exp の型を調べてそれに対して pat を検査するべきでしょうか、それとも先に pat の型を調べて exp を検査するべきでしょうか？val 宣言は val x = exp のようにパターンに型注釈がつかない事例が多そうなことを考えると、前者が良さそうです。しかし、そうすると val pat : ty = exp のように型注釈がついている場合に exp の検査で「文脈から期待される型」が利用できないことになります。そういう場合もやはりアドホックな規則を入れて、左辺のパターンのトップレベルに型注釈があれば、内側のパターンと右辺の式を両方それで検査するのが良さそうです。

将来

本来、Standard MLの型検査にはbidirectional typingのパワーは必要ありません。エラーメッセージがわかりやすくなるとかはあるかもしれませんが。しかし、LunarMLが将来拡張機能を実装した時にbidirectional typingの恩恵を受けられるかもしれません。そういう拡張機能のアイディアをいくつか挙げます。

型に依存する名前

よくあるオブジェクト指向言語では、オブジェクトの型が名前空間を持っていて、メソッドでそれを呼び出せます。さらに、Swiftでは、文脈に期待される型から、型名なしでコンストラクターなど（.init や .some みたいなやつ）を呼び出せます。オブジェクト指向の是非はともかく、型に名前空間を紐づけるというのは便利そうなアイディアなので、LunarMLにも取り入れると良いかもしれません。

（実はStandard MLにも型に値構築子の名前空間が紐づいていて、datatype replicationで利用されたりしますが、普段使いする感じではないですね。）

Javaや.NET向けのSML処理系では obj.#method みたいな感じでメソッド呼び出しを書けたようですが、ここでは別の方法を考えます。

まず、文脈から期待される型がある場合は、コンストラクターの属するモジュール名を省略できるというのはどうでしょうか。つまり、期待される型が StringCvt.radix であれば StringCvt.HEX の代わりに .HEX と書けるようにするのです。

メソッドについてですが、関数型界隈にはすでに「引数を先に、関数を後に」書けるテクニックが知られていますね。パイプライン演算子 |> : 'a * ('a -> 'b) -> 'b です。これを利用できないか考えましょう。

パイプライン演算子の第一引数をオブジェクト、第二引数をメソッドに見立てます。さらに先の「二項演算」で考えたルールを拡張すると、第一引数の型を元にして、第二引数の一部の型を分かった状態で型検査できます。つまり、'a -> 'b の 'a が分かった状態です。'a -> 'b が期待される状態で「型に依存する名前」が現れたら、'a の型に紐づいた名前空間を探索することにしましょう。そうすると、例えば x |> .toString は x の型を元に toString 関数を探索することになります。

「型に依存する名前」に幾つかの引数を適用することも許容しましょう。すると、 xs |> .map (fn y => y + 1) と書くと map 関数が xs の型を元に探索されることになります。

コンストラクターのやつとメソッドっぽいやつを組み合わせると、例えば Word.fmt StringCvt.DEC w を w |> .fmt .DEC と書けることになります。……なるといいなあ。

この方式で行くと、オブジェクト指向なライブラリーのバインディングを作る際は引数の順番は

val method : arg1 * ... * argN -> self -> result

とするのが推奨されることになります。

型に名前空間を紐づけるのは自動でやるのは難しそう（一つの型が複数のモジュールからエクスポートされうる）なので、何らかの宣言で明示することになります。例えば

(* int 型に Int モジュールを紐づける *)
_associate int = Int

となるでしょうか。

GADTs

GADTsもあると良さそうですね。私はまだよく調べていないのですが、とりあえずリストに挙げておきます。

部分型付け

LunarMLはLuaやJavaScriptなど、既存の言語とうまく連携できるようにしたいです。もしもこの先、Javaや.NETなど、既存の静的型付けオブジェクト指向言語とやり取りできるようにしたい、となった時、LunarMLにも部分型付けがあると便利な可能性は十分にあります。

bidirectional typingは、部分型付けをMLの型推論と共存させるのに役立ちそうです。

さて、合併型（ユニオン型）は導入するべきでしょうか。Javaや.NETと連携する上で合併型があると便利かは分かりませんが、JavaScriptと連携する上では欲しくなるかもしれません。普通に合併型を導入するとこれまで型がつかなかった式に型がつくようになります。例えば

if b then 42 else "foo"

という式は従来は型エラーでしたが、合併型があると union[int, string] という型をつけられるようになります。これは望ましいことでしょうか、それとも驚きでしょうか？

合併型については、文脈から期待される型が合併型の場合のみ許容するのが良いかもしれません。つまり、

val x = if b then 42 else "foo"

の場合は拒絶し、

val x = (if b then 42 else "foo") : union[int, string]

の場合は許容するのです。

部分型といえば有界量化もあります。構文をどうするか考えたいです。

単一化との兼ね合い

現在のLunarMLの型推論アルゴリズムでは、単一化の変数をゴリゴリ書き換えています。すると、制約の生成される順番によって高度な型機能のコンパイルが通ったり通らなかったりしそうです。例えば、

val fst : 'a * 'b -> 'a = fn (x, _) => x
fun foo r = fst (Word.fmt r 0w0, r = .DEC)

はコンパイルに成功するべきでしょうか？先に Word.fmt r 0w0 の型検査を行うと成功しそうです。一方、

val fst : 'a * 'b -> 'a = fn (x, _) => x
fun foo r = fst { 2 = r = .DEC, 1 = Word.fmt r 0w0 }

は失敗しそうです。

こういうコンパイラーの実装の詳細に依存する方式はユーザーを驚かせる可能性があるので、慎重にしたいです。

Discussion