Monad Law test doesn't quite limit to valid monads?

[farlee2121]

I've been working on understanding monads. A key question I asked to clarify the rules was: are a bind and return that always return a constant value a valid monad? Example

let return val = ConstantMonad.Value
let bind f x = ConstantMonad.Value

I found some monad law properties in the test suite for FsCheck.

I thought, I'll refactor this to take an arbitrary return and bind, and see if my definition passes.

It did, but further reading (haskell wiki, Scott Wlaschin) seems to indicate that this is incorrect.

I believe the culprit is let f = f >> Gen.constant.

Maybe this doesn't matter for the case in your test suite, but I thought I would point it out.

Here is my generalized version of the ruleset, if it is of interest.

module MonadLaws =
    let LeftIdentity bind _return (a:'a) (f:'a -> 'b) =
        let f = f >> _return
        let left = (bind (_return a)  f)
        let right = f a
        left = right 
    let RightIdentity bind _return (a:'a) =
        let m = _return a
        let left = bind m _return
        let right = m
        left = right
    let Associativity bind _return (a:'a) (f:'a->'b) (g:'b->'c) =
        let m = _return a
        let f = f >> _return
        let g = g >> _return
        let left = bind (bind m f) g
        let right =  bind m (fun x -> bind (f x)  g)
        left = right

    let All bind _return =
        (LeftIdentity bind _return) |@ "Left Identity"
        .&. (RightIdentity bind _return) |@ "RightIdentity"
        .&. (Associativity bind _return) |@ "Associativity"

type EmptyMonad<'a> = 
    | Empty

[<Fact>]
let ``should satisfy Monad laws``() =
    //let bind = (>>=)
    //let _return = Gen.constant
    let bind x f = Empty
    let _return x = Empty
    Check.Quick (MonadLaws.All bind _return)

[kurtschelfthout]

The test can indeed be made stronger and more general.

That said, I don’t see why EmptyMonad isn’t a monad. If anything it’s probably a bit too loosely typed (eg the return type of bind isn’t necessarily the return type of f, as written)

Can you show how any of the laws are violated?

[farlee2121]

Please correct me if I'm misinterpreting. "So that is exactly the first monad law: it says that this lifted function [the id function] must be the same as the id function in the elevated world." source

That tells me that lifting the function identity x = x should be the same as if we implemented the function directly on the monad type. This is not true of my return and bind that always return constant values.

I suppose the counter to this could be that the monad space only has one value, so only one value could be passed to the identity function and thus the monad is still valid.

If we constrained the return type of bind, like you point out, then it could only have the one return value no matter what's it is passed anyway...

[kurtschelfthout]

What may be confusing is that strictly speaking EmptyMonad has only one value, but it doesn't "wrap" any underlying value like useful monads do, so in that sense it's equivalent to Empty of Void where Void doesn't have any values whatsoever.

That makes it impossible to write a bind in the usual style

let bind ma f =
    let a = getContents ma  // Empty has no contents, so a can't have a value
    let mb = f a // f a can only have on implementation, which is to return Empty
    mb

But given that your monad only has one value, the result of this must be Empty which is equal to any other Empty (in fact there isn't even "another Empty"). So all monad laws trivially hold - it doesn't matter how bind or return are implemented.

Compare with monad operations for Identity a = Identity of a and Const b a = Const of a

[kurtschelfthout]

Actually that first paragraph is not quite right. In another sense EmptyMonad can wrap any value, but immediately forgets about it. (Empty is not equivalent to Empty of Void because the latter can't be created...)

[farlee2121]

You make a good point. Rather than empty, a better name would be ForgetfulMonad.

I'm guessing your definitions align with this article where

• Identity monad: is a behaviorless wrapper that simply contains any value its given
• Const monad: always preserves the first value that was instantiated.

The Identity monads seem to be a bit different. It would actually preserve semantic of the identity function implementation when lifted. Const seems similar to what I proposed, but this article suggests an implementation similar to mine is not a real monad and this article says it is a real monad.

Overall, I'm not having much luck finding sources on the on Const monad. Any particular sources you think I should read?

Also, thank you for discussing this with me! And also thank you for such a wonderful testing library!

[kurtschelfthout]

(Looks like all three links point to the same article?)

Indeed, Const is not a monad. It violates left identity law. Good tiny exercise :) Goes to show you always should check these things...I ran across Const while learning about Van Laarhoven lenses, where they are used as applicatives to implement certain lens operations.

Light Googling pointed me at https://stackoverflow.com/questions/11530412/monad-for-const which will spoil the exercise above.

Your Empty type is equivalent to Const of unit which is a monad, again because there is just one possible value as pigworker points out in the comment.

[farlee2121]

Oops. That Stackoverflow thread was supposed to be the other link.

At first I thought that the Const () case was different than mine, but I can see the equivalence now that you mention it. Looks like I've got some reading to do on lenses now too.

Thanks for your help!