TL;DR
- SML の仕様書 The Definition of Standard ML は、言語の振る舞いを形式的な推論規則で定め、実装の方法は定めていない。
- 静的意味論と動的意味論の分離、不透明シグネチャによる型の隠蔽、Functor、可変状態と多相性の扱いなどを、仕様が定めたこととして紹介する。
- LLM が書いたコードが要求どおりかを確かめるには、要求を書き下ろし、機械がチェックできる不変条件でガードする必要がある、という示唆につながる。
内容
言語仕様の書き方
言語の仕様の書き方には、処理系が事実上の仕様になっているもの（Python、Ruby、Rust）や、自然言語の仕様書があるもの（JavaScript、Java、C）がある。SML は形式的な推論規則で仕様が書かれている。
The Definition of Standard ML（PDF）は、プログラミング言語そのものを扱う人を想定し、文法だけでなく形式的な意味まで自然意味論で記述している。どう実装すべきかではなく、どう振る舞うべきかを定めているので、実装は自由である。型推論のアルゴリズム（Algorithm W や J）、構文解析のアルゴリズム、メモリ管理（ヒープ、スタック、GC）などは含まれていない。発表では、形式的な仕様が何を定め、何を定めなかったかを見ていく。
意味論の分離
仕様は、プログラムの正当性を判定する静的意味論と、プログラムの計算結果を定義する動的意味論に分かれている。let 式と関数適用の推論規則が例として示された。関数適用の推論規則には関数でない値が適用されるケースがないので、値の計算に型は要らない。型検査が通れば実行時の評価は破綻しない、ということを仕様として書ける。
型の抽象化
TypeScript で型を区別するには、Branded types のような工夫をレビュー、Lint、慣習で守る必要がある。公称型があれば十分かというと、そうではない。SML では不透明シグネチャで型を隠蔽できる。実装を structure、インタフェースを signature として書き、structure :> signature とし、シグネチャに type t とだけ書くと、t が string だったという事実が型環境から消える。互換性に価値がある場合は透明シグネチャも選べる。OCaml は不透明シグネチャのみである。発表では、推論規則に UserId を当てはめる例が示された。
型の依存関係
依存性の注入では、依存が満たされないと起動時に、遅延注入なら実行時にエラーになる。SML には、structure を受け取って新しい structure を返す Functor がある。静的意味論では Functor の引数がシグネチャを満たすかを検証し、型名を生成する。動的意味論ではモジュール本体のコードを実行するだけで、型の解決は行わない。動的意味論には「実行時にシグネチャが合わなかった」という規則がない。
可変状態の扱い
SML は純粋ではなく、可変セル（ref）を作れる。多相性（ジェネリクス）と可変状態を組み合わせると、型安全を壊しかねない。Haskell は IO の中に閉じ込め、Rust は let 束縛の多相化を許さない。SML は値である式だけを多相化できる（値制限）。ref [] や compose (id, id) は値ではないので多相化されない。本当に安全かではなく構文でチェックするので、η 展開して fn で包めば回避できる。Wright が 20 万行を超える実在のコードを調べたところ、値制限のために書き直しが必要だったのは η 展開の 31 箇所ほか少数だった。この計測をもとに、規則の単純さと型安全性を優先したという。
コンパイラへの信頼
厳密さに差はあっても、仕様があれば検証や議論の下地になる。CakeML は、コンパイラの各パスが意味を保存することを証明した処理系で、それらの定理を合成して、コンパイラ全体が正しいことまでを証明している。
LLM が生成したコード自体には機械的なチェックをかけられる。しかし、自然言語の要求と実装の対応は機械的にチェックできないので、要求を検査できる形に書き下ろす必要がある。The Definition が推論規則で言語を定めたように、LLM の出力も機械がチェックできる不変条件でガードしたい、という。
その後
The Definition は 1997 年の改定のあと改定されていない。議論はあったが、改定を続ける体制は残らなかった。後継として挙げられたのは WebAssembly で、推論規則が W3C の仕様の本文になっており、健全性は機械で検証され、W3C が改定を続けている。