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.1 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 <[EMAIL PROTECTED]> wrote: > 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 > _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
