Re:Is your programming language unreasonable?
by tel on Wednesday February 04, 2015 @03:50PM
(#8999660)
> I think it's important to distinguish equality from equivalence.
This is very true. In particular, equality ought to be merely a subset of equivalence. For codata types, as mentioned, equality may not be computable (or well-defined at all), but we can compute equivalences such as bisimulation if we like.
For any type which has a nice equality then merely setting equivalence to equality should be fast, I agree. This is essentially `deriving Eq` in Haskell.
Memberwise equality works for some types, but notably fails when we have abstraction. You can get away with it for (pure) functions on a finite domain if you really want but that's a little hacky---or rather, it involves (implicitly) injecting your function into some kind of container [0] and computing equality there.
As you note, codata types aren't likely to have nice equalities. In these cases they're not going to have memberwise equality, either.
This is very true. In particular, equality ought to be merely a subset of equivalence. For codata types, as mentioned, equality may not be computable (or well-defined at all), but we can compute equivalences such as bisimulation if we like.
For any type which has a nice equality then merely setting equivalence to equality should be fast, I agree. This is essentially `deriving Eq` in Haskell.
Memberwise equality works for some types, but notably fails when we have abstraction. You can get away with it for (pure) functions on a finite domain if you really want but that's a little hacky---or rather, it involves (implicitly) injecting your function into some kind of container [0] and computing equality there.
As you note, codata types aren't likely to have nice equalities. In these cases they're not going to have memberwise equality, either.
[0] First chapter or so of these lecture notes if I remember correctly, http://lambda-the-ultimate.org/node/4804