> Compile-Time Dependent Types<p>> 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.<p>Those language features are not examples of dependent types, though...<p>> That is, Syl is dependently typed at compile time and simply typed at runtime.<p>> This is the core idea of Staged Compilation with Two-Level Type Theory <a href="https://andraskovacs.github.io/pdfs/2ltt.pdf" rel="nofollow">https://andraskovacs.github.io/pdfs/2ltt.pdf</a> though it’s not presented as a modal type system.<p>But dependent types (and static types in general) don't exist at runtime!<p>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)
Yeah I think this project could use a little guidance.<p>The real magic with types parameters is that they can both be dynamic and erased!<p>> That is, Syl is dependently typed at compile time and simply typed at runtime.<p>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.