30 points ibobev 4 days ago 5 comments
nextaccountic 58 minutes ago | parent
> 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)
Ericson2314 43 minutes ago | parent
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.
wahern 18 minutes ago | parent
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.