Does "Value Restriction" practically mean that there is no higher order functional programming?

Question

Does "Value Restriction" practically mean that there is no higher order functional programming?

I have a problem that each time I try to do a bit of HOP I get caught by a VR error. Example:

let simple (s:string)= fun rq->1 
let oops= simple ""

type 'a SimpleType= F of (int ->'a-> 'a)
let get a = F(fun req -> id)  
let oops2= get ""

and I would like to know whether it is a problem of a prticular implementation of VR or it is a general problem that has no solution in a mutable type-infered language that doesn't include mutation in the type system.

Answer 1

I didn't know the details of the value restriction, so I searched and found this article. Here is the relevant part:

Obviously, we aren't going to write the expression rev [] in a program, so it doesn't particularly matter that it isn't polymorphic. But what if we create a function using a function call? With curried functions, we do this all the time:

- val revlists = map rev;

Here revlists should be polymorphic, but the value restriction messes us up:

- val revlists = map rev;
stdIn:32.1-32.23 Warning: type vars not generalized because of
   value restriction are instantiated to dummy types (X1,X2,...)
val revlists = fn : ?.X1 list list -> ?.X1 list list

Fortunately, there is a simple trick that we can use to make revlists polymorphic. We can replace the definition of revlists with

- val revlists = (fn xs => map rev xs);
val revlists = fn : 'a list list -> 'a list list

and now everything works just fine, since (fn xs => map rev xs) is a syntactic value. (Equivalently, we could have used the more common fun syntax:

- fun revlists xs = map rev xs;
val revlists = fn : 'a list list -> 'a list list

with the same result.) In the literature, the trick of replacing a function-valued expression e with (fn x => e x) is known as eta expansion. It has been found empirically that eta expansion usually suffices for dealing with the value restriction.

To summarise, it doesn't look like higher-order programming is restricted so much as point-free programming. This might explain some of the trouble I have when translating Haskell code to F#.

---

Edit: Specifically, here's how to fix your first example:

let simple (s:string)= fun rq->1 
let oops= (fun x -> simple "" x)     (* eta-expand oops *)

type 'a SimpleType= F of (int ->'a-> 'a)
let get a = F(fun req -> id)
let oops2= get ""

I haven't figured out the second one yet because the type constructor is getting in the way.

Answer 2

Here is the answer to this question in the context of F#. To summarize, in F# passing a type argument to a generic (=polymorphic) function is a run-time operation, so it is actually type-safe to generalize (as in, you will not crash at runtime). The behaviour of thusly generalized value can be surprising though.

For this particular example in F#, one can recover generalization with a type annotation and an explicit type parameter:

type 'a SimpleType= F of (int ->'a-> 'a)
let get a = F(fun req -> id)  
let oops2<'T> : 'T SimpleType = get ""