コンパイル時依存型型

コンパイル時依存型型

コンパイル時依存型型がシステムプログラミングに導入されるのは避けられないように思われます。
C++にはテンプレートと constexpr があります。Rustにはconst genericsがあります。Zigにはcomptimeがあります。Cにさえ_Genericがあります。しかし、これらの機能はしばしば非常に制限的であったり、適切な型システムを欠いていたり、あるいはその両方であったりします。

私はSylという言語に取り組んでいます。これはモダル型システムでコンパイル時計算をエンコードすることを目指しています。Sylは主にAndrás Kovácsの二層型理論に関する研究、およびOxCamlの計画に触発されています。

SylコンパイラはGitHubで見つけることができます。

• モード
• 依存型
• 例
• 拡張機能
• その他すべて

---

モード

Sylでは、すべての値は型とともにモードを持ちます。モードは、型の型とは独立した値のプロパティを記述します。例えば、OxCamlはモードを使用して、値がユニークに所有されているか、書き込み可能か、別のスレッドに送信可能かなどを示します。1

Sylには2つのモード軸があります：静的性と消去性。静的性軸では、値はstaticまたはdynamicのいずれかです。消去性軸では、erasedまたはunerasedのいずれかです。

• static値はコンパイル時に知ることができます。dynamic値はそうではありません。
• unerased値は実行時に知ることができます。erased値はそうではありません。

例えば、リテラルはstatic unerasedです。なぜなら、それらはコンパイル時と実行時の両方で明らかに知ることができるからです。モード注釈を書いて確認できます。

let x = 0 @ static unerased;; 

各モード軸にはサブモージング関係があります。static値を持っている場合、それがコンパイル時に知ることができることを忘れて、それとして扱うのは安全です。同様に、unerased値はerasedとして扱うことができます。モード注釈はモードを「弱める」ことはできますが、「強化」することはできません。

let x = 0 @ dynamic;; 

let y = x @ static;; 
        ^^^^^^^^^^^^
Error: Expected a static expression, but got dynamic.

予想されるように、dynamic値での分岐は結果をdynamicにします。

let x = 0 @ dynamic;; 

let y = (if x == 0 then 1 else 2) @ static;; 
        ^^^^^^^^^^^^^^^^^^^^^^^^^
Error: Expected a static expression, but got dynamic.

dynamic値をキャプチャしたり分岐したりしない限り、関数は静的性を維持します。2

let f = fn (x : int) -> x;; 

let x = (f 0) @ static;; 

let y = (f (1 @ dynamic)) @ static;; 
        ^^^^^^^^^^^^^^^^^^^^^
Error: Expected a static expression, but got dynamic.

erased値を返す関数自体はerasedであるため、実行時に適用できません。

let f = fn (x : unit) -> 1 @ erased;; 

let g = f @ unerased;; 
        ^
Error: Expected an unerased expression, but got erased.

さて、この情報で何ができるでしょうか？値がコンパイル時に知ることができる場合、周囲のコードはモノモルフィゼーションされる可能性があります。staticパラメータの関数はこの事実に依存します。

let f = fn (static x : bool) -> print_bool x;; 

f xを呼び出すたびに、コンパイラはfとxの両方がstaticモードを持つことを要求します。それらがそうであれば、xの値に特化したfの実装を選択します。具体的には、f trueはprint_bool trueをハードコードする関数を呼び出し、f falseも同様です。

この例では、実行時にxの値を印刷しているため、unerasedである必要があります。それはしばしば不要です。もしxがfの本体をコンパイルする方法だけを決定する場合、それはerasedにすることができます。

let f = fn (erased x : bool) -> if erased x then print_int 0 else print_int 1;; 

ここでは、erasedはstaticも意味するため、fはxで特殊化されます。if erased式はstatic erased条件を受け入れ、コンパイル時に解決されることが保証されています。したがって、f trueはprint_int 0の本体を持つソケットを参照し、f falseも同様です。

---

依存型

それ自体では、staticとerasedモードは特殊化ベースの最適化を明示的に要求することを可能にしますが、依存型は提供しません。static引数の関数はそれらの事実を利用します。

let f = fn (erased x : bool) -> if erased x then 0 else true;; 

ここでは、if erasedにより、xがtrueの場合は整数を、それ以外の場合はブール値を返すことができます。したがって、fは結果の型が入力の値にどのように依存するかをエンコードする、依存関数型を持ちます。

