[Haskell-cafe] Monad proof

[Ryan Ingram]

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 <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
>