alt Hacker News> 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)
Replies
> Those language features are not examples of dependent types
They are dependent in the sense that types can depend on (compile-time) values, but indeed they're not conventionally dependent types. I mentioned them because they're popular features that can be implemented with compile-time dependent types.
> But I guess you mean that Syl implement dependent types them with no overhead, like no dictionary passing.
Yes. In 2LTT terms, the meta language is dependently typed, the object language is simply typed, and all types are erased at runtime.
Yeah I think this project could use a little guidance.
The real magic with types parameters is that they can both be dynamic and erased!
> That is, Syl is dependently typed at compile time and simply typed at runtime.
This is not full dependent types. And there is no reason to limit oneself this way for performance, because again dynamic + erased has no overhead.
> Those language features are not examples of dependent types, though...
Ironically C is the only language in that list with a dependent type. It's not _Generic, of course, but variable-length arrays (VLAs), which neither C++, Rust, nor Zig have.
> But dependent types (and static types in general) don't exist at runtime!
That isn't entirely true when it comes to dependent types and can be seen as a design choice. Types can depend on values and those values can often exist at runtime. Erasure only applies to parts we can determine are not computationally relevant.
For example `Vec n a`. The `n` is a natural number you may need at runtime, such as to get the length without walking the list. A dependent pair `Sigma(n : Nat). Vec n a` carries that `n` at runtime as ordinary data.
In fact many dependently typed languages have techniques, such as quantitative type theory, to assert what is needed at runtime.