Luauにおけるセマンティックサブタイピング
Luauは、数百万人のクリエイターにセマンティックサブタイピングの力を提供する最初のプログラミング言語です。
誤検知の最小化
Roblox Studioの「スクリプト分析」ウィジェットのようなツールにおける型エラー報告の問題の一つは、誤検知です。これらは分析の副産物である警告であり、実行時に発生し得るエラーとは一致しません。例えば、プログラム
local x = CFrame.new()
local y
if math.random() < 0.5 then
y = CFrame.new()
else
y = Vector3.new()
end
local z = x * yは、CFrameがVector3およびCFrameの両方との乗算をサポートしているため、実行時には発生し得ない型エラーを報告します。（その型は((CFrame, CFrame) -> CFrame) & ((CFrame, Vector3) -> Vector3)です。）
誤検知は、特に新規ユーザーの導入において好ましくない。型に好奇心のある開発者が型チェックを有効にした途端、大量の誤った赤い波線に直面した場合、すぐにそれを無効にしたくなる強い動機が生じる。
実行時エラーが発生するかどうかを事前に判断することは不可能であるため、型エラーにおける不正確さは避けられません。型システムの設計者は、誤検知（false positive）と検知漏れ（false negative）のどちらを受け入れるかを選択しなければなりません。Luauでは、これはモードによって決定されます。strictモードは誤検知を優先し、nonstrictモードは検知漏れを優先します。
不正確さは避けられないものの、それらが誤ったエラーや、オートコンプリートやAPIドキュメントといった型駆動型ツールの不正確さにつながるため、可能な限り排除するよう努めています。
誤検知の原因となるサブタイピング
Luau（およびTypeScriptやFlowのような他の多くの類似言語）における誤検知の原因の一つは、サブタイピングです。サブタイピングは、変数が初期化または代入される際、および関数が呼び出される際に常に使用されます。型システムは、式が変数の型のサブタイプであるかどうかをチェックします。例えば、上記のプログラムに型を追加すると
local x : CFrame = CFrame.new()
local y : Vector3 | CFrame
if math.random() < 0.5 then
y = CFrame.new()
else
y = Vector3.new()
end
local z : Vector3 | CFrame = x * yすると、型システムは `CFrame` の乗算の型が `(CFrame, Vector3 | CFrame) -> (Vector3 | CFrame)` のサブタイプであることをチェックします。
サブタイピングは非常に有用な機能であり、型和（T | U）や型積（T & U）のような豊富な型構造をサポートします。例えば、number?は、数値またはnilのいずれかの値を持つ和型(number | nil)として実装されています。
残念ながら、サブタイピングと交差型および和集合型の相互作用により、奇妙な結果が生じることがあります。以前の Luau における単純（だがかなり人為的）な例として、次のようなものがありました：
local x : (number?) & (string?) = nil
local y : nil = nil
y = x -- Type '(number?) & (string?)' could not be converted into 'nil'
x = yこのエラーはサブタイピングの失敗によって引き起こされます。古いサブタイピングアルゴリズムは、(number?) & (string?)がnilのサブタイプではないと報告します。これは誤検知です。なぜなら、number & stringには値が含まれていないため、(number?) & (string?)に含まれる可能性のある唯一の値はnilだからです。
これは人工的な例ですが、この問題によって引き起こされた実際の課題が開発者から報告されています。例えば、https://devforum.roblox.com/t/luau-recap-july-2021/1382101/5 などです。 現在、これらの問題は主に、高度な型システムの機能を利用している作成者に影響を及ぼしていますが、型推論の精度が向上するにつれて、型注釈のないコードであっても、和集合型や共通部分型がより一般的になるでしょう。
Luau では、構文的サブタイピングという従来のアプローチから、セマンティック・サブタイピングと呼ばれる代替手法に移行したため、この種の誤検出は発生しなくなりました。
構文的サブタイピング
別名「以前のやり方」。
構文的サブタイピングは、構文主導型の再帰アルゴリズムです。交差型や和集合型を扱う上で興味深いケースは以下の通りです：
- 反射性：
TはTのサブタイプである - 交差 L:
TᵢのいずれかがUのサブタイプである場合、(T₁ & … & Tⱼ)はUのサブタイプとなる - 和集合 L:
(T₁ | … | Tⱼ)は、TᵢのすべてがUのサブタイプである場合に限り、Uのサブタイプである - 交差 R:
TがすべてのUᵢのサブタイプである場合、Tは(U₁ & … & Uⱼ)のサブタイプである - 和集合 R:
Tが(U₁ | … | Uⱼ)の部分型となるのは、TがUᵢのいずれかの部分型である場合に限る。
例：
- 反射性により：
nilはnilのサブタイプである - したがって、Union R により：
nilはnumber?のサブタイプである - したがって：
nilはstring?のサブタイプである - したがって、Rの交わりにより：
nilは(number?) & (string?)のサブタイプである。
やった！ 残念ながら、以下の規則を用いると：
numberはnilのサブタイプではない- したがって、和集合 L により：
(number?)はnilのサブタイプではない - したがって：
stringはnilのサブタイプではない - したがって、和集合 L によれば、
(string?)はnilのサブタイプではない - したがって、交差 L により：
(number?) & (string?)はnilのサブタイプではない。
これは構文的サブタイピングの典型的な特徴である。「はい」という結果が返された場合は正しいが、「いいえ」という結果が返された場合は間違っている可能性がある。このアルゴリズムは保守的な近似であり、「いいえ」という結果が型エラーにつながる可能性があるため、これが誤検知の原因となる。
意味論的サブタイピング
別名「現在のアプローチ」。
サブタイピングを構文主導のものとして考えるのではなく、まずその意味論を検討し、その後でその意味論がどのように実装されるかに戻ります。このため、私たちは意味論的サブタイピングを採用します：
- 型のセマンティクスとは、値の集合である。
- 交差型は、集合の交わりとして考えられます。
- 和集合型は、集合の和集合として捉える。
- サブタイピングは、集合の包含関係として捉えます。
例えば：
型 | 意味論 |
|---|---|
| { 1, 2, 3, … } |
| { “foo”, “bar”, … } |
| { nil } |
| { nil, 1, 2, 3, … } |
| { nil, “foo”, “bar”, … } |
| { nil, 1, 2, 3, … } ∩ { nil, “foo”, “bar”, … } = { nil } |
また、サブタイプは集合の包含関係として解釈されるため：
サブタイプ | 超型 | なぜなら |
|---|---|---|
|
| { nil } ⊆ { nil, 1, 2, 3, … } |
|
| { nil } ⊆ { nil, “foo”, “bar”, … } |
|
| { nil } ⊆ { nil } |
|
| { nil } ⊆ { nil } |
したがって、意味論的サブタイピングによれば、(number?) & (string?)はnilと等価ですが、構文的サブタイピングは一方向のみをサポートします。
これ自体は問題ありませんが、ツールでセマンティックサブタイピングを利用するにはアルゴリズムが必要であり、セマンティックサブタイピングの検証は容易ではないことが判明しています。
セマンティックサブタイピングは難しい
正確にはNP困難です。
グラフの着色をセマンティックサブタイピングに還元することは可能です。グラフを Luau 型としてコーディングし、型に対するサブタイピングのチェックが、グラフの着色が不可能であることのチェックと同じ結果になるようにすればよいのです。
例えば、3つのノードと2つの色を持つグラフの着色は、型を使って次のように行うことができます：
type Red = "red"
type Blue = "blue"
type Color = Red | Blue
type Coloring = (Color) -> (Color) -> (Color) -> boolean
type Uncolorable = (Color) -> (Color) -> (Color) -> falseすると、グラフはサブタイプUncolorableとスーパータイプColoringを持つオーバーロード関数型としてエンコードでき、制約が違反された際にfalseを返すオーバーロード関数として表現できる。各オーバーロードは1つの制約をエンコードする。例えば、線分には隣接するノードが同じ色になってはならないという制約がある：
type Line = Coloring
& ((Red) -> (Red) -> (Color) -> false)
& ((Blue) -> (Blue) -> (Color) -> false)
& ((Color) -> (Red) -> (Red) -> false)
& ((Color) -> (Blue) -> (Blue) -> false)三角形も同様ですが、端点同士も色が同じであってはなりません：
type Triangle = Line
& ((Red) -> (Color) -> (Red) -> false)
& ((Blue) -> (Color) -> (Blue) -> false)ここで、TriangleはUncolorableのサブタイプですが、Lineはサブタイプではありません。なぜなら、線分は2色で塗ることが可能だからです。これは、任意の有限数の色を持つ任意の有限グラフに一般化でき、したがってサブタイプチェックはNP困難です。
これに対処するために、以下の2つの方法を採用しています：
- メモリ使用量を削減するために型をキャッシュし、
- 型キャッシュが肥大化した場合は「Code Too Complex」エラーを発生させて処理を中断する。
幸い、実運用ではこれが頻繁に発生することはないでしょう。Standard MLのような型システム（EXPTIME完全）の経験から、実運用ではこのような問題は生じないという確かな証拠があります。実際、型としてチューリングマシンのテープをコーディングするには、わざわざ手間をかける必要があります。
型の正規化
意味論的サブタイピングを決定するために使用されるアルゴリズムは、型正規化です。構文に左右されるのではなく、まず型を正規化されるように書き換え、その後、正規化された型に対してサブタイピングをチェックします。
正規化された型とは、以下のいずれかの正規化されたnil型（xml-ph-0000@deepl.internal または xml-ph-0001@deepl.internal）の和集合である。
- 正規化されたnil型（
neverまたはnilのいずれか） - 正規化された数値型（
neverまたはnumberのいずれか） - 正規化されたブール型（
never、true、false、またはbooleanのいずれか） - 正規化された関数型（
never、または関数型の交差集合）など
型が正規化されれば、意味的なサブタイピングのチェックは簡単です。
すべての型は正規化可能です（ただし、ジェネリック型パックに関してはいくつかの技術的な制約があります）。重要な手順は以下の通りです：
- 互換性のないプリミティブ型の交差を除去すること。例えば、
number & boolはneverに置き換えられ、 - 関数の和集合の除去。例えば、
((number?) -> number) | ((string?) -> string)は(nil) -> (number | string)に置き換えられる。
例えば、(number?) & (string?) を正規化すると number & string が削除されるため、残るのは nil のみとなります。
型正規化の実装における最初の試みでは、これを多用しましたが、その結果、パフォーマンスが著しく低下しました（複雑なコードの型チェックに、1分未満から一晩かかるようになったのです）。 その理由は、実に単純です。Luauのサブタイピングアルゴリズムには、反射性（TはTのサブタイプである）を処理するための最適化が組み込まれており、これはコストの低いポインタの等価性チェックを行います。型正規化は、ポインタ上同一の型を、意味的には同等（ただしポインタ上同一ではない）な型に変換することがあり、これがパフォーマンスを著しく低下させます。
こうしたパフォーマンス上の問題があるため、我々は依然としてサブタイピングの最初のチェックとして構文的サブタイピングを使用し、構文的アルゴリズムが失敗した場合にのみ型正規化を実行しています。構文的サブタイピングは意味的サブタイピングに対する保守的な近似であるため、これは妥当な手法です。
実用的な意味論的サブタイピング
既成のセマンティックサブタイピングは、Luauで実装されているものとは若干異なります。なぜなら、既成のセマンティックサブタイピングではモデルが集合論的であることが求められ、それには関数型の要素が「関数のように振る舞う」ことが必要となるからです。私たちがこの要件を放棄した理由は2つあります。
第一に、我々は関数型を関数の交差集合へと正規化する。例えば、次のような関数の和集合や交差集合がごちゃ混ぜになった恐ろしい状態になる：
((number?) -> number?) | (((number) -> number) & ((string?) -> string?))オーバーロードされた関数に正規化されます：
((number) -> number?) & ((nil) -> (number | string)?)集合論的なセマンティックサブタイピングはこの正規化をサポートせず、代わりに関数を排他的標準形（関数の交差の和）に正規化します。私たちは、使い勝手の面からこれを行いません。オーバーロードされた関数はLuauでは慣用的な表現ですが、排他的標準形はそうではありません。また、ユーザーにそのような慣用的な表現ではない型を提示したくありません。
私たちの正規化は、関数型の和集合を書き換えることに依存しています：
((A) -> B) | ((C) -> D) → (A & C) -> (B | D)この正規化は、私たちのモデルでは妥当ですが、集合論的モデルでは妥当ではありません。
第二に、Luauにおいて、関数適用f(x)の型は、fの型が(A) -> Bであり、xの型がAである場合、Bとなります。 意外なことに、未使用の型が存在するため、集合論的モデルではこれが常に成り立つとは限りません。集合論的モデルにおいて、x の型が never である場合、f(x) の型は never となります。関数適用に特別な例外ケースが存在するという概念をユーザーに負担させることは望ましくありません。特に、その例外ケースはデッドコードでのみ発生し得るからです。
集合論的モデルでは、A や B がどのような値であっても、(never) -> A は (never) -> B のサブタイプとなります。しかし、Luau ではこれは成り立ちません。
これら2つの理由（これらは技術的な問題というよりは、主に使い勝手の問題である）から、集合論的な要件を放棄し、実用的な意味論的サブタイピングを採用する。
否定型
Luauの型システムと既成のセマンティックサブタイピングとのもう一つの違いは、Luauがすべての否定型をサポートしていない点です。
否定型が必要となる一般的なケースは、条件式の型チェックにおいてです：
-- initially x has type T
if type(x) == "string" then
-- in this branch x has type T & string
else
-- in this branch x has type T & ~string
endこれは、文字列ではない値で構成される否定型 `~string` を使用しています。
Luauでは、string、function、Partなどのテスト型に対してのみ、この種の型精緻化を許可しており、(A) -> Bのような構造型に対しては許可していません。これにより、一般的な否定型の一般的なケースを回避しています。
プロトタイピングと検証
Luauのセマンティックサブタイピングアルゴリズムの設計過程では、変更が加えられました（例えば、当初は集合論的サブタイピングを使用できると考えていました）。このような急速な変化の時期においては、迅速に反復開発を行うことが重要であったため、私たちは本番実装に直行するのではなく、まずプロトタイプを実装しました。
サブタイピングアルゴリズムには予期せぬエッジケースが存在し得るため、プロトタイプの検証は重要でした。このため、プロトタイピング言語としてAgdaを採用しました。Agdaはユニットテストだけでなく機械的検証もサポートしているため、設計に対して確信を持てています。
プロトタイプはLuauのすべてを実装しているわけではなく、関数型のサブセットのみですが、これだけで、本番環境では修正が困難なバグとして表面化したであろう、機能間の微妙な相互作用を発見するには十分でした。
プロトタイピングは完璧ではありません。例えば、本番環境で直面した主な問題はパフォーマンスとC++標準ライブラリに関するものでしたが、これらはプロトタイプでは決して検出できないものです。しかし、それ以外の点では、本番環境向けの実装は比較的単純でした（少なくとも、3,000行規模の変更としては単純な部類に入ります）。
今後の取り組み
セマンティックサブタイピングによって誤検知の原因の一つは解消されましたが、他にも追跡すべき問題が残っています：
- オーバーロードされた関数の呼び出しや演算子
- 複合型の式に対するプロパティへのアクセス
- テーブルの読み取り専用プロパティ
- 時間の経過とともに型が変化する変数（いわゆるタイプステート）
誤った赤線表示を排除する取り組みは続きます！
謝辞
本記事の草案に対して有益なコメントをくださったGiuseppe Castagna氏とBen Greenman氏に感謝します。
Alanは、Roblox Studioにおける開発機能の多くを支えるLuau型システムの設計と実装を統括しています。Dr. Jeffreyは、プログラミング言語の研究において30年以上の経験を持ち、数多くのオープンソースソフトウェアプロジェクトに積極的に参加しており、英国オックスフォード大学で博士号（DPhil）を取得しています。
