Compile-Time Dependent Types

Compile-Time Dependent TypesIt seems inevitable that compile-time dependent types will come to systems programming.C++ has templates and constexpr. Rust has const generics. Zig has comptime. Even C has _Generic. However, these features tend to be highly restricted, lack a proper type system, or both.I’m working on Syl, a language which aims to encode compile-time computation in a modal type system. Syl is primarily inspired by András Kovács’ work on two-level type theory, as well as plans for OxCaml.The Syl compiler may be found on GitHub.ModesDependent TypesExamplesExtensionsEverything ElseModesIn Syl, all values have a mode along with a type. Modes describe properties of values independent of their types. For example, OxCaml uses modes to indicate whether a value is uniquely owned, may be written to, may be sent to another thread, etc.1Syl has two mode axes: staticity and erasure. On the staticity axis, a value may be either static or dynamic. On erasure, either erased or unerased.A static value is knowable at compile time; a dynamic value may not be.An unerased value is knowable at runtime; an erased value may not be.For example, literals are static unerased, since they are clearly knowable at both compile time and runtime. You can check by writing a mode annotation:let x = 0 @ static unerased;; Each mode axis has a sub-moding relation. If you have a static value, it’s safe to forget that it is knowable at compile time and hence treat it as dynamic. Similarly, an unerased value may be treated as erased. Mode annotations may “weaken” the mode, but not “strengthen” it:let x = 0 @ dynamic;; let y = x @ static;; ^^^^^^^^^^ Error: Expected a static expression, but got dynamic. As you might expect, branching on a dynamic value causes the result to be dynamic.let x = 0 @ dynamic;; let y = (if x == 0 then 1 else 2) @ static;; ^^^^^^^^^^^^^^^^^^^^^^^^ Error: Expected a static expression, but got dynamic. As long as they don’t capture or branch on dynamic values, functions preserve staticity.2let f = fn (x : int) -> x;; let x = (f 0) @ static;; let y = (f (1 @ dynamic)) @ static;; ^^^^^^^^^^^^^^^^^ Error: Expected a static expression, but got dynamic. Functions that return erased values are themselves erased, so cannot be applied at runtime.let f = fn (x : unit) -> 1 @ erased;; let g = f @ unerased;; ^ Error: Expected an unerased expression, but got erased. Now, what can we do with this information? When a value is knowable at compile time, surrounding code …