[Haskell-cafe] Monad proof

Ryan Ingram ryani.spam at gmail.com
Fri Apr 11 20:40:22 EDT 2008

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:


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.


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 <almeidaraf at gmail.com> 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 at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe

More information about the Haskell-Cafe mailing list