3 people like it.

A bind/return computation expression that does not satisfy any of the monad laws

A long overdue counterexample of a pure bind/return computation expression that does not satisfy any of the monad laws, as promised to @silverSpoon. This uses binary trees under the hood, which define a binary operation but do not satisfy any unit or associativity laws. Binary trees can also encode the syntactic structure of a computation expression, which is being captured using a state-updating bind implementation.

 1: 
 2: 
 3: 
 4: 
 5: 
 6: 
 7: 
 8: 
 9: 
10: 
11: 
12: 
13: 
14: 
15: 
16: 
17: 
18: 
19: 
20: 
21: 
22: 
23: 
24: 
25: 
26: 
27: 
28: 
29: 
30: 
31: 
32: 
33: 
34: 
35: 
36: 
37: 
38: 
39: 
40: 
41: 
42: 
43: 
44: 
45: 
46: 
47: 
48: 
type M<'T> = Tree -> Tree * 'T
and Tree = 
    | Leaf
    | Branch of Tree * Tree 

type MBuilder () =
    member __.Return(t : 'T) : M<'T> = fun s -> s,t
    member __.ReturnFrom(m : M<'T>) = m
    member __.Bind(m : M<'T>, g : 'T -> M<'S>) : M<'S> =
        fun mt -> let mt',t = m Leaf in g t (Branch(mt, mt'))

let run (m : M<_>) = fst (m Leaf)

let m = new MBuilder()

// 1. left unit
m {
    let! x = m { return 1 }
    return! m { return x + 1 }
} |> run

m {
    let x = 1
    return! m { return x + 1 }
} |> run

// 2. right unit
m { return 1 } |> run

m {
    let! x = m { return 1 }
    return x
} |> run

// 3. associativity
m {
    let! x = m { return 1 }
    let! y = m { return x + 1 }
    return y
} |> run

m {
    let! y = m { 
        let! x = m { return 1 }
        return! m { return x + 1 }
    }
    return y
} |> run
type M<'T> = Tree -> Tree * 'T

Full name: Script.M<_>
union case Tree.Leaf: Tree
union case Tree.Branch: Tree * Tree -> Tree
type Tree =
  | Leaf
  | Branch of Tree * Tree

Full name: Script.Tree
Multiple items
type MBuilder =
  new : unit -> MBuilder
  member Bind : m:M<'T> * g:('T -> M<'S>) -> M<'S>
  member Return : t:'T -> M<'T>
  member ReturnFrom : m:M<'T> -> M<'T>

Full name: Script.MBuilder

--------------------
new : unit -> MBuilder
member MBuilder.Return : t:'T -> M<'T>

Full name: Script.MBuilder.Return
val t : 'T
Multiple items
type M<'T> = Tree -> Tree * 'T

Full name: Script.M<_>

--------------------
type M<'T> = Tree -> Tree * 'T

Full name: Script.M<_>
val s : Tree
val __ : MBuilder
member MBuilder.ReturnFrom : m:M<'T> -> M<'T>

Full name: Script.MBuilder.ReturnFrom
val m : M<'T>
member MBuilder.Bind : m:M<'T> * g:('T -> M<'S>) -> M<'S>

Full name: Script.MBuilder.Bind
val g : ('T -> M<'S>)
val mt : Tree
val mt' : Tree
val run : m:M<'a> -> Tree

Full name: Script.run
val m : M<'a>
val fst : tuple:('T1 * 'T2) -> 'T1

Full name: Microsoft.FSharp.Core.Operators.fst
val m : MBuilder

Full name: Script.m
val x : int
val y : int
Raw view New version

More information

Link:http://fssnip.net/qR
Posted:2 years ago
Author:Eirik Tsarpalis
Tags: counterexample , monads