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

Does “Value Restriction” mean that there is no higher order functional programming?

Absolutely not! The value restriction barely interferes with higher-order functional programming at all. What it does do is restrict some applications of polymorphic functions—not higher-order functions—at top level.

---

Let's look at your example. Your problem is that oops and oops2 are both the identity function and have type forall 'a . 'a -> 'a. In other words each is a polymorphic value. But the right-hand side is not a so-called "syntactic value"; it is a function application. (A function application is not allowed to return a polymorphic value because if it were, you could construct a hacky function using mutable references and lists that would subvert the type system; that is, you could write a terminating function type type forall 'a 'b . 'a -> 'b.

Luckily in almost all practical cases, the polymorphic value in question is a function, and you can define it by eta-expanding:

let oops x = simple "" x

This idiom looks like it has some run-time cost, but depending on the inliner and optimizer, that can be got rid of by the compiler—it's just the poor typechecker that is having trouble.

The oops2 example is more troublesome because you have to pack and unpack the value constructor:

let oops2 = F(fun x -> let F f = get "" in f x)

This is quite a but more tedious, but the anonymous function fun x -> ... is a syntactic value, and F is a datatype constructor, and a constructor applied to a syntactic value is also a syntactic value, and Bob's your uncle. The packing and unpacking of F is all going to be compiled into the identity function, so oops2 is going to compile into exactly the same machine code as oops.

Things are even nastier when you want a run-time computation to return a polymorphic value like None or []. As hinted at by Nathan Sanders, you can run afoul of the value restriction with an expression as simple as rev []:

Standard ML of New Jersey v110.67 [built: Sun Oct 19 17:18:14 2008]
- val l = rev [];
stdIn:1.5-1.15 Warning: type vars not generalized because of
   value restriction are instantiated to dummy types (X1,X2,...)
val l = [] : ?.X1 list
-  

Nothing higher-order there! And yet the value restriction applies.

In practice the value restriction presents no barrier to the definition and use of higher-order functions; you just eta-expand.

Answer 2

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.