On Sun, Jul 4, 2010 at 11:16 AM, Daniel Fischer
On Sunday 04 July 2010 16:05:48, Jorden M wrote:
Now that I've had a really short look at Axioms, I think the Haskell equivalent would be QuickCheck properties. After all, Axioms are not enforced by the compiler, their only effect is documentation. Granted, they
Really? I thought they were.
I think that's not even possible in general.
It would equate to solving the Halting Problem, I suppose. The point of axioms for compiler use must then have been to say, `All right, assume this is true and make optimizations if possible.' A bit fast and loose in the presence of careless programmers, no? At least calling them axioms makes more sense.
Generally, you can't decide the equality of functions [okay, we're dealing with finite domains in a computer, so in principle one could check all possible inputs, but even for a small type like uint64_t, that's impractical].
are part of the source code, but frankly, I don't see how this has more effect than stating invariants as QuickCheck properties or writing them down in a comment.
Would it make sense to try to formalize things like the monad laws using QuickCheck?.
To a certain extent. You'd have a good chance to catch gross violations of the monad laws with QuickCheck. But for subtle violations, the odds are minuscule.
I wonder if the effort to do so would be useful.