Why is Prop not a part of the Type hierarchy?

Stream: new members

[Marko Grdinić]

I've had issues such as returning a Prop in a tuple only to find out it does not typecheck. Or not being able to pattern match on membership proofs that are Props in regular code. And there were recent issues with putting Props in inductive types only to have them not compile.

What is the purpose for splitting the type hierarchy into two? I've never seen this explained up to now, and it feels like some kind of language design error more than anything else. I already know from Agda that things like equalities and inequalities can be regular types, so what is the deal with this?

[Mario Carneiro]

Prop = Sort 0, Type u = Sort (u+1)

[Mario Carneiro]

You can use Sort when you want to be parametric over both, but inductive types with target Sort u behave oddly in a few ways because the recursor goes into Prop instead of Sort

[Mario Carneiro]

You can use pprod if you want to put a Sort in a tuple, and psigma or \Sigma' to have a dependent tuple

[Mario Carneiro]

Or not being able to pattern match on membership proofs that are Props in regular code.

This one is a fundamental restriction. A Prop is erased at runtime so you can't make decisions based on one

[Mario Carneiro]

However, if one side is decidable you can make it work:

def decide {p q} [decidable p] (h : p ∨ q) : psum p q :=
if hp : p then psum.inl hp else psum.inr (h.resolve_left hp)

[Marko Grdinić]

A Prop is erased at runtime so you can't make decisions based on one.

Is there any benefit to this besides being a performance consideration?

[Mario Carneiro]

It's pretty fundamental to the setup

[Marko Grdinić]

What do you mean?

[Mario Carneiro]

The biggest theoretical upshot is proof irrelevance

[Marko Grdinić]

What is the purpose of proof irrelevance?

[Mario Carneiro]

...It makes proofs equal to each other by definition?

[Mario Carneiro]

that's pretty convenient for a lot of reasons

[Mario Carneiro]

like subtypes act like subtypes rather than types with extra data

[Mario Carneiro]

Also proofs tend to be pretty big, so being able to ignore them is a big deal

[Mario Carneiro]

It doesn't quite recover the separation of proof and data from ZFC / FOL foundations, but it goes a long way

[Marko Grdinić]

Also proofs tend to be pretty big, so being able to ignore them is a big deal

In his latest talk, Edwin Brady talked about quantitative type theory which tracks the usage of variables during type checking. Could that be a substitute for using Props for efficiency reasons?

..It makes proofs equal to each other by definition?

I am not familiar with the details, but I know that extensional type theory has uniqueness of identity proofs which I think is supposed to make identity proofs equal to each other. Does that cover some of the functionality of proof irrelevance?

[Mario Carneiro]

yes... there are other possible choices to be made in type theory, but these are the ones that lean has

[Mario Carneiro]

each one seems to be more complicated than the last, though, so I'm not particularly happy about the trend

[Marko Grdinić]

each one seems to be more complicated than the last, though, so I'm not particularly happy about the trend

I see what you mean. Thinking back to my studies of Cubical Agda, at that time I felt happy that progress on the foundations is being made, but at the end I was left hoping that hundred years from now that work will be done because if not who knows where math will end up.

Since simplicity is a value, let me ask you...how do you feel about Lean being implemented in C++ as opposed to some ML language?

[Mario Carneiro]

@Marko Grdinić It wouldn't have been my first choice language, but that's just personal preference. I am on pretty public record saying that neither C++ nor an ML like language come close to giving you the tools to have confidence in functional correctness.

[Marko Grdinić]

Thanks. I think I now understand the error messages a lot better. In hindsight, I think that a lot of my annoyance that I attributed to Lean over the past few weeks has been due to my own inexperience. Hopefully I will be better prepared for the future now that I am through with this.

https://agda.readthedocs.io/en/v2.6.0.1/language/irrelevance.html

When it comes to understanding the functionality of proof irrelevance, I've found Agda's docs helpful here.