The two types of irrelevance: irrelevance à la parametricity, or "I promise I won't look at it", and irrelevance à la Prop (ZSTs for Rustaceans), or "go ahead, there's nothing to see".
What's their relationship? Some duality?
Conversation
Interesting question. My first observation would be that parametricity is a meta theorem while proof irrelevance can be stated as an axiom (e.g. Coq) or even as a typing rule (Lean)
1
1
2
W.r.t. "proof irrelevance" you are referring to my "irrelevance à la Prop", right?
W.r.t. "irrelevance à la parametricity", I think both the irrelevance and the parametricity are meta: if f never inspects A, you can prove both that A can be erased and that f is parametric wrt A.
3
Yes, proof irrelevance means that any two proofs of a proposition are propositionally (Coq) or definitionally (Lean) equal. So props have at most one value and you're allowed to treat them as multiplicity 0, to connect this thread to the other one
1
1
I think I might be using "irrelevance" where I mean "erasure"/"erasibility", or vice versa. Do those mean the same thing or is there a fine distinction?
What does "allowed to treat them as multiplicity 0" mean in practice? I thought lower mult.s give you strictly fewer options?
1
I'm not an expert on either of these topics, but irrelevance as in "computational irrelevance" seems to be equivalent to "erasibility" to me. And I'm not aware of any kind of irrelevance that does not imply computational irrelevance.
1
2
Regarding multiplicity, yes, 0 gives you fewer options, OTOH lower multiplicity is of course desirable for better performance. We statically know that we do not need the "more options" for any proof value because of computational irrelevance, so we know they will always be erased
1
1
What is the dual of multiplicity 0 on a binder/parameter? ie. What does it mean to return something that can never be used?
Related:
Quote Tweet
@dorchard @buggymcbugfix hey, I’m curious what the 1 multiplicity behaves like in the effect position in Granule. Would that be equivalent to uniqueness? Ie. vs. the coeffect position which would be linearity?
Show this thread
1
1
ie. multiplicity 1 on the return type seems to be uniqueness typing (ie. the dual of linear typing)
1
Show replies
(IANAE but) maybe mult 0 on an input is (erased/parametric) universal quantification, and on an output, existential?
(Something like one component of a record being mult 0 and the type of another referencing it; just returning a mult 0 thing by itself doesn't sound useful)