curryhoward

When you say "Rust enums are also enums", that's not true in general. What is true is that _some_ Rust "enums" (like your `Colour` example) can be represented as traditional enums. You don't prove a universal quantification with a single example.

That's right. It's unfortunate that Rust calls them "enums", since as you noted that term already had a well-established meaning in other languages, and the concept that Rust calls "enums" also had several existing names (sum type, coproduct type, disjoint union, and, more generally, algebraic data type) in the literature and in prior languages.

Language designers: stop changing the meanings of words! I know you mean well and you're trying to tie unfamiliar ideas to familiar ones for beginners, but you end up causing more confusion for everyone in the long run.

Did you mean to reply to a different comment? You seem to be restating the correct part of orthoxerox's comment. I was merely refuting the incorrect part.

I love seeing new Haskell projects, though I personally would rather just stick with Haskell's clean syntax:

  data Maybe a = Nothing | Just a

...over this:

  data Maybe<a> {
    Nothing,
    Just(value: a)
  }

I understand that programmers coming from mainstream languages might feel uncomfortable without all those angle brackets, curly braces, and parentheses (why do C-like languages have so many ways to syntactically group things?), so if this project helps them ease their way into Haskell I totally support it. However, a small part of the joy of Haskell is freeing yourself from the arbitrary syntactic boilerplate that most languages have.

That's true in practice, but technically speaking it's false. You could imagine a contrived system which is not Turing complete but still contains a (rather useless) primitive that causes an infinite loop.

I'm guessing the comment was talking about examples like this:

    program -abcdefg.txt

Just from reading this, you can't tell where the flags end and the filename begins unless you have all the flags and their arities memorized.

> I am talking about (1) the proof steps involved in proving a given, fixed statement. You are talking about (2) a wider notion that includes the formulation of the statement to be proved.

No, I am not. The original proof used an implicit assumption, which is a problem with the proof proper, not the formulation of the statement to be proved. Using a proof assistant guarantees that there are no implicit assumptions, which is one reason why this work is notable. It rules out an entire class of errors which were present in previous work.

> The article doesn't say that the original proof was incorrect.

The article very clearly points out an error in the original proof.

The HN community can be so toxic sometimes. Inevitably whenever someone produces a new machine-checked proof, all these commenters come out of the woodwork explaining how assumptions/definitions are not verified and therefore the whole endeavor is somehow worthless.

A researcher being excited about their research is nothing to be ashamed about. I especially appreciate the fact that one of the authors took the time to make an accessible blog post to introduce us to their work.

I feel like most commenters are missing the point. The fact that this issue was finally settled once and for all using a proof assistant is a huge achievement! That's the highest degree of scrutiny that a proof can undergo. This is especially important given the high number of mistakes in prior work—one would be forgiven for distrusting new papers on this topic that don't have machine-certified proofs. I can't believe people think this is just clickbait. Do y'all not recognize the importance of math being...well...correct?

In academia, "type theory" almost always means dependent type theory, such as Martin-Löf type theory or homotopy type theory. Type theory is used in most theorem provers as a foundation for mathematics. The title of this blog post is using the term in a standard way.

Programming languages such as Haskell and Java are not based on type theory. They have type systems. Haskell's type system is much closer to type theory than that of Java, but it's still quite crippled compared to what type theorists study.

It is of course possible to define things in type theory such that 1/0 = Infinity or something else, but that is not the norm.

Content editors should not be able to add arbitrary code to a bank's website unless it undergoes review from someone who understands web security. If there is some kind of content editing tool, it should only allow content (not arbitrary scripts) to be edited.

Another implementation of this idea: https://www.huffgram.com/

> For ‘moderate performance’ surely JVM based languages are what you’re looking for? There’s great tooling and a very low barrier to creating new languages.

Not sure I understand what you're suggesting. I was asking for a language with dependent types (or anything that isn't just another procedural/OOP language). Such a language could use any runtime, whether it be the JVM or anything else.

> It’s already suspicious by virtue of having a hand-wavy "Int" type (what size/signedness is that?) and it appears to be object-oriented (so we have to rely on compiler optimisations to remove dynamic dispatch) and garbage-collected (so by default any non-trivial type is heap-allocated). These are just ways in which it is worse than Rust as far as performance goes, since "ergonomics"/"productivity" is so subjective.

While I agree that this language doesn't seem to be differentiated enough to compete, I disagree with your apparent premise that new languages need to be as fast as Rust. I personally would welcome a new language that gives me full-spectrum dependent types with great tooling and moderate performance. There are many aspects to programming languages beyond raw speed.

The world has enough cookie cutter procedural and OOP languages. I'd love to see a new language from a different paradigm succeed.

I completely sympathize with the difficulty in understanding the notation and wish it were more accessible. I struggled with it for some time. But as someone who eventually learned it, I find it to be fairly sensible. What would be a better way to write the that judgment?

