This isn’t the full content of the Curry-Howard isomorphism. The more important part is that proofs are programs. Given a program with some type, execution of the program will construct a value of that type. Also, given a proof of some proposition, step-by-step evaluation of the proof will construct a term inhabiting that proposition. This is why intuitionistic logic is valuable to practitioners: proofs can’t be evaluated like programs if they use the Law of Excluded Middle.
Does that change the conclusion of the post though, which is that treating propositions as equivalent to types makes the practical implementation of proof assistants more difficult?
Maybe I’m misunderstanding something, but Lean considers Prop to be a type (well, a universe of types), right? Coq does a similar trick… And then if your contention is that some types are not in Prop… well the types that aren’t in Prop are pretty much just like n : nat ; n = 2.
I don’t really get the point of this article, but I feel like I’m missing something. Stating that the pure formal method is a hard way to implement stuff… well, yeah. But you can still derive properties from it, and chop up interesting subsets that are easy to implement and maintain useful theoretical properties. We don’t implement data structures as functions, but the lambda calculus is still pretty useful as a thought process!
If propositions were types, there would be no need for the Prop type. That was my takeaway from the article - that treating propositions and types as exactly the same thing is not actually how proof assistants work. It was also confusing to me, because I thought that was the whole point of Coq / Lean. Which is why I found the post interesting.
It probably makes type-oriented proof systems more complicated, sure. Syntax-oriented proof assistants aren’t affected at all, though, so it’s only an issue for systems where the types on the inside (the objects which have properties that we are proving) are influenced by the types on the outside (the logical framework of the proof assistant.)
My understanding is that it might be mostly just about making sure the right things get erased by program extraction, i.e. if you’re using your verified program the Props shouldn’t exist at runtime at all.
Idris 2 uses Quantitative Type Theory which handles this in a different way. A variable with a quantity of 0 is guaranteed to be erased, a quantity of 1 is used exactly once (which is linear typing unless I’m forgetting some subtlety), and no quantity is just an ordinary variable that may or may not get erased.
I’m no expert here so someone please correct me if I’m wrong. But from what I know the unity of propositions-as-types is very much the point in the concept and implementation of these systems; and a mental model without Prop is complete and valid, but sometimes as programmers we need more control over erasure, hence Prop, QTT, etc.
Well I guess that answers a question I had about why propositions and types are separate in Lean. Although Prop itself, as in the category of all propositions, is a type. Interestingly another textbook I read on dependent types (The Little Typer) treated types and propositions as being equivalent, but maybe it didn’t get far enough into the weeds to cause problems.
I haven’t read it, though I keep planning on it. One guess is that educational books like that often present simplified versions of some theory. It’s easier to teach that way. So practical issues like this, where propositions need to be kept separate from types for ergonomic reasons, don’t show up.
This isn’t the full content of the Curry-Howard isomorphism. The more important part is that proofs are programs. Given a program with some type, execution of the program will construct a value of that type. Also, given a proof of some proposition, step-by-step evaluation of the proof will construct a term inhabiting that proposition. This is why intuitionistic logic is valuable to practitioners: proofs can’t be evaluated like programs if they use the Law of Excluded Middle.
Does that change the conclusion of the post though, which is that treating propositions as equivalent to types makes the practical implementation of proof assistants more difficult?
Maybe I’m misunderstanding something, but Lean considers
Propto be a type (well, a universe of types), right? Coq does a similar trick… And then if your contention is that some types are not inProp… well the types that aren’t inPropare pretty much just liken : nat ; n = 2.I don’t really get the point of this article, but I feel like I’m missing something. Stating that the pure formal method is a hard way to implement stuff… well, yeah. But you can still derive properties from it, and chop up interesting subsets that are easy to implement and maintain useful theoretical properties. We don’t implement data structures as functions, but the lambda calculus is still pretty useful as a thought process!
If propositions were types, there would be no need for the
Proptype. That was my takeaway from the article - that treating propositions and types as exactly the same thing is not actually how proof assistants work. It was also confusing to me, because I thought that was the whole point of Coq / Lean. Which is why I found the post interesting.It probably makes type-oriented proof systems more complicated, sure. Syntax-oriented proof assistants aren’t affected at all, though, so it’s only an issue for systems where the types on the inside (the objects which have properties that we are proving) are influenced by the types on the outside (the logical framework of the proof assistant.)
Coq, idris, and lean all use propositions-as-types pretty successfully. I wonder what I’m missing.
My understanding is that it might be mostly just about making sure the right things get erased by program extraction, i.e. if you’re using your verified program the Props shouldn’t exist at runtime at all.
Idris 2 uses Quantitative Type Theory which handles this in a different way. A variable with a quantity of 0 is guaranteed to be erased, a quantity of 1 is used exactly once (which is linear typing unless I’m forgetting some subtlety), and no quantity is just an ordinary variable that may or may not get erased.
I’m no expert here so someone please correct me if I’m wrong. But from what I know the unity of propositions-as-types is very much the point in the concept and implementation of these systems; and a mental model without Prop is complete and valid, but sometimes as programmers we need more control over erasure, hence Prop, QTT, etc.
Well I guess that answers a question I had about why propositions and types are separate in Lean. Although Prop itself, as in the category of all propositions, is a type. Interestingly another textbook I read on dependent types (The Little Typer) treated types and propositions as being equivalent, but maybe it didn’t get far enough into the weeds to cause problems.
I haven’t read it, though I keep planning on it. One guess is that educational books like that often present simplified versions of some theory. It’s easier to teach that way. So practical issues like this, where propositions need to be kept separate from types for ergonomic reasons, don’t show up.
Prop is a type in lean. Doesn’t look separate to me.
Individual propositions are not types though, they’re props. Prop itself is a type, like how Nat is a type. And Nat by itself is not a Prop.