A question about "monad laws"

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
68 messages Options
1234
Reply | Threaded
Open this post in threaded view
|

A question about "monad laws"

Deokjae Lee
Tutorials about monad mention the "monad axioms" or "monad laws". The
tutorial "All About Monads" says that "It is up to the programmer to
ensure that any Monad instance he creates satisfies the monad laws".

The following is one of the laws.

(x >>= f) >>= g == x >>= (\v -> f v >>= g)

However, this seems to me a kind of mathematical identity. If it is
mathematical identity, a programmer need not care about this law to
implement a monad. Can anyone give me an example implementation of
monad that violate this law ?
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: A question about "monad laws"

Neil Mitchell
Hi

> The following is one of the laws.
>
> (x >>= f) >>= g == x >>= (\v -> f v >>= g)

Or stated another way:

(x >>= f) >>= g == x >>= (f >>= g)

Now it should be easier to see that this is simply associativity. It's
easy enough to violate, if you want to - but I don't have any nice
simple examples to hand.

Thanks

Neil
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: A question about "monad laws"

Michael Reid-3

Now it should be easier to see that this is simply associativity. It's
easy enough to violate, if you want to - but I don't have any nice
simple examples to hand.


I have recently been reading a tutorial or paper where a Monad that violated this law was presented. The authors shrugged it off as not important, that the notation gained by implementing the operation as a Monad was worth it, but what is not clear is what the consequences of violating such associativity are.

Does violating this law introduce the potential that your program will not do what you think it should?

/mike.

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: A question about "monad laws"

Neil Mitchell
In reply to this post by Neil Mitchell
Hi

> > (x >>= f) >>= g == x >>= (\v -> f v >>= g)
>
> Or stated another way:
>
> (x >>= f) >>= g == x >>= (f >>= g)

Which is totally wrong, woops.

See this page for lots of details about the Monad Laws and quite a
nice explanation of where you use them:
http://www.haskell.org/haskellwiki/Monad_Laws

Thanks

Neil
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: A question about "monad laws"

jerzy.karczmarczuk
In reply to this post by Deokjae Lee
Deokjae Lee cites:

> The tutorial "All About Monads" says that "It is up to the programmer to
> ensure that any Monad instance he creates satisfies the monad laws".
>
> The following is one of the laws.
>
> (x >>= f) >>= g == x >>= (\v -> f v >>= g)
>
> However, this seems to me a kind of mathematical identity. If it is
> mathematical identity, a programmer need not care about this law to
> implement a monad. Can anyone give me an example implementation of
> monad that violate this law ?

After three or five reactions to this posting, I think it it is time to
generalize.

Haskell is not math.

Or rather, there is no way to be sure that the *implementation* of some
mathematical domains and operations thereupon are fool-proof. Sometimes
you break "en passant" some sacred laws. For example the transitivity of
ordering. 5>2, right? and 8>5 as well. But, imagine a - little esoteric
example of cyclic arithmetic modulo 10, where the shortest distance
gives you the order, so 2>8.

A mathematician will shrug, saying that calling +that+ an order relation
is nonsense, and he/she will be absolutely right. But people do that...

There is a small obscure religious sect of people who want to implement
several mathematical entities as functional operators, where multiplication
is f. composition. You do it too generically, too optimistically, and then
some octonions come and break your teeth.

So, people *should care*.


Jerzy Karczmarczuk


_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: A question about "monad laws"

Heinrich Apfelmus
In reply to this post by Deokjae Lee
Deokjae Lee wrote:

> Tutorials about monad mention the "monad axioms" or "monad laws". The
> tutorial "All About Monads" says that "It is up to the programmer to
> ensure that any Monad instance he creates satisfies the monad laws".
>
> The following is one of the laws.
>
> (x >>= f) >>= g == x >>= (\v -> f v >>= g)
>
> However, this seems to me a kind of mathematical identity. If it is
> mathematical identity, a programmer need not care about this law to
> implement a monad. Can anyone give me an example implementation of
> monad that violate this law ?

I will be mean by asking the following counter question:

   x + (y + z) = (x + y) + z

is a mathematical identity. If it is a mathematical identity, a
programmer need not care about this law to implement addition + . Can
anyone give me an example implementation of addition that violates this law?


