Compile-time dependent types in the Syl programming language

It 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.

In 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.1

Syl 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.

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.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.

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 can be monomorphized. Functions 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. If they do, it selects a particular implementation of f specialized to the value of x. Concretely, 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. That’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. The if erased expression accepts a static erased condition and is guaranteed to resolve at compile time. Therefore, f true refers to a thunk with the body print_int 0, and likewise for f false.

On their own, the static and erased modes let us explicitly request specialization-based optimizations, but 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. Hence, 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 bool

Note 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;;

let y = (f false) : bool;;

There is no distinct type grammar: type formers like -> and type annotations are normal expressions. int 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;;

let x = id int 0;;

let y = id bool true;;

As we saw above, functions of static arguments are monomorphized. At 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

Constructs that determine the shape of the runtime program require static information.

Types are always erased, so the runtime program cannot inspect types.

Syl implements dependent typechecking similarly to existing languages, so we won’t discuss it in detail. However, the relationship between types and propositions in Syl differs from that of languages like Lean, Rocq, and Agda.

In particular, Syl supports general recursion in compile time computations and gives type type type. Allowing 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:

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

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. The 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. It has two practical consequences:

Functions used in type-level computations may diverge, so typechecking is not decidable.

Functions don’t discharge universally quantified claims, so the compiler must evaluate all applications that produce proofs before relying on their results.45

In 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. Therefore, we only care about invocations of dependent functions that actually occur during compilation—it’s fine for others to diverge.

Still, typechecking getting stuck during development is a poor user experience, so Syl also implements fuel limits. Given competent compile-time debugging tools, I think this is reasonable.

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

let x = 1 : f ();;

Eschewing totality also means Syl can support explicitly partial functions at little additional cost. For example, here’s a division function that statically checks the divisor is non-zero:

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

The unreachable keyword asserts that a branch does not appear in the runtime program. During dependent typechecking, the else branch is treated as a bottom value, so imposes no restrictions on the then branch. However, if else is reached while instantiating safe_div, we get an error:

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

let x = safe_div 0 1;;

Allowing partial functions reopens the door to inscrutable C++-style template instantiation errors. Luckily, 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.

The 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.

We’ll start by defining a variant to use as an index.

let 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 = match erased s { .int -> int, .bool -> bool, } ;;

Note: like if erased, match erased allows an erased scrutinee and is resolved at compile time.

Next, an indexed expression type. The type is literally a recursive function with a sort argument:

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), }, } ;;

Notes: & represents an indirection. ^ is the tuple type former.

Finally, the interpreter. In 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 = 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, }, } ;;

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.

Proper dependent types enable us to encode the length of lists in the type system. Let’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. Instead, let’s define our own Peano nat type.

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

Note: there’s no let rec, so we define nat via a recursive function.

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

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. Note the lack of indirection.

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 }, } ;;

Finally, the append function. Crucially, the compiler is able to infer that the .cons case has the correct return type by unfolding add and vec.

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), }, } ;;

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. Here are few promising (partially implemented) examples.

Higher-kinded types are just erased functions on types. You can abstract over them like anything else.

singleton : erased (erased type