3 ms·
No. Guaranteeing typeclass laws like associativity is hard. People have looked into various ways to do that, but haven't found anything completely satisfying. I
by tikhonj 10y ago
No. Guaranteeing typeclass laws like associativity is hard. People have looked into various ways to do that, but haven't found anything completely satisfying. It's either hard for the programmer (dependent typing) or hard to implement (automatic theorem proving). I hope that'll change, but for now Haskell does not have any facilities for specifying or enforcing typeclass laws.
As it is, it works more or less exactly like interfaces from other languages. When you implement Comparable in Java you implicitly expect certain laws (ie that it's a valid ordering), but there is also no way to specify or verify them.
- Bromskloss 10y agoClueless suggestion: What about the programmer (who implements the semigroup) also providing a proof (that can be automatically checked) that it satisfies associativity? Is that method perhaps already covered by one of the examples you mentioned?
- reuben364 10y agoThat is the dependent typed aspect mentioned. This is actually done in Idris with VerifiedSemigroup and other verified instances.
- Bromskloss 10y agoOK. I'm afraid I don't know enough to make the connection. Actually, I never understood the point of dependent types. They seem to do away with the neat order that types introduce. ¯\_(ツ)_/¯