4 ms·

> You may have abstract types in which case equality should not be implicitly defined. You may also have codata types where you cannot merely compare "value con

by sjolsen 12y ago

> You may have abstract types in which case equality should not be implicitly defined. You may also have codata types where you cannot merely compare "value containment" since it's no longer a concept. These are both important things which are sometimes called "objects" and shouldn't be eliminated from languages. I think it's important to distinguish equality from equivalence. There are many cases (e.g., enumeration types) in which equality is a perfectly appropriate definition of equivalence; but there are also many cases (e.g., some codata types) in which equality is an inappropriate definition of equivalence. Therefore, equality-as-equivalence as default behaviour is probably a poor choice— though it should be easy to opt for that behaviour. As for equality (i.e., intensional equality) itself, I think memberwise equality (or perhaps even equivalence?) is a perfectly reasonable definition. There are times when you really want to discriminate on object identity (in the storage-location sense), but you needn't restrict equality to object identity to allow that.

tel 12y ago
> 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. [0] First chapter or so of these lecture notes if I remember correctly, http://lambda-the-ultimate.org/node/4804 http://lambda-the-ultimate.org/node/4804

by sjolsen 12y ago

tel 12y ago

> 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. [0] First chapter or so of these lecture notes if I remember correctly, http://lambda-the-ultimate.org/node/4804 http://lambda-the-ultimate.org/node/4804