What is the motivation for OCaml to choose “value restriction” over “polymorphism by name” (call by name)?
From my personal view, polymorphism by name does not bring in new rules like 'a to the type system.
And it seems simpler to me.
Reference:
Xavier Leroy, 1993. Polymorphism by name for references and continuations. In 20th symposium Principles of Programming Languages, pages 220-231. ACM Press, 1993.
The value restriction isn’t that onerous, and OCaml improves on it by using a relaxed restriction. The relaxed value restriction addresses some of the concerns about programming with references that are brought up in the linked paper.
Implicit duplication of side effecting computations is a nasty problem to introduce for the little benefit gained. I’m not surprised that the (relaxed) value restriction was considered preferable.
OCaml improves on it by using a relaxed restriction
From a view point of history, relaxed restriction is introduced in a later
time.
And it may not related to the decision of choosing value restriction over
polymorphism by name.
From a view point of now, relaxed restriction loosen the restriction for
some conditions.
It does be an improvement, but not a fundamentally different thing compared
to value restriction.
Implicit duplication of side effecting computations
What do you mean by “implicit”?
In the polymorphism by name paper,
call by name and call by value is clearly distinguished in syntax,
just like laziness and strictness in OCaml.
The definitions look different, but at the use sites of a polymorphic variable there are potential side effects without any syntactic indication, that is, implicitly. Note that Lazy is not quite like this as in order to force a lazy value you have to either call Lazy.force or match on a lazy pattern.
And it may not related to the decision of choosing value restriction over polymorphism by name. From a view point of now, relaxed restriction loosen the restriction for
some conditions.
It seems to me that the OCaml designers started with a standard approach (the value restriction), but were unhappy with the way it worked with references. They experimented with various improvements, including polymorphism-by-name, and eventually settled on the relaxed value restriction. In this sense the two ideas are competitors whether polymorphism-by-name came first or not.
Issues related to the relaxed value restriction has become relevant again after the introduction of GADTs, since these don’t admit positive variance, as required by the relaxation. The way forward may be to restore variance checking; even failing that a new pseudo-variance could indicate that the type is merely state-free for that parameter. Though, inspired by that paper one could consider a somewhat more esoteric but imperative-friendly option:
The by-name binding in the paper induce an evaluation per occurrence. It seems sufficient to evaluate the let-term at each type in order to guarantee safety. Such a “by-type” semantic would generalise the by-value semantic, admitting the same type generalisation as by-name. Though, since it does not generalise the relaxed value restriction it should be a separate let-construct if added to OCaml.
E.g., without suggesting this specific syntax
let [_] get_cell, set_cell, clear_cell =
let r = ref None in
((fun () -> !r), (fun x -> r := Some x), (fun x -> r := None))
val ['a] get_cell : (unit -> 'a option)
val ['a] set_cell : ('a -> unit)
val ['a] clear_cell : (unit -> unit)
would create a reference per instance of 'a.
This would have a performance penalty linear in the number of type instances instead of linear in the number of calls. There would be challenges to the implementation though. A run-time representation of types seems necessary in order to memoise the state at each used type. Since types can be generated at run time, at least due to first-order modules, there are potential space leaks and instances which cannot be identified for initialization at compile-time.
Without being familiar with its implementation, I’d imagine this might trespass into modular-implicits territory due to the instance-creation and implied type argument.