The only difference here is that the associative law for addition is
"obvious" to you, whereas the associative law for monads is not
"obvious" to you (yet). As Neil mentioned, maybe

   http://www.haskell.org/haskellwiki/Monad_Laws

can help to convince yourself that the associative law monads should be
obvious, too.

In short, the reason for its obviousness is the interpretation of >>= in
terms of sequencing actions with side effects. The law is probably best
demonstration with its special case

   x >> (y >> z) = (x >> y) >> z

In other words, it signifies that it's only the sequence of x,y,z and
not the nesting that matters.


Regards,
apfelmus

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: A question about "monad laws"

Bugzilla from jonathanccast@fastmail.fm
In reply to this post by Deokjae Lee
On 11 Feb 2008, at 5:33 AM, Deokjae Lee wrote:

> Tutorials about monad mention the "monad axioms" or "monad laws". The
> tutorial "All About Monads" says that "It is up to the programmer to
> ensure that any Monad instance he creates satisfies the monad laws".
>
> The following is one of the laws.
>
> (x >>= f) >>= g == x >>= (\v -> f v >>= g)
>
> However, this seems to me a kind of mathematical identity.

What do you mean by identity?  It's easy enough to violate:

newtype Gen a = Gen (StdGen -> a)
runGen :: Gen a -> StdGen -> a
runGen (Gen f) = f
instance Monad Gen where
   return x = Gen (const x)
   a >>= f = Gen (\ r -> let (r1, r2) = split r in runGen (f (runGen  
a r1)) r2) [1]

split returns two generators independent of each other and of its  
argument; thus, this `monad' violates all *three* of the monad laws,  
in the sense of equality.  So, for example, the program

do
   x <- a
   return x

denotes a random variable independent of (and hence distinct from)  
a.  In general, you want some kind of backstop `equality' (e.g., that  
the monad laws hold in the sense of identical distribution) when you  
violate them; otherwise, you will violate the expectations your users  
have from the syntax of the do notation.

jcc

[1] Test.QuickCheck
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Re: A question about "monad laws"

Andrew Butterfield
In reply to this post by Heinrich Apfelmus
apfelmus wrote:

> Deokjae Lee wrote:
>> Tutorials about monad mention the "monad axioms" or "monad laws". The
>> tutorial "All About Monads" says that "It is up to the programmer to
>> ensure that any Monad instance he creates satisfies the monad laws".
>>
>> The following is one of the laws.
>>
>> (x >>= f) >>= g == x >>= (\v -> f v >>= g)
>>
>> However, this seems to me a kind of mathematical identity. If it is
>> mathematical identity, a programmer need not care about this law to
>> implement a monad. Can anyone give me an example implementation of
>> monad that violate this law ?
>
> I will be mean by asking the following counter question:
>
>   x + (y + z) = (x + y) + z
>
> is a mathematical identity. If it is a mathematical identity, a
> programmer need not care about this law to implement addition + . Can
> anyone give me an example implementation of addition that violates
> this law?
Hugs> 1.0 + (2.5e-15 + 2.5e-15)
1.00000000000001 :: Double
Hugs> (1.0 + 2.5e-15) + 2.5e-15
1.0 :: Double

Hugs, on Pentium 4 machine  running Windows XP SP2 (all of which is
largely irrelevant!)

This is precisely Jerzy's point - you can have many mathematical laws as
you like but there is no guarantee
that a programming languages implementation will  satisfy them.

The above example is due to rounding errors and arises because the
Double type in Haskell (or C, C++, whatever)
is a finite (rational) approximation to real numbers which are infinite
(platonic) entities.

Associativity of addition applies for platonic reals, but not their
widely used IEEE-standard approximate implementation
on standard hardware.

For monads, the situation is slightly different.
Haskell describes the signature of the monadic operators

return :: x -> m x
(>>=) :: m a -> (a -> m b) -> m b

but cannot restrict how you actually instantiate these.
It admonishes you by stating that you should obey the relevant laws, but
cannot enforce this.

