Compile-Time Dependent Types

Syl is a proposed systems programming language that treats compile-time computation as part of a modal type system. Every value has two independent mode properties: static or dynamic, indicating whether it is known during compilation, and erased or unerased, indicating whether it exists at runtime. Static values can drive specialization; erased values disappear from the runtime program. Functions of static inputs are monomorphized, while erased inputs can determine a function’s result type without being retained. Types themselves are erased, so Syl’s dependent typing operates at compile time and its runtime programs remain simply typed.

The design permits general recursion in compile-time computations and does not require totality checking or a separate hierarchy of universes. This makes type-level programming more flexible, but typechecking can diverge, and a function’s type alone does not prove that it will produce a value. The compiler therefore evaluates proof-producing applications before trusting their results and uses recursion limits to catch stuck computations. Explicitly partial functions can reject unsupported compile-time cases with targeted errors. Demonstrations include a typed interpreter whose indexed cases are specialized away, and length-indexed vectors with an append function whose output type records the sum of input lengths. These examples show how dependent types can express structural guarantees while compiling to specialized runtime code.