3 ms·
I'd love to hear of a case where anyone has actually computed a Goedel number. We very often do arithmetic on booleans, the a canonical homomorphism (Iverson b
by Y_Y 9y ago
I'd love to hear of a case where anyone has actually computed a Goedel number.
We very often do arithmetic on booleans, the a canonical homomorphism (Iverson bracket) with 1 ~ True and 0 ~ False where && and || are multiplication and addition. But I guess you knew that.
- yorwba 9y agoThat is not the only homomorphism. You could just as well have 0 ~ True and 1 ~ False, where && and || are addition and multiplication. Booleans don't have enough algebraic structure to nail down a unique embedding. Integers and reals don't have the same problem, because there's a unique ring homomorphism between them.
- catnaroek 9y agoBlessing noncanonical structures and mappings is indeed evil. Let's take this to its logical conclusion and banish type classes.
- yorwba 9y agoI'm not sure what you mean by that. Type classes are all about making canonical structures explicit.
- catnaroek 9y agoType class instances are only “canonical” by fiat. Once you elaborate type classes into record-passing, by no means are the resulting instance types uniquely inhabited. This is just as bad as the existence of truthy or falsy values.