> 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)
> 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.
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 ¯\(ツ)/¯)
Pairs in general (ie binary products) are always sums. A pair type `X * Y` is a multiplication, which is equivalent to `enum {Y y_x0,Y y_x1,Y y_x2,...}` or `Y + Y + Y + ...`, effectively a sum type where the descriminant of the enum is a X, and each case of the enum contains a Y. This is equivalent to how 3 * 7 = 7 + 7 + 7, where you have three terms of size seven.
Similarly, functions in general (ie (binary) exponentiations) are always products. A function type `X -> Y` (or `Y ^ X`) is a exponentiation, which is equivalent to `struct {Y y_x0,Y y_x1,Y y_x2,...}` or `Y * Y * Y * ...`, effectively a product (or latent array) type where the index of the 'array' is a X, and each element of the 'array' is a Y. This is equivalent to how 7 ^ 3 = 7 * 7 * 7, where you have three factors of size seven. (Note that functions have the exponent/argument first and the base/result second.)
All of the above applies without dependent types. Dependent types let the `Y` type depend on which value of type X is involved. (That is, the Y type depends on the X value.)
> 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.
> Not entirely, since Syl uses static data to describe types' runtime layout. Allowing dynamic there would require overhead (e.g. a uniform representation).
This is where it is crucial to distinguish types from layouts. "uniform representation" means the layout is static while the type is dynamic. But this isn't an overhead in the sense of dynamic checks or lack of erasure.
Having static (erased) layout parameter and dynamic (erased) type parameter is the fully-general solution: monomorphization per layout, not type. And the caller decided whether to thread a layout parameter, or fix a single layout.
- OOP is existential types where the layouts share some sort of shared prefix (e.g. pointer to vtable, fields in common, etc.). To accurately model such things (and they occur in FFI), you need to separate types from layout, and hold the "supertype's layout" fixed.
- A classic use-case of dependent types is dynamically-sized arrays, and "tensors". When you have a pair (L: Nat, V: Pointer(Array(N, T))), you have a layout behind the pointer that is dynamic, but you don't want to conflate this with arbitrary types of the pointee.
Failure to deal with this in fully generality will force you to go down Rust's path of ad-hoc arrays and "dyn trait", which is actually more complexity.
I think those can be modeled without explicitly separating layouts from types (not that doing so is necessarily a bad idea).
For arrays:
let dyn_array = fn (erased t : type) -> record { len : int @@ dynamic, data : pointer(array(len, t)) }
For "dyn trait":
let vtable = fn (erased t : type) -> record { print : pointer(t) -> string, ... }
let dyn_print = record { t : type @@ dynamic erased, vtable : pointer(vtable(t)), data : pointer(t) }
Both use dependent records and the dynamic modality I mentioned above. dyn_print doesn't match C++ since it doesn't inline the data, and giving that a static layout would require parameterizing on the layout of t, so I see your point. However, it might be fine to give dyn_print an "incomplete" layout that can only appear behind a pointer.
> 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.
> 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.
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.
That particular syntax has far too many caveats to be safely employed, IMO. It would be better to use variably-modified types (VMTs), which currently is more-or-less[1] a pointer to a VLA:
int foo(int (*bar)[10])
In particular, sizeof(*bar) and (in C2y) countof(*bar) will do the correct thing. But you need to dereference bar almost every to use it properly, and unfortunately sizeof(bar) instead of sizeof(*bar) will compile cleanly, though countof(bar) is guaranteed to fail.
The dilemma is C's array to pointer decaying semantics. C2y will try to roll that back somewhat (a[i] will no longer be identical to i[a] via the a[i] == a + i == i + a transitive relation), but there's only so much you can do in that regard, especially for array passing, without new syntax or silently breaking alot of valid, proper, carefully written C code. There's too much that can fall through the cracks by relying on non-standard compiler heuristics to substitute for proper typing.
[1] Strictly speaking a VLA can only be created as automatic storage objects, but a VMT can type dynamically allocated (malloc'd) memory. But the syntax looks like a pointer to a VLA because it originates from the need to pass actual VLAs as parameters.
> 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 ¯\(ツ)/¯)
Similarly, functions in general (ie (binary) exponentiations) are always products. A function type `X -> Y` (or `Y ^ X`) is a exponentiation, which is equivalent to `struct {Y y_x0,Y y_x1,Y y_x2,...}` or `Y * Y * Y * ...`, effectively a product (or latent array) type where the index of the 'array' is a X, and each element of the 'array' is a Y. This is equivalent to how 7 ^ 3 = 7 * 7 * 7, where you have three factors of size seven. (Note that functions have the exponent/argument first and the base/result second.)
All of the above applies without dependent types. Dependent types let the `Y` type depend on which value of type X is involved. (That is, the Y type depends on the X value.)
(Bool->Bool,Uint8+()) is just a verbose way of saying (2^2 * (256+1)), where 1,2, and 256 are types with the appropriate number of elements.
The cases involving infinite types are just a (straightforward?) generalization of that.
0: eg 0=noreturn [1],1=void,2=Bool,256=uint8_t
1: Much like in set theory, zero is the empty set.
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.
This is where it is crucial to distinguish types from layouts. "uniform representation" means the layout is static while the type is dynamic. But this isn't an overhead in the sense of dynamic checks or lack of erasure.
Having static (erased) layout parameter and dynamic (erased) type parameter is the fully-general solution: monomorphization per layout, not type. And the caller decided whether to thread a layout parameter, or fix a single layout.
- OOP is existential types where the layouts share some sort of shared prefix (e.g. pointer to vtable, fields in common, etc.). To accurately model such things (and they occur in FFI), you need to separate types from layout, and hold the "supertype's layout" fixed.
- A classic use-case of dependent types is dynamically-sized arrays, and "tensors". When you have a pair (L: Nat, V: Pointer(Array(N, T))), you have a layout behind the pointer that is dynamic, but you don't want to conflate this with arbitrary types of the pointee.
Failure to deal with this in fully generality will force you to go down Rust's path of ad-hoc arrays and "dyn trait", which is actually more complexity.
For arrays:
For "dyn trait": Both use dependent records and the dynamic modality I mentioned above. dyn_print doesn't match C++ since it doesn't inline the data, and giving that a static layout would require parameterizing on the layout of t, so I see your point. However, it might be fine to give dyn_print an "incomplete" layout that can only appear behind a pointer.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 dilemma is C's array to pointer decaying semantics. C2y will try to roll that back somewhat (a[i] will no longer be identical to i[a] via the a[i] == a + i == i + a transitive relation), but there's only so much you can do in that regard, especially for array passing, without new syntax or silently breaking alot of valid, proper, carefully written C code. There's too much that can fall through the cracks by relying on non-standard compiler heuristics to substitute for proper typing.
[1] Strictly speaking a VLA can only be created as automatic storage objects, but a VMT can type dynamically allocated (malloc'd) memory. But the syntax looks like a pointer to a VLA because it originates from the need to pass actual VLAs as parameters.