[Haskell-cafe] Monad proof

[Derek Elkins]

On Mon, 2008-04-14 at 16:52 -0700, harke at cs.pdx.edu 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.