Max Slater · October 25, 2026
\nIt seems inevitable that compile-time dependent types will come to systems programming.
\nC++ has templates and constexpr. Rust has const generics. Zig has comptime. Even C has _Generic.\nHowever, 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.\nSyl is primarily inspired by András Kovács’ work on two-level type theory, as well as plans for OxCaml.
\nThe Syl compiler may be found on GitHub.
\n\nIn Syl, all values have a mode along with a type.\nModes describe properties of values independent of their types.\nFor example, OxCaml uses modes to indicate whether a value is uniquely owned, may be written to, may be sent to another thread, etc.1
\nSyl has two mode axes: staticity and erasure.\nOn the staticity axis, a value may be either static or dynamic.\nOn erasure, either erased or unerased.
static value is knowable at compile time; a dynamic value may not be.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.\nYou can check by writing a mode annotation:
let x = 0 @ static unerased;;Each mode axis has a sub-moding relation.\nIf you have a static value, it’s safe to forget that it is knowable at compile time and hence treat it as dynamic.\nSimilarly, an unerased value may be treated as erased.\nMode annotations may “weaken” the mode, but not “strengthen” it:
let x = 0 @ dynamic;;\n\nlet y = x @ static;;\n ^^^^^^^^^^\nError: 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;;\n\nlet y = (if x == 0 then 1 else 2) @ static;;\n ^^^^^^^^^^^^^^^^^^^^^^^^\nError: Expected a static expression, but got dynamic.As long as they don’t capture or branch on dynamic values, functions preserve staticity.2
let f = fn (x : int) -> x;;\n\nlet x = (f 0) @ static;;\n\nlet y = (f (1 @ dynamic)) @ static;;\n ^^^^^^^^^^^^^^^^^\nError: 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;;\n\nlet g = f @ unerased;;\n ^\nError: Expected an unerased expression, but got erased.Now, what can we do with this information?\nWhen a value is knowable at compile time, surrounding code can be monomorphized.\nFunctions of static parameters take advantage of this fact:
let f = fn (static x : bool) -> print_bool x;;Whenever we call f x, the compiler requires that both f and x have mode static.\nIf they do, it selects a particular implementation of f specialized to the value of x.\nConcretely, f true would call a function that hard-codes print_bool true, and likewise for f false.
In this example, we’re printing the value of x at runtime, so it needs to be unerased.\nThat’s often unnecessary: if x only determines how to compile the body of f, it can be erased.
let f = fn (erased x : bool) -> if erased x then print_int 0 else print_int 1;;Here, erased also implies static, so f will be specialized on x.\nThe if erased expression accepts a static erased condition and is guaranteed to resolve at compile time.\nTherefore, the body of f true is simply print_int 0, and likewise for f false.
On their own, the static and erased modes let us explicitly request specialization-based optimizations,\nbut they don’t give us dependent types. Functions of static arguments do.
let f = fn (erased x : bool) -> if erased x then 0 else true;;Here, if erased allows us to return an integer if x is true and a boolean otherwise.\nHence, f has a dependent function type, which encodes how the result type depends on the value of the input.
f : erased bool as x -> if erased x then int else boolNote ty as name gives the argument a name for use in the result.
Applications can then determine the correct result type by evaluating f’s type.
let x = (f true) : int;;\n\nlet y = (f false) : bool;;There is no distinct type grammar: type formers like -> and type annotations are normal expressions.\nint and bool are just erased values of type type, and abstracting over them gives us polymorphism.
let id = fn (erased t : type) -> fn (x : t) -> x;;\n\nlet x = id int 0;;\n\nlet y = id bool true;;As we saw above, functions of static arguments are monomorphized.\nAt runtime, id int refers to an identity function that directly operates on integers, and likewise for id bool.
That is, Syl is dependently typed at compile time and simply typed at runtime.3
\nstatic information.erased, so the runtime program cannot inspect types.Syl implements dependent typechecking similarly to existing languages, so we won’t discuss it in detail.\nHowever, the relationship between types and propositions in Syl differs from that of languages like Lean, Rocq, and Agda.
\nIn particular, Syl supports general recursion in compile time computations and gives type type type.\nAllowing either of these features implies that constructing an expression of type t does not prove the proposition corresponding to t.
For example, we can implement a function that ostensibly returns a value of any type:
\nlet magic =\n fn (erased t : type) ->\n fun loop (_ : unit) : t = loop () in\n loop ()\n;;Note magic could also be implemented using type : type via Girard’s paradox.
Despite having type erased type as t -> t, this function never actually produces a value—it’s an infinite loop.\nThe type describes what magic t would produce if it completed, but does not guarantee that it does.
Although this type system would not be suitable for a theorem proving language, it does not rule out type safety or even useful proofs.\nIt has two practical consequences:
\nIn return, we don’t need a totality checker (all static expressions may be used in types) or universe machinery (type-level programming is intuitive).
Because Syl is a programming language, the point of compilation is to produce a runtime artifact satisfying the invariants enforced by the type system.\nTherefore, we only care about invocations of dependent functions that actually occur during compilation—it’s fine for others to diverge.
\nStill, typechecking getting stuck during development is a poor user experience, so Syl also implements fuel limits.\nGiven competent compile-time debugging tools, I think this is reasonable.
\nfun f (erased _ : unit) : erased type = f ();;\n ^\nError: Recursion limit reached.\n\nlet x = 1 : f ();;Eschewing totality also means Syl can support explicitly partial functions at little additional cost.\nFor example, here’s a division function that statically checks the divisor is non-zero:
\nlet safe_div =\n fn (static d : int) ->\n if erased d != 0\n then fn (x : int) -> x / d\n else unreachable\n;;The unreachable keyword asserts that a branch does not appear in the runtime program.\nDuring dependent typechecking, the else branch is treated as a bottom value, so imposes no restrictions on the then branch.\nHowever, if else is reached while instantiating safe_div, we get an error:
...\n else unreachable\n ^^^^^^^^^^^\nError: Unreachable reached.\n;;\n\nlet x = safe_div 0 1;;Allowing partial functions reopens the door to inscrutable C++-style template instantiation errors.\nLuckily, explicit partiality means we can require users to provide error messages in unsupported cases, and combined with the lack of duck-typing at compile time, I think Syl can avoid most of the downsides.
\nThe following program does not require the full power of dependent types—it’s often used as a motivating example for GADTs in OCaml or Haskell—but I think the comparison is illustrative.
\nWe’ll start by defining a variant to use as an index.
\nlet sort = variant { int, bool };;Notes: Both sort and its constructors sort.int/sort.bool are normal values. Variants are unboxed.
Then a function to convert a sort to the corresponding type.
fun value (erased s : sort) : erased type =\n match erased s {\n .int -> int,\n .bool -> bool,\n }\n;;Note: like if erased, match erased allows an erased scrutinee and is resolved at compile time.
Next, an indexed expression type.\nThe type is literally a recursive function with a sort argument:
fun expr (erased s : sort) : erased type =\n match erased s {\n .int ->\n variant {\n lit : int,\n add : &(expr sort.int ^ expr sort.int),\n if_ : &(expr sort.bool ^ expr sort.int ^ expr sort.int),\n },\n .bool ->\n variant {\n lit : bool,\n eq : &(expr sort.int ^ expr sort.int),\n },\n }\n;;Notes: & represents an indirection. ^ is the tuple type former.
Finally, the interpreter.\nIn the .int branch, the compiler knows that only the int-returning constructors appear, and likewise for .bool.
fun eval (erased s : sort) : expr s -> value s =\n fn (e : expr s) ->\n match erased s {\n .int ->\n match e {\n .lit n -> n,\n .add &(left, right) -> eval sort.int left + eval sort.int right,\n .if_ &(condition, yes, no) ->\n if eval sort.bool condition then eval sort.int yes else eval sort.int no,\n },\n .bool ->\n match e {\n .lit b -> b,\n .eq &(left, right) -> eval sort.int left == eval sort.int right,\n },\n }\n;;Functions of static arguments are monomorphized and erased branches are eliminated, so the interpreter compiles to the same structure you’d expect from template specialization in C++.6
Warning: the syntax here needs a lot of work.
\nProper dependent types enable us to encode the length of lists in the type system.\nLet’s write an append function whose type shows that the output length is the sum of the input lengths.
While we could index our list by an int, Syl lacks tools for reasoning about signed, fixed-width integers.\nInstead, let’s define our own Peano nat type.
let nat =\n fun nat (erased _ : unit) : erased type =\n variant { zero, succ : &(nat ()) }\n in\n nat ()\n;;Note: there’s no let rec, so we define nat via a recursive function.
Then an addition function for nats.
fun add (static nm : nat ^ nat) : nat =\n match static nm {\n (.zero, m) -> m,\n (.succ &n, m) -> nat.succ box (add (n, m)),\n }\n;;Notes: match static is like match erased but does not erase the contents of the scrutinee. We should use erased everywhere, but variant constructors are not yet mode-polymorphic. If all nats were erased, the box indirection also wouldn’t be necessary.
Now the unboxed, length-indexed list.\nNote the lack of indirection.
\nfun vec (erased t : type) : erased (erased nat -> erased type) =\n fn (erased n : nat) ->\n match erased n {\n .zero -> variant { nil },\n .succ &n -> variant { cons : t ^ vec t n },\n }\n;;Finally, the append function.\nCrucially, the compiler is able to infer that the .cons case has the correct return type by unfolding add and vec.
fun append\n (erased t : type) : (static nat as n\n -> static nat as m\n -> vec t n\n -> vec t m\n -> vec t (add (n, m))) =\n fn (static n : nat) ->\n fn (static m : nat) ->\n fn (v1 : vec t n) ->\n fn (v2 : vec t m) ->\n match static n {\n .zero -> v2,\n .succ &n_minus_1 ->\n match v1 {\n .cons (x, xs) -> (vec t (add (n, m))).cons (x, append t n_minus_1 m xs v2),\n },\n }\n;;Notes: this is rather verbose since we don’t have n-ary function syntax. We also have to fully qualify the vec type .cons comes from because it’s not inferred yet.
As above, all lengths are known at compile time, so the runtime program has semantics akin to a constexpr length computation in C++ (though the unerased lengths may be materialized).
Many useful language features can be defined in user code using compile-time dependent types.\nHere are few promising (partially implemented) examples.
\nHigher-kinded types are just erased functions on types.\nYou can abstract over them like anything else.
singleton :\n erased (erased type -> erased type) as container ->\n erased type as element ->\n element ->\n container elementThis example already works, but as written, all you can do with container is apply it.\nWe also need the ability to specify interfaces that connect types and values, leading to…
Once Syl has OxCaml-style modalities7, you’ll be able to nest erased/dynamic values inside unerased/static values.\nThen dependent records can take the place of ML-style modules:
let container = record {\n ty : erased type -> erased type @@ erased,\n create : erased type as element -> element -> ty element,\n};;Note @@ erased implies that all uses of container.ty see an erased value regardless of the erasure of container.\nNow we can give singleton an implementable type:
singleton :\n static container as container ->\n erased type as element ->\n element ->\n container.ty elementSimilarly, ML-style functors can be implemented as dependent functions:
\nfun pair (static c : container) : container = {\n ty = (fn (erased element : type) ->\n c.ty element ^ c.ty element),\n create = (fn (erased element : type) ->\n fn (e : element) ->\n c.create element e, c.create element e),\n};;Finally, with inferred arguments, records could provide most of the affordances of typeclasses or traits.
\nWe can even use static computation to describe how multi-file programs are built.\nThe compiler just has to provide the following functions:
\nimport_sig : erased string -> erased type\nimport : erased string as path -> import_sig pathIf we treat file-level definitions as record fields, import_sig can infer a record type for a file and import can produce a value of that type.\nIn fact, these functions could just as easily take code strings, letting us generate code at compile time!
Syl already has rudimentary reflection via the built-in repr function, which returns metadata for a type.
fun print_ty (erased t : type) : unit =\n match erased repr t {\n .unit -> print "unit",\n .bool -> print "bool",\n .int -> print "int",\n _ -> unreachable,\n }\n;;This facility could be straightforwardly extended to allow inspecting the structure of types, which could then be used to implement typed Rust or OCaml-style derivers.
\nWhile fairly speculative, I think we should be able to define and manipulate types’ runtime layouts at compile time.\nWith such a feature, users could safely describe interoperable niche optimizations, possibly in the style of Bit-Stealing Made Legal.\nThis would also require some notion of “unaddressable” fields that do not allow creating pointers to them.
\nSyl’s design is far from complete.\nIn particular, it needs stories for mode polymorphism, lifetimes, linearity, implicit parameters, and proofs.\nThe compiler needs incremental compilation, useful error traces, and an LLVM backend.\nI hope to share more thoughts on these areas in the future.
\nIn the literature, modal type systems are presented in terms of modalities.
We will describe modes as they appear in OxCaml, but you can translate by thinking of all values as static unerased\n until captured under a dynamic or erased modality. ↩︎
Currently, staticity has modal axiom K, which allows staticity-preserving functions to operate
on dynamic arguments. I plan to replace the implicit application rule with mode polymorphism, which can also handle erasure. ↩︎
assert erased b could establish b = true in the proof context by checking it reduces to true. ↩︎Originally published at thenumb.at.
","headings":[{"level":1,"text":"Compile-Time Dependent Types","id":"compile-time-dependent-types"},{"level":2,"text":"Modes","id":"modes"},{"level":2,"text":"Dependent Types","id":"dependent-types"},{"level":3,"text":"Proofs","id":"proofs"},{"level":3,"text":"Totality","id":"totality"},{"level":2,"text":"Examples","id":"examples"},{"level":3,"text":"Typed Interpreter","id":"typed-interpreter"},{"level":3,"text":"Length-Indexed Vector","id":"length-indexed-vector"},{"level":2,"text":"Extensions","id":"extensions"},{"level":3,"text":"Higher-Kinded Types","id":"higher-kinded-types"},{"level":3,"text":"Modules and Functors","id":"modules-and-functors"},{"level":3,"text":"Imports","id":"imports"},{"level":3,"text":"Reflection","id":"reflection"},{"level":3,"text":"User-Defined Layouts","id":"user-defined-layouts"},{"level":2,"text":"Everything Else","id":"everything-else"},{"level":1,"text":"Footnotes","id":"footnotes"}]}}