LunarMLの近況/中間言語に型をつける

私が作っているStandard MLコンパイラー、LunarMLの近況報告記事です。LunarMLに関する直近の記事は

でした。

400スター

GitHubスター数が400に到達しました。ありがとうございます(執筆時点では402に増えています)。まだスターをつけていない方は https://github.com/minoki/LunarML でスターをつけることができます。

スターが350に到達したのは2024年10月、300に到達したのは2024年5月のことだったようです。

(本プロジェクト限定というわけではありませんが)GitHub Sponsorsにも触れておくと、現在は @toyboot4e さんと @kevin-kmetz さんにスポンサーしていただいています。ありがとうございます。

https://github.com/sponsors/minoki

中間言語に型をつけたい:型をつける動機付け

JavaScript連携の記事で、

JavaScriptの Promisethen はコールバックが Promise(正確にはThenable)を返したら更にそれを待ち受ける挙動をします。モナドのbindみたいな感じです。この仕様があると ('a promise) promise みたいな型をいい感じに扱えないので、Standard MLの世界のコードが Promise の中身として Promise を返そうとした場合はラッパーを噛ませるようにします。

と書きました。「Promise の中身として Promise (より正確には Thenable)を返そうとした場合はラッパーを噛ませる」の部分をコードで説明すると、次のような関数 wrapThenable, unwrapThenable の呼び出しを適宜噛ませる形になります:

function ThenableWrapper(x) {
    this.payload = x;
}
function wrapThenable(x) {
    if (typeof x === "object" && typeof x.then !== "undefined") {
        return new ThenableWrapper(x);
    } else {
        return x;
    }
}
function unwrapThenable(x) {
    if (x instanceof ThenableWrapper) {
        return x.payload;
    } else {
        return x;
    }
}

JavaScriptの通常の Promise との相互運用を可能にするため、値が Thenable ではない場合は元の値を活用します。

しかし、Promise の操作をするたびに必ず wrapThenable の呼び出しを挟むというのはダサいです。値の型が stringint など、明らかに Thenable ではないことがわかっている場合は、呼び出しを省略したいです。そのためには、最適化が進んだ段階でもコードの型情報を保持しておくことが必要です(インライン化によって型が判明する状況を考慮する)。現状のLunarMLでは最適化はCPS中間言語に対して行っているので、CPS中間言語を型付きにすることが必要です。

型情報の別の用例を挙げます。次のコードを考えます:

(* val foo : unit -> unit
   val bar : unit -> string *)
val x : unit = foo ()
val _ = bar x

xunit 型の変数で、情報を保持していません。こんなコードを書く人はいないと思われるかもしれませんが、最適化の結果としてこういうコードが現れることは十分にあり得ます。

この場合、ソース中の x という変数を出力コードに反映させるのは無駄です。特に、Luaではローカル変数は貴重な資源なので、節約したいです。そこで、「型が unit の変数の使用は値 () で置き換える」という変換が考えられます。

そんな感じで、中間言語、特にCPS中間言語に型がついていると便利そうです。

中間言語に型をつけたい:作業

LunarMLの中間言語は

  • ソース(Standard ML)→(いくつかの前処理と型検査)
  • →型付き中間言語→(モジュールの脱糖、オーバーロードとequality typeの脱糖)
  • →System Fωライクな中間言語→(パターンマッチの脱糖)
  • →System Fωライクな中間言語→(CPS変換)
  • →CPS中間言語→(各種最適化)
  • →CPS中間言語→(ネストされた式の回復)
  • →ネストした式のある中間言語→(変換)
  • →LuaやJavaScriptのコード→(変換)
  • →最終的なLuaやJavaScriptのコード

という流れになっています。

従来は、System Fωライクな中間言語までは型がついていて、CPS中間言語には型がないという状況でした。3月ごろに、System Fωライクな中間言語の型検査器を実装しました。

今回、CPS中間言語を型付きにして、型検査器も実装しました。

型付きのCPS変換はしっくりくる先行研究が少なくて、なかなか難航しました。LunarMLの型付きCPSメモにいくつかメモりましたが。

最終的には、「型抽象と型適用は、通常の関数と関数適用と同様に扱う(ただしフラグをつけて区別できるようにする)」「最適化をある程度かけた段階で、多相型を消去する。完全に型を消去するのではなく、漸進的型付けのAnyのような感じで置き換える。その後再び最適化をかける」という形にしました。

最初は中間言語に対する型検査器はなくても良いかなと思っていましたが、型に関するバグがあったときに型検査器がないとエスパーでデバッグする羽目になり、しんどかったです。なので、結局型検査器を実装しました。実装したらしたで無限にバグが見つかってしんどいことになりましたが。

型周りのバグの発見には、過去に書いたテストが役に立ちました。テストは資産です。

悪いニュースとして、CPS中間言語に型をつけたことで、コンパイルが遅くなったり、メモリ使用量が増大したりしています。中間言語の型検査をやめれば時間の増加は軽減されると思いますが、テスト時はしっかり検査したいので、テストの所要時間は減らせなさそうです。

ML Family Workshop

今年のICFPはシンガポールでの開催で、それと併設で10月16日にML Family Workshopというのが開催されます。学会誌なんかは出ない、インフォーマルな集まりのようです。

このML Family WorkshopにLunarMLの話を応募したところ、通りました。というわけで、行ってきます。

このところLunarMLの作業を頑張っているのは、ML Family Workshopで話せる内容を少しでも増やしたいという気持ちからです。ですがCPS中間言語の型付けに時間を使いすぎた感があるので、そろそろ資料作成と発表練習をしないといけません。

バージョン0.3.0

ML Family Workshopの前になるか後になるかは不明ですが、そろそろ新しいバージョンとしてリリースしても良いかもしれないと思っています。ユーザー視点ではJavaScript周り(Promise連携とか)が新機能になるかと思います。GitHub Actionsでビルドする仕組みを整えたので、MLtonでビルドしたバイナリーも配布できると思います。

可算選択公理を仮定しない構成的数学での実数の構成について

可算選択公理を仮定しない構成的数学では、Cauchy列に基づいた実数の構成をやるときに完備性が示せなくなる(らしい)。この弱点は、実数の構成に使うCauchy列を有理数の点列ではなく、有理数の集合の列とすれば克服できる。

このことは「Handbook of Constructive Mathematics」のFred Richmanの記事で示唆されているが、あまり詳しい取扱いはなかったので自分でやってみた。と言っても、地味な命題の証明は省略しているが……。

https://miz-ar.info/math/real-construction-without-choice-20250816.pdf

Mathlogにも書いてみた。

構成的数学での実数の構成について | Mathlog

続・TypeScriptのnever型の話/型付け規則についての雑談

前に書いた「TypeScript使いの憂鬱:never型はプロパティを持つか」の補足をして、関連する話題を取り上げます。前の記事では

「never型の式にプロパティアクセスができない」という動作は型システムの一貫性から外れた、アドホックな(場当たり的な)動作であるということです。

と書きました。「never型の式にプロパティアクセスができる」という動作が普通の型システムでどのように正当化されるのかを掘り下げます。

TAPLこと「型システム入門」をベースに説明します。

続きを読む

有限にも無限にもなれない僕らの集合

「集合\(A\)が有限集合であるとは、ある自然数\(n\)に対し、\(A\)と\(\{0,1,\dotsc,n-1\}\)の間に全単射が存在することである。一方、有限集合ではない集合は無限集合である。」

「存在量化子\(\exists\)の有限回の除去は通常の論理でできるので、選択公理が力を発揮するのはもっぱら無限集合が相手の時である。」

……本当にそうだろうか?

「集合は有限集合か無限集合のどちらかだ」という考え方は排中律的であり、構成的数学では考え直す必要がある。

この記事では、「無限」ではないが「有限」とも言えない集合について考えたい。有限集合の定義は最初に書いたものとする。無限集合のちゃんとした定義はしない。

続きを読む

良いコンパイラーは親切なエラーメッセージを出さなければならない:LunarMLの場合

プログラミング言語の静的解析の良い点として、一回の解析で複数の誤りを検出できる(場合がある)点があります。実行時エラーしか出ない言語だったら、一回の実行で一個のエラーに遭遇して、修正して、またエラーに遭遇して、ということを繰り返さなければなりません。

言い換えると、遭遇した最初の誤りでコンパイルが停止してしまうようなコンパイラーは、いくら静的な型システムを備えていても、動的言語並みの貧弱な開発体験しか得られないということです。コンパイルの手間がかかる分むしろマイナスです。

コンパイラーではなく言語サーバーでも同じことで、ソースコードの最初の誤りで解析が停止してしまう言語サーバーからは貧弱な開発体験しか得られないでしょう。

検出できるエラーの個数だけではなく、エラーメッセージの親切さも、結構開発体験を左右するのではないかと思います。よくある誤りに対して的確なエラーメッセージを出すことができれば、ユーザーがエラーの原因で悩む手間が省けます。

一つの言語仕様に対して複数のコンパイラーが存在する状況で、エラーメッセージの品質はコンパイラー間での差別化の要素になり得ます。この記事では、Standard MLコードに対して良いエラーメッセージを出す工夫について考えてみます。

続きを読む

LunarMLとJavaScriptの連携について

久しぶりにLunarMLの話題です。LunarMLは、私が作っているStandard MLコンパイラーです。

最近は、JavaScriptとの連携に関する機能を追加しています。Webで使えるようにするのと、Promise/async/await周りの統合をいい感じにすることを目標にしています。

続きを読む

定理証明支援系についての問題意識

定理証明支援系 (proof assistant / interactive theorem prover) というのは、専用の言語で書いた証明を機械にチェックさせるツール、およびその証明の記述を支援するツールです。Rocq(旧名Coq)、Agda、Lean、Isabelleなどが有名です。

この記事では、定理証明支援系について私が感じている問題意識を説明します。私自身は定理証明支援系のヘビーユーザーではないので、もっと勉強したり、定理証明支援系を使い込んだりすれば答えが見つかるのかもしれません。詳しい方からのフィードバックを頂けると嬉しいです。

続きを読む

「関数型まつり」に行ってきた

去る6月14日・15日に東京・中野で開催されたイベント「関数型まつり」に行ってきました。と言っても、14日は地元で予定があったので、参加したのは15日だけです。

関数型まつり

3つの部屋でセッションが同時進行しており、どれも面白そうだったので、分身の術を習得しておかなかったのが悔やまれます。

直接聞いた発表に限らず、資料のみ見た発表についても、いい機会だと思って思ったことを書かせてもらいます。

続きを読む

可算選択公理と実数

構成的数学に基づいて解析学を展開し、プログラミングでそれを実装するようなコンテンツを作れないかなあと去年ぐらいから考えています。

構成的数学と一口に言っても、選択公理をどのくらい認めるかによっていくつか流儀があります。Bishopの構成的数学は従属選択公理 (dependent choice) を認めていますが、人によっては可算選択公理 (countable choice) すら使いたくないかもしれません。

Bishop流の構成的数学では、古典数学とそう変わらない実数論が展開されています。これは可算選択公理が使える、という点が大きそうです。

それでは、可算選択公理を仮定しない構成的数学だと実数の概念がどうなるか気になるのが人情だと思います。

続きを読む

「関数の副作用の有無」よりも大事なもの

プログラミングをやっていると、「関数に副作用がある」とか「副作用がない」あるいは「純粋である」という話をちょいちょい耳にする。そして、「外界の状態を読み取るけど変更はしない関数」、例えば

function getTime() {
    return Date.now();
}

のような関数に副作用があるか?みたいな議論が始まったりする。

くだらない議論だ。

何か概念を定義するときは、それが「役に立つ」場面を提示できる必要がある。「関数の副作用」を定義するときは、「関数の副作用」がわかったときに何をしたいのかをはっきりさせる必要がある。「関数のどういう側面に注目したいか」を決めずに「副作用の有無」を論じるのはナンセンスだ。

ここでは、言語処理系(コンパイラー)を実装する者の立場で、関数の副作用について論じてみたい。

続きを読む