30 Apr
2005
30 Apr
'05
5:44 p.m.
Jan-Willem Maessen <jmaessen@alum.mit.edu> wrote:
...discussion of the laws of MonadPlus reinforces to me the real need for being able to declare the laws that a typeclass should satisfy, not just the signature.
On this I cannot but agree. But we don't usually count on being able to prove these by construction.
Note that I was just suggesting that the laws be given and available (ie as type-level constructs, not comments). I was not suggesting that 'proofs' be either done by the compiler, nor even given as necessary annotations. Although if they were present (as annotations), the proof itself might furnish some additional ingredients that an advanced optimizer might be able to use to good effect... Jacques