`A` is a type, yes.

Whether `Type` is a type depends on what type system you're working in. If `Type` is its own type, then it turns out you can use that to do infinite recursion (this is called Girard's paradox). Dependent types are often used for proving theorems, where infinite recursion corresponds to circular reasoning—a big no-no. So, in many dependently typed languages, `Type` is not its own type (instead, it's common to have an infinite tower of types: `42` has type `Int`, `Int` has type `Type0`, `Type0` has type `Type1`, `Type1` has type `Type2`, and so on).

However, if the programming language is just used for programming and not for proving, then it's perfectly fine (and quite convenient) to have `Type` be its own type.

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

Unfortunately you need to know type theory/logic notation in order to read this. Here's the English translation:

- There is a variable called `x` in scope.

- `x` is known to have type `A`.

- `B` is a function that, when given `x` as an argument, returns a type. If this seems weird, it's because you need dependent types to even be able to say this.

Honestly, this article is not written for programmers, and I don't know why it's on Hacker News right now. Most HN readers don't have the necessary background to follow it.

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

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.

I've been meaning to write a tutorial on dependent types, but aimed at programmers rather than mathematicians and computer scientists. Here are some of the reasons I love them so much:

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

I agree with the other commenter about the comma in this sentence. But I'd also like to point out that 100% error-free code is possible. There's a whole branch of computer science dedicated to it: formal verification. I personally have used Coq to write certified code in the past, and I'm quite confident that my code was 100% error-free.

Of course, there are some qualifications one should make regarding such a claim: you have to trust that your specification is "correct", that your hardware is functioning correctly, that the proof checker didn't accept a bogus proof, that the underlying logic (e.g., the calculus of inductive constructions) is consistent, etc. That's a lot of things to trust, but the point is that you don't have to trust yourself.

This looks a lot like Toast: https://github.com/stepchowfun/toast

The question you were answering was not talking about proof search. It was merely asking whether it was possible to do verification in the same language that the program is written in. And, contrary to your response, it is possible to do verification in the same language as the program is written in. Coq is an example of that.

Yes, proof search is undecidable. But that's not what we're talking about in this thread. seL4 isn't verified by proof search. The proofs were provided by humans (with limited automation).

Not if the human provides the proofs and the compiler merely checks them (like in Coq, for example).

Consider these equations for integers:

    x * 1 = x
    1 * x = 1
    x * (y * z) = (x * y) * z

These should be familiar if you know about integers.

Now consider the following equations for strings:

    concat(x, "") = x
    concat("", x) = x
    concat(x, concat(y, z)) = concat(concat(x, y), z)

These should be familiar if you know about strings.

Now consider the following equations for booleans:

    x or false = x
    false or x = x
    x or (y or z) = (x or y) or z

These should be familiar if you know about booleans.

If you can see the pattern, you understand monoids. Monoids are everywhere in programming.

I believe they are just saying that tail calls can be used in a mutually recursive way without consuming unbounded memory. They said "self tail recursion" is not necessary but you interpreted it as "tail recursion is not necessary".

> all those things you're mentioning are side effects and are captured by the same concept, of representing effects by carrying a parameter through a chain of function calls

No. The state and environment monads fall under that rubric, but many of the others are far removed from what you're describing. You can't implement backtracking in a purely functional way simply by passing around an extra parameter, because backtracking affects the control flow. Continuations are even stranger—they're not even algebraic!

> I'm not backing down from the core claim that Moggi realised that CT monads are a nice formalization of side effects in pure functional programming

No, Moggi's paper was about formalizing the semantics of impure programming languages. It wasn't until Wadler that we started using monads to model side effects in pure functional programming. Please read the actual research before citing it.

> by carrying a "world" parameter that represents the state being modified

From this, it's clear you've never read and understood Moggi's seminal paper. Monads are functors with some extra monoidal structure. The concept, and even Moggi's use of it in categorical semantics, has nothing to do with "worlds".

The important realization is that there are many more monads than just the one hardcoded into one's programming language of choice. State, error handling, parsing, reading from an environment, backtracking, nondeterminism, mutable state, logging, probability, continuations, async/await, I/O, ...these are all just specific instantiations of the general interface of monads. Recognizing that allows you to build abstractions that work for any monad, rather than re-discovering and re-implementing the same idea for each one separately. It's been a remarkably fruitful area of research.

> In a typical PL context "effects" is always short for algebraic effects

The word "effects" has a long and storied history in programming language theory that predates algebraic effects/handlers by decades. The study of effect systems includes algebraic effects but also monads and other type and effect systems. In some situations the lines between these are blurred, for example with "extensible effects" which are algebraic effects implemented by a free(r) monad combined with "data types a la carte"-style open unions.