What language features are needed in order to implement dependent types? Can you implement it on top of existing features of say Rust or Swift?
A second feature that I think is needed is a way to go between types and values which I don’t think rust or swift can do.
Two fundamental dependent types are the dependent sum and dependent product. The dependent product is the type of a function whose output type depends on its input value. This is a generalisation of the product type: the product type (a,b) is like the dependent product type (x:{1,2}) -> T x where T 1 = a and T 2 = b.
The dependent sum type consists of a tag value of some type and a value whose type depends on the tag. For example a vector of arbitrary length Of floats could be written with a type something like:
Sum(n:Nat)(Vec n Float)
(2,[1,2])
I think instead, for one of these languages, the ideal would be opt in should you need it. Dependent types are, by their nature, proof carrying[2], and there are times when you want this, but for a general-purpose programming language, also times that you do not. You can't be total over IO (or any effect for that matter), so, yeah, skip it when arg-parsing, but then opt-in when you're processing your financial transactions or actuating your robot.
Totality is orthogonal to dependent types. You can absolutely have non-total programs at the type level: Rust has such programs today in fact!
> Generally this means that recursion is only allowed if its structural, and there can be no run-forever loops, i.e., no servers.
You can have an infinite loop in a total language like Agda or Idris: coinduction is the mechanism.
> Dependent types are, by their nature, proof carrying[2], and there are times when you want this, but for a general-purpose programming language, also times that you do not.
This doesn't make a whole lot of sense to me. Dependent types are "proof carrying" in the sense that any program of the type:
Int -> Int
> You can't be total over IO (or any effect for that matter), so, yeah, skip it when arg-parsing, but then opt-in when you're processing your financial transactions or actuating your robot.
You can be total over IO, and effects do not imply non-totality either.
Absolutely, the talk I linked to gets at this to some extent. In rust, partiality causes type checking to fail. You could use it on purpose!
> You can have an infinite loop in a total language like Agda or Idris: coinduction is the mechanism.
For sure, but the totality checker is appeased by sized-types, or at least that's how I know to do it in Agda. I've heard it can be done without them, but I'm not familiar with the approach. This is what I intended w/r/t structural recursion.
> This doesn't make a whole lot of sense to me.
This is because, as the authors state, to type check the program is to evaluate it, so before it can run you have proof that it is correct.
By opting out I'm more talking about the converse, to opt in when you need it. Kind of the opposite of Idris's %partial directive.
> You can be total over IO, and effects do not imply non-totality either.
That's fair, you're right. This is poorly stated.
LF does not have higher kinded types but it does have dependent types.
You can definitely add dependent types to Rust, but I see at least the following problems.
1. Rust compile times and dependent typing compile times are both really long. Combining the two sounds like it'd be unacceptably long.
2. Rust promises full type erasure when you're not using "dyn". Predictably erasing dependent types seems to be a hard problem. Heck, even ergonomically giving low-level control over the layout of a dependent sum sounds hard.
3. Dependent types give you a whole bunch of new ways to do things that you can already do in Rust, which is probably a bad thing.
I think "bolt-on" approaches, as Hoare logic is to imperative pseudocode, or SPARK is to Ada, are something that Rust could easily employ, which are more well-tested, and would solve all of the use cases of dependent types in industry.
I don't know if "type erasure" is the accurate term to use with the generic-specialization scheme that Rust uses; one can trivially write a generic Rust function that demonstrates that types, while inaccessible at runtime, still semantically affect the generated code:
use std::mem::size_of;
fn foo<T>(t: T) {
dbg!(size_of::<T>());
}
fn main() {
foo(1); // prints 4
foo("bar"); // prints 16
}Equivalent C++ code (admittedly, C++ templates aren't really generics) would have enough information to shove literal 4 and 16 into the binary there.
Rust does guarantee type erasure on lifetimes, but lifetimes are only used for semantic analysis, and are completely separate from and unrelated to code generation/type layout.
In C++ you can do any syntactically valid thing with the Type Parameter in a Template body, and it isn't type-checked until you attempt to instantiate it.
I guess I had mistakenly thought that run time dispatch and a single binary implementation was somehow required for parametric polymorphism since it requires treating all types identically. Upon reflection I can see that it's not actually exclusive of compile time dispatch though.
From a pragmatic perspective it seems unfortunate that such generics can't be used in an API without corresponding access to the source code. I saw the ability to work with arbitrary future types at runtime as largely being the point of type erasure.
From a theoretical perspective I'm having some trouble accepting the idea that Rust generics are an example of true parametric polymorphism. In the earlier example a function could behave differently based on the size of the type. That's not uniformly dispatching to a behavior implemented by the type though, which seems like the core idea behind parametric polymorphism to me. (I suppose my concerns are purely academic though. AFAIK runtime reflection in Java allows utterly breaking type erasure but in practice Java generics still seem to be referred to as an example of parametric polymorphism.)
The effect without concepts is that you can (in principle) get things that "accidentally" match, like applying "+" to strings; and that the error messages when they don't match are unpleasant. Concepts resolve both.
what's happening here is that rust does "monomorphization" – it generates two versions of `foo`, one for ints and one for strings; then, in each specialized version, `size_of` is specialized to that particular type's implementation of `size_of` (compiler-generated), which returns 4 for i32 and 16 for <whatever that string type is>.
i'm sure it's actually more nuanced than that, but i think that's the general principle.
But it is not easy to plug dependent types to existing compilers of Rust or Swift. In general, a dependently typed language is not Turing-complete so that the type checking (which now requires running programs) is decidable. That means you have to rule out features like general recursion and arbitrary loops. That could mean reconnecting the wires in the existing compiler. From an engineering aspect, it should be easier to plug dependent types on a functional programming language, e.g., dependent Haskell, than imperative languages.
You don't bolt this functionality on to an existing language; it requires changes to your whole compiler pipeline to be useful.
What is possible and what is practical are two different things.
I don't know enough to say whether this would be possible in Rust.
Useful steps on the road: singleton types (needed to make it easy to represent basic values as types), higher-kinded types (needed to implement functions at the type level), kind polymorphism (needed to be able to reuse the same functions at the type and the value level). Rust is I think getting the first, is gradually implementing little subsets of the second, and is nowhere near the third.
The other thing you need to worry about is how dependent types interact with existing language features. In particular, if not implemented carefully then they may break type inference, and I imagine Rust's lifetime inference might have similar issues.
Dependent Types via macros, in Racket
somewhere near the end of the paper is a table of the macro features used, which gives the impression it was only possible in Racket, but the lack of a common terminology for these things makes it hard to compare other languages' macro systems unless you are deeply familiar with them, so maybe it could be adapted
So yes to all of your questions.
If you want dependent types IN Rust or Swift then Turing-completeness won’t help you, because neither of them have Turing-complete type checkers. You’d have to modify the compiler for them (and thus change the language itself).
Apparently Haskell has some restrictions that make typeclasses decidable (if -XUndecidableInstances is not set), but Rust has no such mechanism other than numeric iteration limits.
For example, write a type that implements a Turing machine parameterized by a program and a natural number N of evaluation steps to take. Apply that type to Graham’s number or some suitably large natural number. You now have a type that is, for all practical purposes, Turing-complete, even though it is theoretically guaranteed to terminate.
To do that you’d first need to be able to fit Graham’s number into your source code which unfortunately is never going to happen.
Idris has a termination checker which in practice rejects non-primitive recursion. If you can’t prove to the type checker that your recursive function deferments toward a base case at every step then your program won’t type check. So there’s no back-door method to get Graham’s number or other silliness like the Ackerman function into your types.