CODEWITHSUNDEEP
ocaml
Jackson Tale
Jackson Tale

Reputation: 25812

Why does a partial application have value restriction?

I can understand that allowing mutable is the reason for value restriction and weakly polymorphism. Basically a mutable ref inside a function may change the type involved and affect the future use of the function. So real polymorphism may not be introduced in case of type mismatch.

For example, 

# let remember =
    let cache = ref None in
    (fun x ->
       match !cache with
       | Some y -> y
       | None -> cache := Some x; x)
  ;;
val remember : '_a -> '_a = <fun>

In remember, cache originally was 'a option, but once it gets called first time let () = remember 1, cache turns to be int option, thus the type becomes limited. Value restriction solves this potential problem.

What I still don't understand is the value restriction on partial application.

For example,

let identity x = x
val identity: 'a -> 'a = <fun>

let map_rep = List.map identity
val map_rep: '_a list -> '_a list = <fun>

in the functions above, I don't see any ref or mutable place, why still value restriction is applied?

Upvotes: 1

Views: 325

Answers (4)

Tarmil
Tarmil

Reputation: 11362

Partial application doesn't preclude mutation. For example, here is a refactored version of your code that would also be incorrect without value restriction:

let aux cache x =
    match !cache with
    | Some y -> y
    | None -> cache := Some x; x

let remember = aux (ref None)

Upvotes: 1

Jeffrey Scofield
Jeffrey Scofield

Reputation: 66818

Here is a good paper that describes OCaml's current handling of the value restriction:

Garrigue, Relaxing the Value Restriction

It has a good capsule summary of the problem and its history.

Here are some observations, for what they're worth. I'm not an expert, just an amateur observer:

  1. The meaning of "value" in the term "value restriction" is highly technical, and isn't directly related to the values manipulated by a particular language. It's a syntactic term; i.e., you can recognize values by just looking at the symbols of the program, without knowing anything about types.

  2. It's not hard at all to produce examples where the value restriction is too restrictive. I.e., where it would be safe to generalize a type when the value restriction forbids it. But attempts to do a better job (to allow more generalization) resulted in rules that were too difficult to remember and follow for mere mortals (such as myself).

  3. The impediment to generalizing exactly when it would be safe to do so is not separate compilation (IMHO) but the halting problem. I.e., it's not possible in theory even if you see all the program text.

Upvotes: 3

seanmcl
seanmcl

Reputation: 9946

A 'let' expression is not a (syntactic) value. While there is a precise definition of 'value', roughly the only values are identifiers, functions, constants, and constructors applied to values.

This paper and those it references explains the problem in detail.

Upvotes: 2

gsg
gsg

Reputation: 9377

The value restriction is pretty simple: only let-bound expressions that are syntactically values are generalized. Applications, including partial applications, are not values and thus are not generalized.

Note that in general it is impossible to tell whether an application is partial, and thus whether the application could have an effect on the value of a reference cell. Of course in this particular case it is obvious that no such thing occurs, but the inference rules are designed to be sound in the event that it does.

Upvotes: 2

Related Questions