Hopefully Rust will evolve into it or a new language will come up for that: we really need this to finally have a programming language that is strictly better than all others and can thus be the single language in use and finally the solve the programming language problem.
The Coq language groups types into two categories: Set and Prop. Prop, which (informally speaking) contains all your proofs, is erased when you "compile" your Coq code into another language like Haskell or OCaml. This is something people have thought about quite a bit already.
I think the reason people aren't using dependent types has more to do with the ecosystem around these languages: the tooling, the libraries, the documentation, the tutorials, ... None of that is where it needs to be for these languages to be appealing to industry programmers.
> Hopefully Rust will evolve into it or a new language will come up for that: we really need this to finally have a programming language that is strictly better than all others and can thus be the single language in use and finally the solve the programming language problem.
I have serious doubts about this. Rust, like every mainstream language, already has too many features that overlap with what dependent types give you for free. Also, Rust is not a functional language (some people claim it to be, but there are side effects everywhere!), so it would be a bit of an impedance mismatch.
As much as I'd like to believe in this unicorn language that is better than all the others, experience has taught me to be skeptical of that. Programming is used to solve so many different kinds of problems that it's hard to imagine a one-size-fits-all solution, but I won't claim it's impossible.
Also it's not enough to erase irrelevant types, the types that end up in the program also need to be treated efficiently, which means generic monomorphization, not auto-boxing things unless essential (or ideally never), using computed layouts where possible (i.e. store (n, [T; n], [T; n]) in a single allocation if n is immutable), etc.
The issue is that I think all of the current dependently typed languages don't have zero-cost abstraction and compiled code efficiency as a primary goal, they are designed for research or as machine-checked proof systems.
There's also the issue that some features may not compose well, e.g. Rust's ability to mutate a single field in place (needed for zero-cost since CPUs can do that with a store instruction) doesn't compose very well with dependent types because that can change the type of other fields, and also linear types (again needed to fully use CPUs) don't go well with having proof-like types that refer to other values, etc. All this seems fixable, but it seems quite involved to find the most general and ergonomic solution.
You don't need linear types for in-place updates. You can use a monad (which is another thing you can easily do with dependent types) to express the side effect of doing mutations. Then you can compile that monadic Coq code to Haskell, which then compiles to efficient machine code that actually does in-place updates.
Though, perhaps it is also worth mentioning that Idris 2 has both linear types and dependent types.
Regarding the need for automatic memory management: yes, most dependently typed languages have a garbage collector, but many "real" programming languages have garbage collectors and programmers are still happy to use them. I don't know why everyone in this thread is so concerned about performance. Dependently typed code can compile to reasonable machine code without any stretch of the imagination.
> Also it's not enough to erase irrelevant types, the types that end up in the program also need to be treated efficiently, which means generic monomorphization, not auto-boxing things unless essential (or ideally never), using computed layouts where possible (i.e. store (n, [T; n], [T; n]) in a single allocation if n is immutable), etc.
Memory layout is certainly something that needs to be dealt with, but compilers can monomorphize where possible to generate fast code with unboxed types in many cases. I don't think this is the main blocker for dependent types. I've written dependently typed code that easily outperforms the dynamically typed code I write for production at work (by at least an order of magnitude). In fact, dependent types can be used to guarantee that certain things don't need to be checked at runtime, which can in some cases give even better performance than what you'd get in a regular old statically-typed language.
I'm certain that this can be modelled using dependent types (after all, anything can), but I can't think of a way to do it that's anywhere near as ergonomic as Rust.
Mandatory GC is not a zero-cost abstraction (it is ridiculously inefficient and unnecessary in general), and a language with mandatory GC is a non-starter as a universal language. C programs (like web browsers) are starting to have new code written in a different language only now that Rust is available as the first zero-cost non-GC safe language.
Yes, dependent types improve performance by eliding checks, but that's only likely to be a net win if the rest of the compilation is optimal.
Even more, the performance limitations of most GC languages have more to do with the lack of good ways of writing code which simply doesn't allocate, rather then the problem of collection. GCs are often faster than malloc/free, but not as fast as simply not allocating/freeing anything.
Finally, it's important to remember that there are algorithms that are significantly more difficult to implement without a GC tahn with a GC. Even simple compare-and-swap atomic sets can require many times more code and care to implement if you have to handle cleanup of temporaries as well.
malloc/free is fast with a moving GC, but moving is not, and if an object is never moved it's likely that it should not have been allocated on the heap in the first place.
The cmpxchg problem is solvable by epoch-based reclamation libraries (RCU, crossbeam-epoch, etc.), and while a traditional GC also solves it, it's not necessary.
AIUI, dependently-typed languages don't really have a fixed phase distinction between "compile time" and "run time". The type checking pass can involve execution of "run time" code (this is one way to understand why these languages are generally not Turing complete), and "run time" code may be required to somehow build complex code like a JSON parser "on the fly", depending perhaps on user input.
In practice, some systems have a "code extraction" component that's intended to filter out the "irrelevant" parts of the code and transpile it to a conventional programming language, which obviously reintroduces a separate "run time" deployment step. This could definitely be done using, e.g. Rust, provided that the issues due to a lack of general GC in that language are addressed too.
Do it! There's a dearth of such a format for the more "hi-falutin" topics out there. Doesn't need polish or total precision either, "us programmers" can deal with IRC-like stream-of-tid-bits.
Question: if compile-time evaluation of language X is fully-featured-fully-capable X (sans IO / syscalls, say) with "types as values" (of compile-time-only type `type`, say), ie. given Turing-completeness, where you can have functions that build up and return types --- do you still need complex theoretical type system constructs like "dependent"/"refinement"/"row-polymorphic" etc natively.. say at compile time, given sufficient prim builtins and storage-describing "prim types" (int, arr, tup) any further type-details are described programmatically. I suppose this leads to being able to express predicates that the type checker can "evaluate" in tandem with those compile-time evals..
I haven't gotten to the dependent types part yet. I find most tutorials one these languages start with the theory up front. I'm taking a more pragmatic tack by demonstrating the language through examples building on familiar learning patterns of writing simple programs first and working your way up.
It is a neat way to write programs!
- how much of the burden of writing the proof falls on me, and how much falls to the compiler? I've seen Idris type signatures, and I didn't find them super easy to grasp.
- What are the full range of things I can express? What can't I express, even with dependent types? I come from math, so I'm used to have infinite flexibility to define what goes into my set of possible values. When I first learned Haskell I was surprised that I couldn't easily define types like "this set, modulo an equivalence relation". Or something like: "Int, but only even numbers".
- how huch more effort falls to me when structuring my code, in order to pass the properties or proofs through? I already run into this all the time in Haskell, with Maybes thay I _know_ to contain a value, or Lists that I know not to be empty. There is a real trade off between writing clear code, and wrapping/unwrapping values all the time everywhere.
Length-indexed vectors is a great example, because it is such a non-story in math, and yet for programming I have to front-load all this complexity to express something so utterly trivial. It's part infuriating, part enlightening how surprisingly tricky seemingly small things can be.
The compiler in Idris can do some magic, but usually the burden is mostly on you to write proofs. Idris (and similar languages) have assistance in editors to help you automatically write code and proofs.
> What are the full range of things I can express?
Dependent types as present in Idris, Coq, Agda, etc. can serve as a foundation for mathematics, so… pretty much anything!
For your example, most such languages don't have quotient types, so you'll still need to use setoids or similar to model quotients.
> - how huch more effort falls to me when structuring my code, in order to pass the properties or proofs through?
It's pretty much the same situation as Haskell or Rust, but I think having to write fromJust / unwrap is great. It tells you when you're reading the code exactly what assumption has been made, and it doesn't seem awfully burdensome.
> yet for programming I have to front-load all this complexity to express something so utterly trivial.
What's "all this complexity" that you're referring to?
Also, does support of dependent types suggest, imply, or require a particular paradigm (function, imperative, procedural, declarative, etc) or is that an orthogonal concern?
> I'm curious, are there languages that in your opinion support dependent typing well enough to allow all the concepts that you are describing?
Most of my experience with dependent types comes from a language called Coq (as well as one of my side projects, which is a new dependently typed language). Agda and Idris (among others) also support this style of programming. Idris goes further and uses dependent types to provide amazing IDE capabilities. There's a YouTube video where the designer of Idris used his IDE to automatically implement matrix transposition (the type was so precise that the compiler discovered the only sensible implementation).
Unfortunately I think the world is still lacking a good general-purpose dependently typed programming language suitable for production use (though I'm working on it).
> Also, does support of dependent types suggest, imply, or require a particular paradigm (function, imperative, procedural, declarative, etc) or is that an orthogonal concern?
Generally speaking, dependently typed languages are functional. The fundamental concept in dependently typed languages is the dependent function type, also called "pi type" or (confusingly) "dependent product type". So, the whole thing is based on functions and their types. One could imagine some kind of hybrid language, but combining dependent types and implicit side effects (like imperative languages have) is an active area of research.
I'm already having troubles following it after 8 lines of type definitions, while matrix transposition in the language of my choice is just `#(apply mapv vector %)`
Sorry, I'm not trying to be dismissive, I just want the ergonomics of expressing my intentions to the computer be free of all this boilerplate while leaving compiler a possibility to give me some useful feedback when something might be wrong, are we really not there yet or are there languages aiming to make dependent types practical? You mentioned Coq, but I'm still not being able to find any code examples or some getting started guide in its official documentation...
1 - 'compile-time' code execution of some arbitrary code with the result of that execution then being available at run time
2 - a specific type of function which takes the AST of some language and then uses some procedural methodology to mutate/alter that AST transforming it into some other AST
I would say, that while dependent types can be a useful basis for covering several of the typical use cases of macros, they do not without some additional structure, provide a firm proof/type theory for the whole scope of macros.
I would suggest that the most sound attempts at describing the computational phenomena encapsulated by the most common usage of the term 'macro' would be found in the following: a) implementation of Temporal Logic (per Frank Pfenning's interpretation) for description of compile-time code execution and b) implementation of Modal Logic, describing multi-staged compilation, as in Davies and Pfenning
So, I would not say that dependent types can eliminate macros, but they do cover a chunk of the areas that are often implemented by macros, including generics and other type based compile time code patterns.
- The most popular motivation: the ability to write proofs about your programs, using the same language for both programming and proving. It's so satisfying to write code and prove it correct (with a type checker to catch your mistakes), but so few people get to experience this feeling.
- Of course, you can also use dependent types to just write proofs for the purpose of doing mathematics, without any programming. I've written about my experience doing that here: https://www.stephanboyer.com/post/134/my-hobby-proof-enginee...
- But dependent types are also useful in ordinary everyday programming! Many "features" of programming languages that we use at work are actually just limited special cases of the general idea of dependent types. For example, in a dependently typed language, you don't need special support for generics—you get it for free!
- Dependent types also eliminate much of the need for macros. In Rust, for example, you might use a macro to generate a JSON parser for a given type. If you had dependent types, you could just write a function that takes your type as an argument and returns the parser!
- Of course, there's that famous example of length-indexed vectors. The idea is that you can keep track of the sizes of your arrays in their types, and statically prevent out-of-bounds errors. So, for example, trying to get the first element of an empty array would be a type error.
- Haskell's generalized algebraic datatypes are another example of a limited special case of the full power you'd get from a dependently typed programming language.
- Another example: some languages have special support for existential types in some form or another. For example, Rust has something called "impl Trait" which is a limited use of existential types. This is another thing you get for free with dependent types (or rank-2 polymorphism).
- Other examples of things you get for free with dependent types: type aliases, higher-kinded types, higher-rank types, and compile-time code execution.
Dependent types may seem complicated at first glance. But after seeing how all these programming language features collapse into a single unified framework, you might change your mind: dependent types are extremely simple compared to the cornucopia of concepts we have to learn in their absence! I strongly believe that programming languages have grown too complex, and dependent types have the right power-to-weight ratio to cull that complexity.