4 ms·
Clueless suggestion: What about the programmer (who implements the semigroup) also providing a proof (that can be automatically checked) that it satisfies assoc
by Bromskloss 10y ago
Clueless 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. ¯\_(ツ)_/¯