Rendered at 19:45:26 GMT+0000 (Coordinated Universal Time) with Cloudflare Workers.
nextaccountic 3 hours ago [-]
> 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.
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)
solomonb 2 hours ago [-]
> 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.
mkehrt 41 minutes ago [-]
You've exactly described the answer, but to people who don't know much about dependent types, this may be a little unclear. The point is that there are two sorts of dependent types.
When people who don't know much about them think of dependent types, they are probably thinking of functions, which can take a value on the left hand side to be used in the type on the right. Confusingly, these are normally called "dependent products" in the type theory. However since this is confusing and they are generally written with a capital Pi, they are often just referred to as "Pis". For example
Pi x:nat . Vec x string
is a function that takes a nat (non-negative number) and returns a Vector whose length is that nat and which is encoded in the type.
On the other hand, you are talking about pairs (confusingly: "dependent sums", here "sum" being something like a union/enum in type theory), often called "Sigmas". These are pairs (2-tuples) of values in which the type of the second value depends on the value of the first. So, your example, a pair where the vector length is held in the first element and the vector itself in the second. In this contrived example, Vector may not know its own length at runtime, so we need to package them up together.
Sigma x: nat . Vec x string
These are both "dependent types", but people who are only passingly familiar with them might mostly know about the first.
(Why are functions "dependent products" and pairs "dependent sums"? I've never understood this but I've heard hand-wavy explanations that infintitary products are functions and infinitary sums are products ¯\(ツ)/¯)
TheNumbat 2 hours ago [-]
> 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.
wahern 2 hours ago [-]
> 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.
Someone 27 minutes ago [-]
C also ‘supports’ fixed-length arrays. You can write
That was basically Dennis Ritchies' proposal as well: Dennis Ritchie, Variable-Size Arrays in C, September 1990, http://jclt.iecc.com/Jct22.pdf#page=5
IIRC, one of the problems there is how to generalize it to, e.g., struct members. (Maybe you can speak to that.) The approach adopted by C99[1], being based on dependent typing, was I think better conceptually. But despite dependent typing being awesome, it manifestly was and still remains a tough sell to compiler implementors, so VLAs/VMTs have languished in C and have yet to be fully developed. I think I'd agree C would have been better off with the approach you suggest. Adoption likely would have been quicker, and it could have been implemented in full almost immediately.[2] The consolation prize is that hopefully C will soon see some progression on the VMT front, specifically the proposals under discussion on the committee for forward-referencing in function parameter VMTs and VMT struct array members. The final piece of that puzzle would be addressing the scary syntax for VLA passing, which feels error prone (C2y countof operator semantics help a little bit).
[2] Ironically GCC already had nascent VLA support, which may have helped nudge the C99 committee toward that instead of adopting Ritchie's approach. But the fat pointer approach has a more obvious and straight-forward implementation.
Ericson2314 3 hours ago [-]
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.
TheNumbat 1 hours ago [-]
> And there is no reason to limit oneself this way for performance, because again dynamic + erased has no overhead.
Not entirely, since Syl uses static data to describe types' runtime layout. Allowing dynamic there would require overhead (e.g. a uniform representation).
That said, there's not a good reason to prevent types from ever mentioning dynamic values. I didn't include it in the post as I haven't entirely thought it through, but with OxCaml-style modalities, you should be able to mention runtime data in types under a dynamic modality.
carterschonwald 2 hours ago [-]
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 4 hours ago [-]
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.
uecker 3 hours ago [-]
In my experience, compilers are very good at this.
> 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)
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.
When people who don't know much about them think of dependent types, they are probably thinking of functions, which can take a value on the left hand side to be used in the type on the right. Confusingly, these are normally called "dependent products" in the type theory. However since this is confusing and they are generally written with a capital Pi, they are often just referred to as "Pis". For example
is a function that takes a nat (non-negative number) and returns a Vector whose length is that nat and which is encoded in the type.On the other hand, you are talking about pairs (confusingly: "dependent sums", here "sum" being something like a union/enum in type theory), often called "Sigmas". These are pairs (2-tuples) of values in which the type of the second value depends on the value of the first. So, your example, a pair where the vector length is held in the first element and the vector itself in the second. In this contrived example, Vector may not know its own length at runtime, so we need to package them up together.
These are both "dependent types", but people who are only passingly familiar with them might mostly know about the first.(Why are functions "dependent products" and pairs "dependent sums"? I've never understood this but I've heard hand-wavy explanations that infintitary products are functions and infinitary sums are products ¯\(ツ)/¯)
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.
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.
C VLAs are a terribly clumsy design. Here's the right way to do it in C:
https://www.digitalmars.com/articles/C-biggest-mistake.html
IIRC, one of the problems there is how to generalize it to, e.g., struct members. (Maybe you can speak to that.) The approach adopted by C99[1], being based on dependent typing, was I think better conceptually. But despite dependent typing being awesome, it manifestly was and still remains a tough sell to compiler implementors, so VLAs/VMTs have languished in C and have yet to be fully developed. I think I'd agree C would have been better off with the approach you suggest. Adoption likely would have been quicker, and it could have been implemented in full almost immediately.[2] The consolation prize is that hopefully C will soon see some progression on the VMT front, specifically the proposals under discussion on the committee for forward-referencing in function parameter VMTs and VMT struct array members. The final piece of that puzzle would be addressing the scary syntax for VLA passing, which feels error prone (C2y countof operator semantics help a little bit).
[1] Tom MacDonald, Variable Length Arrays, December 1989, http://jclt.iecc.com/Jct13.pdf#page=67
[2] Ironically GCC already had nascent VLA support, which may have helped nudge the C99 committee toward that instead of adopting Ritchie's approach. But the fat pointer approach has a more obvious and straight-forward implementation.
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.
Not entirely, since Syl uses static data to describe types' runtime layout. Allowing dynamic there would require overhead (e.g. a uniform representation).
That said, there's not a good reason to prevent types from ever mentioning dynamic values. I didn't include it in the post as I haven't entirely thought it through, but with OxCaml-style modalities, you should be able to mention runtime data in types under a dynamic modality.