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
Replying to
Something something multiplicity 0. I think there is mumbling from Mcbride about Prop being abit hacky, but I don't know about what the solution is. Could you also have things that are irrelevant because they exist in a later execution phase? Or would that just be ill-formed. 🤔
Replying to
My hunch would be that multiplicity 0 is closely related to the "irrelevance à la parametricity" half of things, whereas "à la Prop" is the sort of thing which can be erased *even if you have infinitely many of them*. Could be mistaken though!
1
(The second half of your tweet reminds me of McBride's "oil and water" remark here: pigworker.wordpress.com/2014/12/31/wor. Is that what you had in mind? N.B. it's been a while since I read (or tried to read) that and I can't remember how much of it I got.)
2
1
Show replies