Syl brings compile-time dependent types to systems programming
C++ has templates, Rust has const generics, Zig has comptime — but all are restricted or lack a real type system. Syl is a new language that encodes compile-time computation in a modal type system inspired by two-level type theory and OxCaml. Values carry modes for staticity and erasure, letting the compiler monomorphize static arguments while keeping runtime code simply typed. The trade-off: typechecking isn't decidable, so Syl uses fuel limits instead of a totality checker.
That is, Syl is dependently typed at compile time and simply typed at runtime.
- nextaccountic
> 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)
- carterschonwald
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
- superxpro12
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.