(of course, technically if you implement a dodgy monad, its not really a
monad at all, but something
different with operators with the same name and types - also technically
values of type Double are
not real numbers, (or true rationals either !)

let m denote the "list monad" (hypothetically). Let's instantiate:

return :: x -> [x]
return x = [x,x]

(>>=) :: [x] -> (x -> [y]) -> [y]
xs >>= f   =  concat ((map f) xs)

Let g n = [show n]

Here  (return 1 >>= g ) [1,2,3] = ["1","1","1","1","1","1"]
but  g[1,2,3] = ["1","2","3"],
thus violating the first monad law   | return
<http://haskell.org/ghc/docs/latest/html/libraries/base/Prelude.html#v:return>
a >>=
<http://haskell.org/ghc/docs/latest/html/libraries/base/Prelude.html#v:&gt;&gt;=>
f  =  f a

|

--------------------------------------------------------------------
Andrew Butterfield     Tel: +353-1-896-2517     Fax: +353-1-677-2204
Foundations and Methods Research Group Director.
Course Director, B.A. (Mod.) in CS and ICT degrees, Year 4.
Department of Computer Science, Room F.13, O'Reilly Institute,
Trinity College, University of Dublin, Ireland.
                            http://www.cs.tcd.ie/Andrew.Butterfield/
--------------------------------------------------------------------

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Re: A question about "monad laws"

Felipe Lessa
On Feb 11, 2008 1:35 PM, Andrew Butterfield
<[hidden email]> wrote:
> Hugs> 1.0 + (2.5e-15 + 2.5e-15)
> 1.00000000000001 :: Double
> Hugs> (1.0 + 2.5e-15) + 2.5e-15
> 1.0 :: Double

Prelude> (1e30 + (-1e30)) + 1
1.0
Prelude> 1e30 + ((-1e30) + 1)
0.0

I love this example from David Goldberg
(http://docs.sun.com/source/806-3568/ncg_goldberg.html).

--
Felipe.
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Re: A question about "monad laws"

Arnar Birgisson
In reply to this post by Heinrich Apfelmus
Hi all,

On Feb 11, 2008 3:14 PM, apfelmus <[hidden email]> wrote:
> I will be mean by asking the following counter question:
>
>    x + (y + z) = (x + y) + z
>
> is a mathematical identity. If it is a mathematical identity, a
> programmer need not care about this law to implement addition + . Can
> anyone give me an example implementation of addition that violates this law?

Depends on what you mean by "addition". In general, algebraists call
any associative and commutative operation on a set "addition", and
nothing else. From that POV, there is by definition no "addition" that
violates this law.

Arnar
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Re: A question about "monad laws"

Andrew Butterfield
In reply to this post by Andrew Butterfield
Andrew Butterfield wrote:

> let m denote the "list monad" (hypothetically). Let's instantiate:
>
> return :: x -> [x]
> return x = [x,x]
>
> (>>=) :: [x] -> (x -> [y]) -> [y]
> xs >>= f   =  concat ((map f) xs)
>
> Let g n = [show n]
>
> Here  (return 1 >>= g ) [1,2,3] = ["1","1","1","1","1","1"]
> but  g[1,2,3] = ["1","2","3"],
> thus violating the first monad law   | return
> <http://haskell.org/ghc/docs/latest/html/libraries/base/Prelude.html#v:return>
> a >>=
> <http://haskell.org/ghc/docs/latest/html/libraries/base/Prelude.html#v:&gt;&gt;=>
> f  =  f a
>
I messed this up - I was trying for the simplest example I could get !
Apologies.

Start over:

Program ----------------------------------------------------

module BadMonad where
import Monad

newtype MyList t = MyList [t]

instance Show t => Show (MyList t) where
  show (MyList xs) = show xs

unmylist (MyList xs) = xs

myconcat xs = MyList (concat (map unmylist xs))

instance Monad MyList  where
  return x  =  MyList [x,x]
  (MyList xs) >>= f  =  myconcat ((map f) xs)

i2s :: Int -> MyList Char
i2s x = MyList (show x)

m = i2s 9

Hugs transcript ----------------------------------------

BadMonad> m
"9" :: MyList Char
BadMonad> m >>= return
"99" :: MyList Char

We violate the second law (Right Identity, m = m >>= return )


--
--------------------------------------------------------------------
Andrew Butterfield     Tel: +353-1-896-2517     Fax: +353-1-677-2204
Foundations and Methods Research Group Director.
Course Director, B.A. (Mod.) in CS and ICT degrees, Year 4.
Department of Computer Science, Room F.13, O'Reilly Institute,
Trinity College, University of Dublin, Ireland.
                            http://www.cs.tcd.ie/Andrew.Butterfield/
--------------------------------------------------------------------

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Re: A question about "monad laws"

Bugzilla from jonathanccast@fastmail.fm
In reply to this post by Arnar Birgisson
On 11 Feb 2008, at 7:52 AM, Arnar Birgisson wrote:

> Hi all,
>
> On Feb 11, 2008 3:14 PM, apfelmus <[hidden email]> wrote:
>> I will be mean by asking the following counter question:
>>
>>    x + (y + z) = (x + y) + z
>>
>> is a mathematical identity. If it is a mathematical identity, a
>> programmer need not care about this law to implement addition + . Can
>> anyone give me an example implementation of addition that violates  
>> this law?
>
> Depends on what you mean by "addition". In general, algebraists call
> any associative and commutative operation on a set "addition", and
> nothing else. From that POV, there is by definition no "addition" that
> violates this law.

I agree.  The Num Double instance should be expelled from the Prelude  
immediately.

jcc

(What?  Haskell has a Float type?)

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: A question about "monad laws"

MigMit
In reply to this post by Deokjae Lee
> (x >>= f) >>= g == x >>= (\v -> f v >>= g)
>
> However, this seems to me a kind of mathematical identity. If it is
> mathematical identity, a programmer need not care about this law to
> implement a monad. Can anyone give me an example implementation of
> monad that violate this law ?

It's well known that "ListT m" monad violates this law in general  
(though it satisfies it for some particular monads m). For example,

Prelude Control.Monad.List> runListT ((ListT [[(),()]] >> ListT [[()],
[()]]) >> ListT [[1],[2]])
[[1,1],[1,2],[2,1],[2,2],[1,1],[1,2],[2,1],[2,2],[1,1],[1,2],[2,1],
[2,2],[1,1],[1,2],[2,1],[2,2]]
Prelude Control.Monad.List> runListT (ListT [[(),()]] >> (ListT [[()],
[()]] >> ListT [[1],[2]]))
[[1,1],[1,2],[1,1],[1,2],[2,1],[2,2],[2,1],[2,2],[1,1],[1,2],[1,1],
[1,2],[2,1],[2,2],[2,1],[2,2]]

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: A question about "monad laws"

Dan Piponi-2
IOn Feb 11, 2008 9:46 AM, Miguel Mitrofanov <[hidden email]> wrote:
> It's well known that "ListT m" monad violates this law in general
> (though it satisfies it for some particular monads m). For example,

I went through this example in quite a bit of detail a while ago and
wrote it up here:
http://sigfpe.blogspot.com/2006/11/why-isnt-listt-monad.html . I tried
to show not just why the monad laws fails to hold for ListT [], but
also show how it almost holds.
--
Dan
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: A question about "monad laws"

Wolfgang Jeltsch-2
In reply to this post by Michael Reid-3
Am Montag, 11. Februar 2008 14:57 schrieb Michael Reid:

> > Now it should be easier to see that this is simply associativity. It's
> > easy enough to violate, if you want to - but I don't have any nice
> > simple examples to hand.
>
> I have recently been reading a tutorial or paper where a Monad that
> violated this law was presented. The authors shrugged it off as not
> important, that the notation gained by implementing the operation as a
> Monad was worth it, but what is not clear is what the consequences of
> violating such
> associativity are.
>
> Does violating this law introduce the potential that your program will not
> do what you think it should?
>
> /mike.

Other libraries might (and probably will) expect Monad instances to satisfy
the monad laws and will not work as intended or even make sense if the monad
laws aren’t satisfied.

Sometimes it looks as if people think that monads are special in that they
have to satisfy certain laws.  But this isn’t the case.  Practically every
Haskell type class has some laws (informally) attached to it which instances
should satisfy.  For example, the following should hold for instances of the
Ord class:

    a < b = compare a b = LT
    a == b = compare a b = EQ
    a > b = compare a b = GT
    a <= b = a < b || a == b
    a >= b = a > b || a == b
    a < b = b > a
    a < b && b < c => a < c

If an Ord instances doesn’t obey these laws than it’s likely to make Set and
Map behave strangely.

Best wishes,
Wolfgang
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Re: A question about "monad laws"

Wolfgang Jeltsch-2
In reply to this post by Andrew Butterfield
Am Montag, 11. Februar 2008 16:35 schrieb Andrew Butterfield:
> This is precisely Jerzy's point - you can have many mathematical laws as
> you like but there is no guarantee that a programming languages
> implementation will satisfy them.

But people writing instances of type classes should take care of satisfying
the laws since other libraries will most likely expect this.

Best wishes,
Wolfgang
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: A question about "monad laws"

Stefan O'Rear
In reply to this post by Neil Mitchell
On Mon, Feb 11, 2008 at 01:59:09PM +0000, Neil Mitchell wrote:

> Hi
>
> > > (x >>= f) >>= g == x >>= (\v -> f v >>= g)
> >
> > Or stated another way:
> >
> > (x >>= f) >>= g == x >>= (f >>= g)
>
> Which is totally wrong, woops.
>
> See this page for lots of details about the Monad Laws and quite a
> nice explanation of where you use them:
> http://www.haskell.org/haskellwiki/Monad_Laws
My favorite presentation of the monad laws is associativity of Kliesli
composition:

(a1 >=> a2) x = a1 x >>= a2   -- predefined in 6.8 control.monad

-- The laws

return >=> a    = a
a >=> return    = a
a >=> (b >=> c) = (a >=> b) >=> c

Stefan

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe

signature.asc (196 bytes) Download Attachment
Reply | Threaded
Open this post in threaded view
|

Re: A question about "monad laws"

David Benbennick
In reply to this post by Wolfgang Jeltsch-2
On Feb 11, 2008 11:24 AM, Wolfgang Jeltsch <[hidden email]> wrote:
>     a < b && b < c => a < c
>
> If an Ord instances doesn't obey these laws than it's likely to make Set and
> Map behave strangely.

Some months ago I pointed out that Ratio Int (which is an Ord
instance) doesn't satisfy this property.  I provided a patch to fix
the problem, but my bug report was closed as wontfix:
http://hackage.haskell.org/trac/ghc/ticket/1517.


--
I'm doing Science and I'm still alive.
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: A question about "monad laws"

Ben Franksen
In reply to this post by Dan Piponi-2
Dan Piponi wrote:
> IOn Feb 11, 2008 9:46 AM, Miguel Mitrofanov <[hidden email]> wrote:
>> It's well known that "ListT m" monad violates this law in general
>> (though it satisfies it for some particular monads m). For example,
>
> I went through this example in quite a bit of detail a while ago and
> wrote it up here:
> http://sigfpe.blogspot.com/2006/11/why-isnt-listt-monad.html . I tried
> to show not just why the monad laws fails to hold for ListT [], but
> also show how it almost holds.

...and the Unimo paper[1] explains how to easily write a 'correct' ListT.
BTW, Unimo is an extreme case of the monad laws holding only w.r.t.
the 'right' equality, i.e. in the laws m == m' is to be understood as

  observe_monad m == observe_monad m'

(and even this '==' is of course /not/ the Eq class method but a semantic
equality.)

[1] http://web.cecs.pdx.edu/~cklin/papers/unimo-143.pdf

Cheers
Ben

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Re: A question about "monad laws"

Richard A. O'Keefe
In reply to this post by Andrew Butterfield
On 12 Feb 2008, at 4:35 am, Andrew Butterfield wrote:
[floating point addition is not associative]

And this is an excellent example of why violating expected laws is BAD.
The failure of floating point addition to be associative means that  
there
are umpteen ways of computing polynomials, for example, and doing it  
different
ways will give you different answers.  This is *not* a good way to write
reliable software.  I did enough Numerical Analysis papers in my pre-
PhD years
to get quite scared sometimes.  Oh, here's a good one:

        dot1 [] [] = 0
        dot1 (x:xs) (y:ys) = x*y + dots1 xs ys

Obvious naive code for dot product.  Switch over to tail recursion

        dot2 xs ys = aux xs ys 0
          where aux [] [] s = s
                aux (x:xs) (y:ys) s = aux xs ys (s + x*y)

The problem is that (a) in floating point arithmetic these two functions
give DIFFERENT answers, and (b) NEITHER of them is wrong (arguably,  
neither
of them is right either).  For integers, of course, they must agree  
(if I
haven't made any silly mistakes).

This kind of thing makes it incredibly hard to think about numerical
calculations.

Basically, laws are stated so that implementors will make stuff that
clients don't have to think about until their brains melt.

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
1234