21

From the Haskell wiki:

Monads can be viewed as a standard programming interface to various data or control structures, which is captured by the Monad class. All common monads are members of it:

class Monad m where
  (>>=) :: m a -> (a -> m b) -> m b
  (>>) :: m a -> m b -> m b
  return :: a -> m a
  fail :: String -> m a

In addition to implementing the class functions, all instances of Monad should obey the following equations, or Monad Laws:

return a >>= k  =  k a
m >>= return  =  m
m >>= (\x -> k x >>= h)  =  (m >>= k) >>= h

Question: Are the three monad laws at the bottom actually enforced in any way by the language? Or are they extra axioms that you must enforce in order for your language construct of a "Monad" to match the mathematical concept of a "Monad"?

10
  • 7
    They are not enforced by the language or compiler. The programmer is responsible for making sure the laws hold.
    – ErikR
    May 9, 2016 at 20:11
  • Since Haskell is a Turing complete language, you cannot enforce any laws on its functions. May 9, 2016 at 20:47
  • 9
    @WillemVanOnsem That's really misleading. A turning complete language can still have a proof system and provide guarantees about operations. For example, many extensions (often SMT based) on top of Haskell can prove the monad laws - do these new extended language suddenly become non-Turing-complete? May 9, 2016 at 20:59
  • 1
    @ThomasM.DuBuisson I guess it is impossible in general to automatically determine if the monad laws are satisfied in a Turing Complete Language: en.wikipedia.org/wiki/Rice%27s_theorem
    – PyRulez
    May 10, 2016 at 1:27
  • 1
    @ThomasM.DuBuisson: I would compare it with the halting problem which is well studied. There exists a lot of heuristics that can prove, for most programs whether they will halt for a given input. But you cannot construct a prover that will prove it for any instance. The same holds for monads: you cannot construct a prover that can prove whether monadic laws will hold. But you can get lucky that for a given defintion a heuristic can prove it. That's the consequence of Rice's theorem I think. May 11, 2016 at 20:37

2 Answers 2

22

You are responsible for enforcing that a Monad instance obeys the monad laws. Here's a simple example that doesn't.

Even though its type is compatible with the Monad methods, counting the number of times the bind operator has been used isn't a Monad because it violates the law m >>= return = m

{-# Language DeriveFunctor #-}

import Control.Monad

data Count a = Count Int a
    deriving (Functor, Show)

instance Applicative Count where
    pure = return
    (<*>) = ap

instance Monad Count where
    return = Count 0
    (Count c0 a) >>= k = 
        case k a of
            Count c1 b -> Count (c0 + c1 + 1) b
12

No, the monad laws are not enforced by the language. But if you don't adhere to them, your code may not necessarily behave as you'd expect in some situations. And it would certainly be confusing to users of your code.

Your Answer

Reminder: Answers generated by Artificial Intelligence tools are not allowed on Stack Overflow. Learn more

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.