f : erased bool as x -> if erased x then int else bool

ty as nameは引数に名前を与え、結果で使用できるようにします。

アプリケーションは、fの型を評価することで正しい結果型を決定できます。

let x = (f true) : int;; 

let y = (f false) : bool;; 

型文法は区別されません。->のような型構成子や型注釈は通常の式です。intとboolは単にtypeのerased値であり、それらを抽象化すると多相性が得られます。

let id = fn (erased t : type) -> fn (x : t) -> x;; 

let x = id int 0;; 

let y = id bool true;; 

前述のように、static引数の関数はモノモルフィゼーションされ、実行時にはid intは整数を直接操作する恒等関数を参照し、id boolも同様です。

つまり、Sylはコンパイル時には依存型であり、実行時には単純型です。3

• ランタイムプログラムの形状を決定する構造はstatic情報を必要とします。

• 型は常にerasedであるため、ランタイムプログラムは型を検査できません。

Sylは既存の言語と同様に依存型チェックを実装しているため、詳細については説明しません。しかし、型と命題の関係は、Lean、Rocq、Agdaのような言語とは異なります。

証明

特に、Sylはコンパイル時計算で一般再帰をサポートし、type型にtypeを与えます。これらの機能のいずれかを許可すると、型tの式を構築することが、tに対応する命題を証明することにならないことになります。

例えば、あらゆる型の値を持つように見える関数を実装できます。

let magic = 
  fn (erased t : type) -> 
    fun loop (_ : unit) : t = loop () in 
    loop () 
;; 

magicはジラールのパラドックスを介してtype : typeを使用して実装することもできます。

erased type as t -> tという型を持つにもかかわらず、この関数は実際には値を生成しません。無限ループです。型はmagic tが完了した場合に生成されるものを記述しますが、それが完了することを保証しません。

この型システムは定理証明言語には適していませんが、型安全性や有用な証明を排除するものではありません。実用的な結果は2つあります。

• 型レベル計算で使用される関数は発散する可能性があるため、型チェックは決定可能ではありません。

• 関数は普遍的に量化された主張を解消しないため、コンパイラは証明を生成するすべてのアプリケーションを、それらの結果に依存する前に評価する必要があります。45

その見返りに、全域性チェッカー（すべてのstatic式は型で使用できる）や宇宙機械（型レベルプログラミングは直感的）を必要としません。

全域性

Sylはプログラミング言語であるため、コンパイルの目的は、型システムによって強制される不変条件を満たすランタイム成果物を生成することです。したがって、コンパイル中に実際に発生する依存関数の呼び出しのみを気にします。他のものが発散しても構いません。

それでも、開発中に型チェックが停止するのはユーザーエクスペリエンスが悪いため、Sylは燃料制限も実装しています。有能なコンパイル時デバッグツールがあれば、これは妥当だと考えます。

fun f (erased _ : unit) : erased type = f ();; 
                                        ^
Error: Recursion limit reached.

let x = 1 : f ();; 

全域性を回避することは、Sylが追加コストなしで明示的に部分関数をサポートできることも意味します。例えば、除数がゼロでないことを静的にチェックする除算関数を次に示します。

let safe_div = 
  fn (static d : int) -> 
    if erased d != 0 
    then fn (x : int) -> x / d 
    else unreachable 
;; 

unreachableキーワードは、分岐がランタイムプログラムに現れないことを主張します。依存型チェック中、else分岐はボトム値として扱われるため、then分岐に制約を課しません。しかし、safe_divをインスタンス化する際にelseに到達すると、エラーが発生します。

    ... 
    else unreachable 
         ^^^^^^^^^^^
Error: Unreachable reached.
;; 

let x = safe_div 0 1;; 

部分関数を許可すると、不可解なC++スタイルのテンプレートインスタント化エラーのドアが再び開きます。幸いなことに、明示的な部分性により、サポートされていないケースでエラーメッセージを提供するようにユーザーに要求できます。また、コンパイル時のダックタイピングの欠如と組み合わせることで、Sylはほとんどの欠点を回避できると考えています。

---

例

型付きインタープリター

次のプログラムは、依存型の完全な力を必要としません。これは、OCamlやHaskellのGADTsの動機付けの例としてよく使用されますが、比較は示唆的だと思います。

まず、インデックスとして使用するバリアントを定義します。

let sort = variant { int, bool };; 

注：sortとそのコンストラクタsort.int/sort.boolはどちらも通常の値です。バリアントはアンボックスです。

