Zulip Chat Archive

Stream: new members

Topic: Why is Prop not a part of the Type hierarchy?


view this post on Zulip Marko Grdinić (Oct 31 2019 at 10:31):

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?

view this post on Zulip Mario Carneiro (Oct 31 2019 at 10:39):

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

view this post on Zulip Mario Carneiro (Oct 31 2019 at 10:41):

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

view this post on Zulip Mario Carneiro (Oct 31 2019 at 10:42):

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

view this post on Zulip Mario Carneiro (Oct 31 2019 at 10:43):

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

view this post on Zulip Mario Carneiro (Oct 31 2019 at 10:45):

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)

view this post on Zulip Marko Grdinić (Oct 31 2019 at 10:47):

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?

view this post on Zulip Mario Carneiro (Oct 31 2019 at 10:48):

It's pretty fundamental to the setup

view this post on Zulip Marko Grdinić (Oct 31 2019 at 10:48):

What do you mean?

view this post on Zulip Mario Carneiro (Oct 31 2019 at 10:48):

The biggest theoretical upshot is proof irrelevance

view this post on Zulip Marko Grdinić (Oct 31 2019 at 10:49):

What is the purpose of proof irrelevance?

view this post on Zulip Mario Carneiro (Oct 31 2019 at 10:49):

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

view this post on Zulip Mario Carneiro (Oct 31 2019 at 10:50):

that's pretty convenient for a lot of reasons

view this post on Zulip Mario Carneiro (Oct 31 2019 at 10:50):

like subtypes act like subtypes rather than types with extra data

view this post on Zulip Mario Carneiro (Oct 31 2019 at 10:51):

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

view this post on Zulip Mario Carneiro (Oct 31 2019 at 10:53):

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

view this post on Zulip Marko Grdinić (Oct 31 2019 at 10:57):

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?

view this post on Zulip Mario Carneiro (Oct 31 2019 at 11:34):

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

view this post on Zulip Mario Carneiro (Oct 31 2019 at 11:35):

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

view this post on Zulip Marko Grdinić (Oct 31 2019 at 12:48):

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?

view this post on Zulip Mario Carneiro (Oct 31 2019 at 17:00):

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

view this post on Zulip Marko Grdinić (Oct 31 2019 at 20:16):

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.


Last updated: May 10 2021 at 00:31 UTC