Hacker News Reader

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.

> 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.

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.

> 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.

Tangential: How would the function `first :: &(Vec a) -> Option &a` (which, given a non-exclusive reference to a vector, returns a non-exclusive reference to the first item of the vector, with the same lifetime) be typed using linear and / or dependent types?

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.

Monads work for just doing in-place updates, but they seem unable to also prevent/control mutable aliasing, avoid rc/gc of arrays/records, put arrays/records inline in the containing record, and anyway they unnecessarily linearize code, which also seems to play badly with providing proofs.

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.

I agree with your point in general, but I think it is vastly exaggerated to call GC 'ridiculously inefficient' or 'unnecessary in general'. For many common problems, GCs add at best constant overhead. And, almost all highly performance critical programs have some kind of (admittedly specialized) GC mechanisms in place, because often releasing objects as they go out of scope is not efficient enough.

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.

All non-toy languages and compilers only add constant overhead; unfortunately that's still a problem, the goal is to not have any overhead at all.

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.

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!

> 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.

> aimed at programmers rather than mathematicians and computer scientists

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 started one such tutorial: https://agentultra.github.io/lean-for-hackers/

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!

I'm generally interested in this, but (even as somebody who knows intermediate Haskell), I don't have a good intuition about the scope of dependent types:

- 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.

> - how much of the burden of writing the proof falls on me, and how much falls to the compiler?

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?

I, for one, would be quite fascinated by such a blog post - you make it sound downright magical! I'm curious, are there languages that in your opinion support dependent typing well enough to allow all the concepts that you are describing?

Also, does support of dependent types suggest, imply, or require a particular paradigm (function, imperative, procedural, declarative, etc) or is that an orthogonal concern?

Maybe with shelter-in-place I'll have time to write it. :)

> 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.

Damn, this area of programming sounds very interesting, but I'm so so lost in these type compositions... Is it this Idris video you are talking about? https://youtu.be/X36ye-1x_HQ?t=1716

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...

I’m very curious as to what you’re working on. Is the language open source?

Do dependent types really eliminate the need for macros? As far as I can tell you cannot pattern match against values of type Type in dependent languages, so I don’t see how you could generate a JSON parser without some kind of reflection.

I sort of glossed over the differences between macros and dependent types in another answer in this thread, but I'll expand on it here. Typically the term macros is used to imply one of two things (that may be used in the same instance of a macro):

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.

How is that a function working on types not a macros, if that function is executed as part of the compilation process? And how is that function efficient if it is not executed as part of the compilation?

It is a stretched analogy and omits both practical (at the proof level) and theoretical subtlety, but you can sort of think of a dependently typed function as a compile time macro or a template-like generic. However, I think it would be fair to say that macros and generics are merely a mechanized implementation of a very small slice of what dependent types are capable of in full generality