11 Aug
2017
11 Aug
'17
4:37 p.m.
On Fri, Aug 11, 2017, at 11:39, Richard Eisenberg wrote:
If we have a more flexible notion of equality, how can we be sure that this more inclusive equality is always respected? Specifically, you would want this: if (ty1 == ty2) and ty1 is substituted for ty2 in some context, everything still works.
Not too familiar with this area, but I recall at one point realizing that the only kind of user-defined equality that is consistent with Leibniz equality is when the difference occurs in rigid type variables. That is, whereas you can't make Set (A, B) == Set (B, A) since they are observably different, you can (sometimes) make F a == F b if a and b are existentially quantified variables (no-one would be the wiser).