Another bind/return computation expression that does not satisfy the monad laws

c.f. http://fssnip.net/qR In this example different syntactic structures result in different types.

 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 T = interface end
type L = inherit T
type B<'T1, 'T2 when 'T1 :> T and 'T2 :> T> = inherit T

type M<'C, 'T when 'C :> T> = M of (unit -> 'T)

type MBuilder () =
    member __.Return(t : 'T) : M<L,'T> = M(fun () -> t)
    member __.ReturnFrom(m : M<_,_>) = m
    member __.Bind((M f) : M<'C1,'T>, g : 'T -> M<'C2, 'S>) : M<B<'C1,'C2>, 'S> =
        M(fun () -> let t = f () in let (M sf) = g t in sf ())


let m = new MBuilder()

// 1. left unit
let u1l = m {
    let! x = m { return 1 }
    return! m { return x + 1 }
}

let u1r = m {
    let x = 1
    return! m { return x + 1 }
}

// 2. right unit
let u2l = m { return 1 }

let u2r = m {
    let! x = m { return 1 }
    return x
}

// 3. associativity
let assl = m {
    let! x = m { return 1 }
    let! y = m { return x + 1 }
    return y
}

let assr = m {
    let! y = m { 
        let! x = m { return 1 }
        return! m { return x + 1 }
    }
    return y
}

type T

Full name: Script.T

type L =
  interface
    inherit T
  end

Full name: Script.L

type B<'T1,'T2 (requires 'T1 :> T and 'T2 :> T)> =
  interface
    inherit T
  end

Full name: Script.B<_,_>

type M<'C,'T (requires 'C :> T)> = | M of (unit -> 'T)

Full name: Script.M<_,_>

union case M.M: (unit -> 'T) -> M<'C,'T>

type unit = Unit

Full name: Microsoft.FSharp.Core.unit

Multiple items
type MBuilder =
  new : unit -> MBuilder
  member Bind : M<'C1,'T> * g:('T -> M<'C2,'S>) -> M<B<'C1,'C2>,'S> (requires 'C1 :> T and 'C2 :> T)
  member Return : t:'T -> M<L,'T>
  member ReturnFrom : m:M<'a,'b> -> M<'a,'b> (requires 'a :> T)

Full name: Script.MBuilder

--------------------
new : unit -> MBuilder

member MBuilder.Return : t:'T -> M<L,'T>

Full name: Script.MBuilder.Return

val t : 'T

val __ : MBuilder

member MBuilder.ReturnFrom : m:M<'a,'b> -> M<'a,'b> (requires 'a :> T)

Full name: Script.MBuilder.ReturnFrom

val m : M<#T,'b>

member MBuilder.Bind : M<'C1,'T> * g:('T -> M<'C2,'S>) -> M<B<'C1,'C2>,'S> (requires 'C1 :> T and 'C2 :> T)

Full name: Script.MBuilder.Bind

val f : (unit -> 'T)

val g : ('T -> M<#T,'S>)

val sf : (unit -> 'S)

val m : MBuilder

Full name: Script.m

val u1l : M<B<L,L>,int>

Full name: Script.u1l

val x : int

val u1r : M<L,int>

Full name: Script.u1r

val u2l : M<L,int>

Full name: Script.u2l

val u2r : M<B<L,L>,int>

Full name: Script.u2r

val assl : M<B<L,B<L,L>>,int>

Full name: Script.assl

val y : int

val assr : M<B<B<L,L>,L>,int>

Full name: Script.assr

Raw view Test code New version

More information

Link:	http://fssnip.net/qS
Posted:	8 years ago
Author:	Eirik Tsarpalis
Tags:	counterexample