How does the Delay exactly works in continuation monad to prevent stackoverflow?

Question

This is a reference question to this: StackOverflow in continuation monad
with whom I played a little and would need a few clarifications.

1) I suppose this:

member this.Delay(mk) = fun c -> mk () c

makes the behavior in computational workflow do the diffrence as showed by toyvo between these:

cBind (map xs) (fun xs -> cReturn (f x :: xs))  

cBind (fun c -> map xs c) (fun xs -> cReturn (f x :: xs))

So I don't exactly understand what is the trick, when
(fun c -> map xs c) is only different notation of (map xs)

2) Inference issue. - In OP's second map example I found out it doesn't compile due to inference problem with v value, because it infers f as a -> b list, instead of desired a -> b. Why it infers in this way? In case let v = f x it would infer well.

3) It seems to me that VS shows inaccurate type signatures in the tooltips: return type of the monad's Return is: ('e->'f)->f, while the return type of the Bind is only 'c->'b. -It seems it simplify ('e->'f) to only c in the Bind case, or am I missing something here?

Thanks for the clarification,
tomas

Edit - testing dump:

let cReturn x = fun k -> k x
let cBind m f = 
    printfn "cBind %A" <| m id
    fun c -> m (fun a -> f a c)

let map_fixed f xs =
  let rec map xs =
    printfn "map %A" xs
    match xs with
      | [] -> cReturn []
      | x :: xs -> cBind (fun c -> map xs c) (fun xs -> cReturn (f x :: xs)) 
  map xs (fun x -> x)

let map f xs =
  let rec map xs =
    printfn "map %A" xs
    match xs with
      | [] -> cReturn []
      | x :: xs -> cBind (map xs) (fun xs -> cReturn (f x :: xs)) 
  map xs (fun x -> x)

[1..2] |> map_fixed ((+) 1) |> printfn "%A"
[1..2] |> map ((+) 1) |> printfn "%A"

map_fixed:
map [1; 2] map [2] map [] cBind [] map [] cBind [3] map [2] map [] cBind [] map [] [2; 3]

map:
map [1; 2] map [2] map [] cBind [] cBind [3] [2; 3]

Edit to question 2:

let map f xs =
    let rec map xs =
        cont {
            match xs with
            | [] -> return []
            | x :: xs ->
                let v = f x // Inference ok
                //let! v = cont { return f x } // ! Inference issue - question 2
                let! xs = map xs
                return v :: xs
        }
    map xs id

Answer 1

The issue is exactly that fun c -> map xs c is not the same as map xs. They have the same "meaning" in some sense, but their runtime semantics are different. In the latter case, evaluating the expression results in an immediate call to the map function with xs as an argument (returning another function as the result). On the other hand, evaluating fun c -> map xs c does not result in an immediate call to map! The call to map is delayed until the resulting function is actually applied. This is the critical difference that prevents a stack overflow.

Regarding your other questions, I can't quite make out what you're asking in your second question. For your third question, the compiler has inferred the most general type possible for Bind. You're right that the traditional type that you might expect is more specific than this, but it's not really a problem that you can call Bind in a wider set of contexts than is strictly necessary. And if you really want a more specific type, you can always add annotations to constrain the signature.