4 ms·

The problem is that, as far as I can tell, there is no language with zero-cost dependent types, i.e. a language with dependent types that has a subset equivalen

by devit 6y ago

The problem is that, as far as I can tell, there is no language with zero-cost dependent types, i.e. a language with dependent types that has a subset equivalent to Rust that compiles to machine code as efficient as the Rust compiler outputs. 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.

curryhoward 6y ago
> The problem is that, as far as I can tell, there is no language with zero-cost dependent types, i.e. a language with dependent types that has a subset equivalent to Rust that compiles to machine code as efficient as the Rust compiler outputs. 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.
- devit 6y ago
  AFAICT Coq doesn't have linear types, and thus can't provide in-place modification of array elements or non-reference-counted/GCed non-primitive values, which means it can't take full advantage of a real CPU+RAM machine. 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.
  - curryhoward 6y ago
    > AFAICT Coq doesn't have linear types, and thus can't provide in-place modification of array elements or non-reference-counted/GCed non-primitive values, which means it can't take full advantage of a real CPU+RAM machine. 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.
bjz_ 6y ago
I've been trying to learn enough about this problem to be of use in implementing this (playing around with my own language implementations). It seems like a real challenge might be around ensuring that your programs have extraneous 'type stuff' removed in the compiled program. Part of this could be helped with a nice way of doing proof irrelevance (eg. something like Quantitative Type Theory) and another could be multistage programming (eg. something like MetaML or MetaOCaml). The latter would make it much easier to do a more general form of Rust's monomorphisation of type parameters. You'd then may also want some sort of uniqueness typing and borrowing, but I have no idea where to get started on that! And you also don't want to drown in a mountain of annotations!
zozbot234 6y ago
> The problem is that, as far as I can tell, there is no language with zero-cost dependent types, i.e. a language with dependent types that has a subset equivalent to Rust that compiles to machine code as efficient as the Rust compiler outputs. 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.

by devit 6y ago

curryhoward 6y ago

> The problem is that, as far as I can tell, there is no language with zero-cost dependent types, i.e. a language with dependent types that has a subset equivalent to Rust that compiles to machine code as efficient as the Rust compiler outputs. 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.

devit 6y ago
AFAICT Coq doesn't have linear types, and thus can't provide in-place modification of array elements or non-reference-counted/GCed non-primitive values, which means it can't take full advantage of a real CPU+RAM machine. 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.
- curryhoward 6y ago
  > AFAICT Coq doesn't have linear types, and thus can't provide in-place modification of array elements or non-reference-counted/GCed non-primitive values, which means it can't take full advantage of a real CPU+RAM machine. 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.

bjz_ 6y ago

I've been trying to learn enough about this problem to be of use in implementing this (playing around with my own language implementations). It seems like a real challenge might be around ensuring that your programs have extraneous 'type stuff' removed in the compiled program. Part of this could be helped with a nice way of doing proof irrelevance (eg. something like Quantitative Type Theory) and another could be multistage programming (eg. something like MetaML or MetaOCaml). The latter would make it much easier to do a more general form of Rust's monomorphisation of type parameters. You'd then may also want some sort of uniqueness typing and borrowing, but I have no idea where to get started on that! And you also don't want to drown in a mountain of annotations!

zozbot234 6y ago

> The problem is that, as far as I can tell, there is no language with zero-cost dependent types, i.e. a language with dependent types that has a subset equivalent to Rust that compiles to machine code as efficient as the Rust compiler outputs. 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.