Conversation

rntz
@arntzenius
Hold up... Isn't proof irrelevance just a degenerate case of information flow typing? Information may not flow from proof irrelevant to proof relevant computation, but it can go vice-versa. So proof-irrelevant is “high security” & proof-relevant is “low”!
5
13
Joey Eremondi @ ICFP
@EremondiJoey
Yeah, my understanding is that it's the same, but proof irrelevance adds the constraint that all elements are definitionally equal, so the terms are indistinguishable at both runtime and compile time. E.g. you can't case split on an irrelevant term even in a type annotation.
1
2