
I really like Chuan-Kai Lin's Unimo paper; in it he talks about
defining a monad in terms of defining the behavior of its effects:
http://web.cecs.pdx.edu/~cklin/papers/unimo-143.pdf
Prompt is based on the same idea, with one small difference. While
it's possible to write observation functions that break the monad laws
with Unimo, it's actually impossible to do so with Prompt.
http://hackage.haskell.org/cgi-bin/hackage-scripts/package/MonadPrompt-1.0.0...
This way you don't have to prove the Monad laws at all, you just write
the code you want and some properties are guaranteed for you.
-- ryan
On 4/11/08, Rafael C. de Almeida
Hello,
I was studying Monads and I was trying to think about new Monads I could define. So, a question poped into my mind: how is proof regarding the 3 Monad laws handled? I know that, aside from testing all the possible values (and there can be a lot of them), there's no general way to prove it. Nonetheless, I think that it would be insightful to see how people write those proofs for their monads -- specially for new user monads. Is there some article or some notes on proving that Monads are implemented correctly?
[]'s Rafael _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe