Re: [Haskell-cafe] Monad proof
Here's part of a pencil-and-paper proof of laws for a state monad. Before doing so, I've got a question of my own about the *other* laws: Is there a place where somebody has explicitly written the laws that non-proper morphisms of commonly used monads? Back to the original question... Beware. What I'm about to say doesn't quite work in Haskell, for two reasons. First, you can't make my definition into an instance of the class Monad without inserting type constructors into inconvenient places. Second, due to the way undefined works in Haskell, the state monad doesn't obey all the laws. Assume we don't have non-termination, and assume we don't care about overloading (=) and return (so we don't need to shoe-horn our monad into the monad type class). Preliminaries. From the Prelude we have: curry :: ((a,b) - c) - a - b - c uncurry :: (a - b - c) - (a,b) - c id :: a - a We define the state monad to be a synonym for a function returning a pair: M a = s - (a,s) Define morphisms return = curry id -- where id is specialized to type (a,s) - (a,s) m = k = (uncurry k) . m get = \s - (s,s) put s = \_ - ((),s) Now check the laws. Of the basic 3, I'll only do associativity. The other 2 are easier. Take the two sides of the conjectured law and unfold the definition of = (and return), then use properties of uncurry (and curry) to massage them into the same form. If you can do so, the law holds. (I'm going to avoid unfolding the definition of (un)curry so I can stay at a higher level of abstraction, though the following might be shorter if I did unfold them.) LHS == (p = q) = r == uncurry r . (p = q) == uncurry r . (uncurry q . p) RHS = == p = (\x - q x = r) == uncurry (\x - q x = r) . p == uncurry (\x - uncurry r . q x) . p == uncurry (\x s - (uncurry r . q x) s) . p == uncurry (\x s - uncurry r (q x s)) . p == (\xs - uncurry r (q (fst xs) (snd xs))) . p == (\xs - uncurry r (uncurry q xs)) . p == (\xs - (uncurry r . uncurry q) xs) . p == (uncurry r . uncurry q) . p Now, one thing that's equally interesting (and perhaps not spoken of often enough) is the laws that the non-proper morphisms obey. In the case of state: put a get == put a return a where each side reduces to \_ - (a,a) get get == get where each side reduces to \s - ((),s) BTW, in a proof assistant like Coq, Isabelle or Agda these identities can be verified much more easily (though a badly done proof script may be unreadable.) On Fri, Apr 11, 2008 at 02:35:28PM -0300, Rafael C. de Almeida 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 -- Tom Harke Portland State University ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Monad proof
On Mon, 2008-04-14 at 16:52 -0700, [EMAIL PROTECTED] wrote: Here's part of a pencil-and-paper proof of laws for a state monad. Before doing so, I've got a question of my own about the *other* laws: Is there a place where somebody has explicitly written the laws that non-proper morphisms of commonly used monads? Back to the original question... Beware. What I'm about to say doesn't quite work in Haskell, for two reasons. First, you can't make my definition into an instance of the class Monad without inserting type constructors into inconvenient places. Second, due to the way undefined works in Haskell, the state monad doesn't obey all the laws. Assume we don't have non-termination, and assume we don't care about overloading (=) and return (so we don't need to shoe-horn our monad into the monad type class). Preliminaries. From the Prelude we have: curry :: ((a,b) - c) - a - b - c uncurry :: (a - b - c) - (a,b) - c id :: a - a A shorter version. First, verify that curry and uncurry make an isomorphism. (They don't in Haskell because of seq, this is where we close our eyes and stick our fingers in our ears.) Then curry and uncurry define an adjunction: (,) a -| (-) a State is the monad of that adjunction. QED. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Monad proof
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
Re: [Haskell-cafe] Monad proof
Did you see this? http://okmij.org/ftp/Computation/proving-monad-laws.txt []'s Rodrigo Geraldo Ribeiro. PhD student - UFMG On Fri, Apr 11, 2008 at 2:35 PM, 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
Re: [Haskell-cafe] Monad proof
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