次に、sortを対応する型に変換する関数です。

fun value (erased s : sort) : erased type = 
  match erased s { 
    .int -> int, 
    .bool -> bool, 
  } 
;; 

注：if erasedと同様に、match erasedはerasedの被検査値を受け入れ、コンパイル時に解決されます。

次に、インデックス付き式型。この型は、sort引数を持つ再帰関数そのものです。

fun expr (erased s : sort) : erased type = 
  match erased s { 
    .int -> 
      variant { 
        lit : int, 
        add : &(expr sort.int ^ expr sort.int), 
        if_ : &(expr sort.bool ^ expr sort.int ^ expr sort.int), 
      }, 
    .bool -> 
      variant { 
        lit : bool, 
        eq : &(expr sort.int ^ expr sort.int), 
      }, 
  } 
;; 

注：&は間接参照を表します。^はタプル型構成子です。

最後に、インタープリターです。.int分岐では、コンパイラはintを返すコンストラクタのみが現れることを知っており、.boolも同様です。

fun eval (erased s : sort) : expr s -> value s = 
  fn (e : expr s) -> 
    match erased s { 
      .int -> 
        match e { 
          .lit n -> n, 
          .add &(left, right) -> eval sort.int left + eval sort.int right, 
          .if_ &(condition, yes, no) -> 
            if eval sort.bool condition then eval sort.int yes else eval sort.int no, 
        }, 
      .bool -> 
        match e { 
          .lit b -> b, 
          .eq &(left, right) -> eval sort.int left == eval sort.int right, 
        }, 
    } 
;; 

static引数の関数はモノモルフィゼーションされ、erased分岐は削除されるため、インタープリターはC++のテンプレート特殊化から期待される構造と同じ構造にコンパイルされます。6

長さインデックス付きベクトル

警告：ここでの構文は多くの作業が必要です。

真の依存型により、リストの長さを型システムにエンコードできます。出力長が入力の長さの合計であることを示す型を持つappend関数を記述しましょう。

リストをintでインデックス付けすることもできますが、Sylには符号付き固定幅整数を推論するツールがありません。代わりに、独自のPeano nat型を定義しましょう。

let nat = 
  fun nat (erased _ : unit) : erased type = 
    variant { zero, succ : &(nat ()) } 
  in 
  nat () 
;; 

注：let recがないため、再帰関数を介してnatを定義します。

次にnatの加算関数です。

fun add (static nm : nat ^ nat) : nat = 
  match static nm { 
    (.zero, m) -> m, 
    (.succ &n, m) -> nat.succ box (add (n, m)), 
  } 
;; 

注：match staticはmatch erasedに似ていますが、被検査値の内容を消去しません。すべてのnatが消去された場合、boxの間接参照も不要になります。

次に、アンボックスで長さインデックス付きリストです。間接参照がないことに注意してください。

fun vec (erased t : type) : erased (erased nat -> erased type) = 
  fn (erased n : nat) -> 
    match erased n { 
      .zero -> variant { nil }, 
      .succ &n -> variant { cons : t ^ vec t n }, 
    } 
;; 

最後に、append関数です。決定的なのは、コンパイラがaddとvecを展開することで、.consケースが正しい戻り型を持つことを推論できることです。

fun append 
  (erased t : type) : (static nat as n 
                         -> static nat as m 
                         -> vec t n 
                         -> vec t m 
                         -> vec t (add (n, m))) = 
  fn (static n : nat) -> 
    fn (static m : nat) -> 
      fn (v1 : vec t n) -> 
        fn (v2 : vec t m) -> 
          match static n { 
            .zero -> v2, 
            .succ &n_minus_1 -> 
              match v1 { 
                .cons (x, xs) -> (vec t (add (n, m))).cons (x, append t n_minus_1 m xs v2), 
              }, 
          } 
;; 

注：n項関数構文がないため、これは非常に冗長です。推論されていないため、.consが発生するvec型を完全に修飾する必要もあります。

上記のように、すべての長さはコンパイル時にわかっているため、ランタイムプログラムはC++のconstexpr長さ計算に似たセマンティクスを持ちます（ただし、unerased長さは具体化される場合があります）。

---

拡張機能

多くの有用な言語機能は、コンパイル時依存型を使用してユーザーコードで定義できます。ここでは、有望な（部分的に実装された）例をいくつか示します。

高階型

高階型は、型に対するerased関数にすぎません。他のものと同様に抽象化できます。

