---
title: "Compile-Time Dependent Types"
slug: compile-time-dependent-types
url: https://listedarticles.com/articles/compile-time-dependent-types
canonical_url: https://thenumb.at/Syl-Intro/
content_type: blog_post
language: en
published_at: 2026-10-25T00:00:00.000Z
updated_at: 2026-10-27T23:14:42.254Z
author: "Max Slater"
author_url: https://thenumb.at/
authored_by: human
publisher: "thenumb.at"
publisher_url: https://thenumb.at/
topics: ["Programming Languages", "Compilers", "Systems Programming"]
license: all-rights-reserved
word_count: 2608
reading_minutes: 11
citation: "Max Slater, thenumb.at. \"Compile-Time Dependent Types.\" 25 Oct 2026. https://thenumb.at/Syl-Intro/ (all-rights-reserved)"
# The full text follows. The web page shows an extract and sends readers
# to the source above; quote the citation and link the canonical URL.
---

# Compile-Time Dependent Types

> Max Slater introduces Syl, a systems language that encodes compile-time computation in a modal type system inspired by two-level type theory and OxCaml: values carry staticity and erasure modes, enabling dependent types, proofs and totality checks, with examples like a typed interpreter and length-indexed vectors and planned extensions such as modules, reflection and user-defined layouts.

# Compile-Time Dependent Types

*Max Slater · October 25, 2026*

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](https://syl.dev/), 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](https://andraskovacs.github.io/pdfs/2ltt.pdf) [type theory](https://andraskovacs.github.io/pdfs/2ltt_icfp24.pdf), as well as plans for [OxCaml](https://oxcaml.org/).

*The Syl compiler may be found on [GitHub](https://github.com/TheNumbat/Syl).*

- [Modes](#modes)
- [Dependent Types](#dependent-types)
- [Examples](#examples)
- [Extensions](#extensions)
- [Everything Else](#everything-else)

---

## Modes

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](https://oxcaml.org/documentation/modes/intro/) to indicate whether a value is uniquely owned, may be written to, may be sent to another thread, etc.[1](#fn: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`.

- 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.[2](#fn: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, the body of `f true` is simply `print_int 0`, and likewise for `f false`.

---

## Dependent Types

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](#fn: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.

### Proofs

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](https://ncatlab.org/nlab/show/Burali-Forti%27s+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.[4](#fn:4)[5](#fn:5)

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

### Totality

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.

---

## Examples

### Typed Interpreter

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](#fn:6)

### Length-Indexed Vector

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

Then an addition function for `nat`s.

```
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 `nat`s 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).

---

## Extensions

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

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

```
singleton :
    erased (erased type -> erased type) as container ->
    erased type as element ->
    element ->
    container element
```

This example already works, but as written, all you can do with `container` is apply it.
We also need the ability to specify interfaces that connect types and values, leading to…

### Modules and Functors

Once Syl has [OxCaml-style modalities](https://oxcaml.org/documentation/modes/reference/#modalities)[7](#fn:7), you’ll be able to nest `erased`/`dynamic` values inside `unerased`/`static` values.
Then dependent records can take the place of ML-style modules:

```
let container = record {
  ty : erased type -> erased type @@ erased,
  create : erased type as element -> element -> ty element,
};;
```

Note `@@ erased` implies that all uses of `container.ty` see an `erased` value regardless of the erasure of `container`.
Now we can give `singleton` an implementable type:

```
singleton :
    static container as container ->
    erased type as element ->
    element ->
    container.ty element
```

Similarly, ML-style functors can be implemented as dependent functions:

```
fun pair (static c : container) : container = {
  ty = (fn (erased element : type) ->
         c.ty element ^ c.ty element),
  create = (fn (erased element : type) ->
             fn (e : element) ->
               c.create element e, c.create element e),
};;
```

Finally, with inferred arguments, records could provide most of the affordances of typeclasses or traits.

### Imports

We can even use static computation to describe how multi-file programs are built.
The compiler just has to provide the following functions:

```
import_sig : erased string -> erased type
import : erased string as path -> import_sig path
```

If 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.
In fact, these functions could just as easily take code strings, letting us generate code at compile time!

### Reflection

Syl already has rudimentary reflection via the built-in `repr` function, which returns metadata for a type.

```
fun print_ty (erased t : type) : unit =
  match erased repr t {
    .unit -> print "unit",
    .bool -> print "bool",
    .int -> print "int",
    _ -> unreachable,
  }
;;
```

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.

### User-Defined Layouts

While fairly speculative, I think we should be able to define and manipulate types’ runtime layouts at compile time.
With such a feature, users could safely describe interoperable niche optimizations, possibly in the style of [*Bit-Stealing Made Legal*](https://inria.hal.science/hal-04165615v1/document).
This would also require some notion of “unaddressable” fields that do not allow creating pointers to them.

---

## Everything Else

Syl’s design is far from complete.
In particular, it needs stories for mode polymorphism, lifetimes, linearity, implicit parameters, and proofs.
The compiler needs incremental compilation, useful error traces, and an LLVM backend.
I hope to share more thoughts on these areas in the future.

---

# Footnotes

---

1. In 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`
   until captured under a `dynamic` or `erased` modality. [↩︎](#fnref:1)
2. 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. [↩︎](#fnref:2)
3. This is the core idea of [*Staged Compilation with Two-Level Type Theory*](https://andraskovacs.github.io/pdfs/2ltt.pdf), though it’s not presented as a modal type system. [↩︎](#fnref:3)
4. This idea is formally explored in [*Irrelevance, Heterogeneous Equality, and Call-by-value Dependent Type Systems*](https://www.cis.upenn.edu/~sweirich/papers/msfp12prog.pdf). Thanks to Chris for proofreading this post! [↩︎](#fnref:4)
5. Syl does not yet have equality types, but once it does, erasure will provide a natural mechanism for forcing proof-producing computations when their results are needed. For example, `assert erased b` could establish `b = true` in the proof context by checking it reduces to `true`. [↩︎](#fnref:5)
6. This isn’t a fair comparison, but it’s better! [C++](https://godbolt.org/z/zP3Y9PjMG) / [Syl](https://pastebin.com/BNrfcP8B). [↩︎](#fnref:6)
7. There exist ideas on how to make such modalities inferrable, but I don’t understand them yet. [↩︎](#fnref:7)

---

*Originally published at [thenumb.at](https://thenumb.at/Syl-Intro/).*