Syl Explores Compile-Time Dependent Types With a Modal Type System
A developer's experimental language, Syl, aims to bring dependent types to systems programming by encoding compile-time computation in a modal type system.
The author argues that compile-time dependent types are likely to reach systems programming. Existing tools such as C++ templates and constexpr, Rust's const generics, Zig's comptime, and C's _Generic are described as highly restricted or lacking a proper type system.
Syl, the language under development, gives every value a mode along with a type. It has two mode axes: staticity, which marks whether a value is knowable at compile time, and erasure, which marks whether it is knowable at runtime. Static values can be specialized through monomorphization, and types are erased at runtime, so the program is dependently typed at compile time but simply typed at runtime. The design is inspired by András Kovács's work on two-level type theory and by plans for OxCaml.
Unlike proof-oriented languages such as Lean, Rocq, and Agda, Syl supports general recursion in compile-time code and allows type : type. As a result, typechecking may not terminate, and the compiler uses fuel limits to stop runaway evaluation. The author notes that this trade-off suits a programming language rather than a theorem prover.
The article includes examples such as a typed interpreter and a length-indexed vector, and the author acknowledges that the vector syntax still needs considerable work.
