Compile-Time Dependent Types

> Compile-Time Dependent Types

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

Those language features are not examples of dependent types, though...

> That is, Syl is dependently typed at compile time and simply typed at runtime.

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

But dependent types (and static types in general) don't exist at runtime!

But I guess you mean that Syl implement dependent types them with no overhead, like no dictionary passing. So you can have full type erasure. Is that accurate? (will read the paper)

very cool! ive a long running back burner project that overlaps in the same design and influence space, but takes it in a very different direction

I wonder how well LTO optimizes for these sorts of things, vs doing all of the legwork to compile-time resolve polymorphic functions and objects.