In Spire we're thinking of downgrading Eq[A] from equality to just an equivalence relation. What do you think? Good? Bad? Ugly?
-
-
Replying to @mcclure111
@mcclure111 So that was my intuition too.@tixxit sorta talked me out of it by explaining that the distinction is often lost on folks.3 replies 0 retweets 0 likes -
Replying to @d6
@d6@mcclure111@tixxit what are you seeing the distinction being? Substitutivity? That's a pretty unusual kind of property in programming.1 reply 0 retweets 0 likes -
Replying to @copumpkin
@copumpkin@mcclure111@tixxit for equality, x == y implies that f(x) === f(y) for all f, yeah.2 replies 0 retweets 1 like -
Replying to @d6
@d6@mcclure111@tixxit ah, I'd call that cong, in Agda parlance. Instance of subst, which says if statement is true for x, then true for y.1 reply 0 retweets 0 likes -
Replying to @copumpkin
@copumpkin@mcclure111@tixxit Right. I mean, I don't have sufficiently fine tools in Scala to distinguish that from substitutivity.2 replies 0 retweets 0 likes -
Replying to @d6
@d6@mcclure111@tixxit my point was more about both of those being global properties about the rest of your program, not the type itself1 reply 0 retweets 0 likes -
Replying to @copumpkin
@d6@mcclure111@tixxit i.e., almost impossibly onerous in a world with object identity2 replies 0 retweets 0 likes
@copumpkin @d6 @mcclure111 yeah, it would really be more a promise to the programmer + retstriction on "f" (no object identity, refl, etc.)
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.