3 people like it.
Like the snippet!

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 Test code New version

More information

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