singleton :
    erased (erased type -> erased type) as container ->
    erased type as element ->
    element ->
    container element

この例はすでに機能していますが、書かれたとおり、containerに対してできることは適用することだけです。また、型と値をつなぐインターフェースを指定する能力も必要です。これは…につながります。

モジュールとファンクタ

SylがOxCamlスタイルのモダリティ7を持つようになると、erased/dynamic値をunerased/static値の中にネストできるようになります。その後、依存レコードがMLスタイルのモジュールの代わりになります。

let container = record {
  ty : erased type -> erased type @@ erased,
  create : erased type as element -> element -> ty element,
};;

@@ erasedは、container.tyのすべての使用が、containerの消去性に関係なく、erased値を見ることを意味します。これで、singletonに実装可能な型を与えることができます。

singleton :
    static container as container ->
    erased type as element ->
    element ->
    container.ty element

同様に、MLスタイルのファンクタは依存関数として実装できます。

fun pair (static c : container) : container = {
  ty = (fn (erased element : type) ->
         c.ty element ^ c.ty element),
  create = (fn (erased element : type) ->
             fn (e : element) ->
               c.create element e, c.create element e),
};;

最後に、推論される引数により、レコードは型クラスまたはトレイトのほとんどの機能を提供できます。

インポート

静的計算を使用して、マルチファイルプログラムがどのように構築されるかを記述することさえできます。コンパイラは次の関数を提供するだけで済みます。

import_sig : erased string -> erased type
import : erased string as path -> import_sig path

ファイルレベルの定義をレコードフィールドとして扱う場合、import_sigはファイルのレコード型を推論でき、importはその型の値を生成できます。実際、これらの関数はコード文字列を受け取ることもできるため、コンパイル時にコードを生成できます！

リフレクション

Sylには、型のメタデータを返す組み込みのrepr関数を介して、すでに初歩的なリフレクションがあります。

fun print_ty (erased t : type) : unit = 
  match erased repr t {
    .unit -> print "unit",
    .bool -> print "bool",
    .int -> print "int",
    _ -> unreachable,
  }
;; 

この機能は、型の構造を検査できるように簡単に拡張でき、それを使用して型付きRustまたはOCamlスタイルのデリバーを実装できます。

ユーザー定義レイアウト

かなり推測的ですが、コンパイル時に型のランタイムレイアウトを定義および操作できるはずだと考えています。このような機能があれば、ユーザーは相互運用可能なニッチな最適化を安全に記述できる可能性があります。おそらくBit-Stealing Made Legalのスタイルで。これには、「アドレス指定不可能な」フィールドの概念も必要になります。これは、それらへのポインタを作成できないフィールドです。

---

その他すべて

Sylの設計は完成にはほど遠いです。特に、モード多相性、ライフタイム、線形性、暗黙的パラメータ、証明のストーリーが必要です。コンパイラには、増分コンパイル、有用なエラートレース、LLVMバックエンドが必要です。将来的には、これらの分野に関するさらに多くの考えを共有できることを願っています。

---

注釈

---

1. 文献では、モダル型システムはモダリティの観点から提示されます。OxCamlに現れるモードとして説明しますが、すべての値をstatic unerasedとして考え、dynamicまたはerasedモダリティの下でキャプチャされるまで、それらを翻訳できます。↩︎

2. 現在、静的性にはモダリティ公理Kがあり、静的性を維持する関数が動的引数で動作することを許可します。暗黙的な適用規則をモード多相性に置き換える予定であり、これも消去性を処理できます。↩︎

3. これはStaged Compilation with Two-Level Type Theoryの核心的なアイデアですが、モダル型システムとしては提示されていません。↩︎

4. このアイデアはIrrelevance, Heterogeneous Equality, and Call-by-value Dependent Type Systemsで形式的に探求されています。Chrisにこの投稿の校正を依頼しました！↩︎

5. Sylはまだ等価型を持っていませんが、一度持つようになると、消去性は証明生成計算の結果が必要なときに強制するための自然なメカニズムを提供します。例えば、assert erased bは、それがtrueに還元されることをチェックすることにより、証明コンテキストでb = trueを確立できます。↩︎

6. これは公平な比較ではありませんが、より良いものです！C++ / Syl。↩︎

7. そのようなモダリティを推論可能にする方法についてのアイデアは存在しますが、まだ理解していません。↩︎

2026年10月25日に記述

---