Why does ML's Value Restriction stop you from capturing parametric values?

Here the MLton manual explains ML's value restriction. Specifically, it disallows functions to take on multiple parametric instantiations if they have a closure over local variables.

Edit: note from the answer that the MLton manual is wrong about the value restriction. See instead Real World Ocaml.

Why is this a problem in ML when C# can easily form closures over parametric variables?

For example, this code is invalid, because ML will not allow this function to parameterize over int and string in the same program, because it has a let binding.

val f = let in fn x => x end
val _ = (f "foo"; f 13)


However, I can easily make a C# function which captures a parameterized variable, and parametrically instantiate it over both int and string. I've made the example more convincing, because a literal translation of the above ML is a trivial C# program.

class Program {

static Func<A> foo<A>(Func<A,A,A> fn, A initial, A accumulate) {
A cur = initial;
return () => {  cur = fn(cur,accumulate); return cur;};
}

static void Main(string[] args) {
var my_bar_a = foo( (x,y) => { return x+y;}, 0, 1);
var my_bar_b = foo( (x,y) => { return x+y; }, ":", "-");

Console.WriteLine("a: " + my_bar_a().ToString());
Console.WriteLine("a: " + my_bar_a().ToString());
Console.WriteLine("b: " + my_bar_b().ToString());
Console.WriteLine("b: " + my_bar_b().ToString());
Console.WriteLine("a: " + my_bar_a().ToString());
Console.WriteLine("b: " + my_bar_b().ToString());
}
}

output as expected:

a: 1
a: 2
b: :-
b: :--
a: 3
b: :---


Why does ML prevent us from doing this?

However, I can easily make a C# function which captures a parameterized variable, and parametrically instantiate it over both int and string.

The equivalent to code forbidden by value restriction would need a generic local variable of type which would be written something like Func<A, A> foo<A> = ..., which isn't legal in C# (though it isn't enough to violate value restriction, it's required). In your case my_bar_a and my_bar_b do not themselves have generic parameters.

If C# did allow generic local variables then it would need something like the value restriction.

Your C# example doesn't trigger the value restriction at all. Here it is in OCaml:

# let foo f init acc =
let cur = ref init in
(fun () -> cur := f !cur acc ; !cur) ;;
val foo : ('a -> 'b -> 'a) -> 'a -> 'b -> unit -> 'a = <fun>

# let my_bar_a = foo (+) 0 1 ;;
val my_bar_a : unit -> int = <fun>
# let my_bar_b = foo (^) ":" "-" ;;
val my_bar_b : unit -> string = <fun>

# my_bar_a () ;;
- : int = 1
# my_bar_a () ;;
- : int = 2
# my_bar_b () ;;
- : string = ":-"
# my_bar_b () ;;
- : string = ":--"
# my_bar_a () ;;
- : int = 3
# my_bar_b () ;;
- : string = ":---"


Note that your initial example shouldn't trigger it either:

let f = fun x -> x in f "plop", f 2 ;;
- : string * int = ("plop", 2)


f here is a non mutable value, it can be safely generalized.

The ML value restriction doesn't stop you from capturing parametric values as long as, given a unique reference, it will only be instantiated with a unique type. This is the case in your C# example: the reference cell is created for each new function.

I'm not extremely fond of the MLTON manual. You can read Real World OCaml for a decent introduction to the value restriction here. OCaml also has extensions to the value restriction when type parameters are in covariant position, which you can read about in Jacque Garrigue's paper.