0 people like it.

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

More information

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