Does Scala have a value restriction like ML, if not then why?

Question

Here’s my thoughts on the question. Can anyone confirm, deny, or elaborate?

I wrote:

Scala doesn’t unify covariant List[A] with a GLB ⊤ assigned to List[Int], bcz afaics in subtyping “biunification” the direction of assignment matters. Thus None must have type Option[⊥] (i.e. Option[Nothing]), ditto Nil type List[Nothing] which can’t accept assignment from an Option[Int] or List[Int] respectively. So the value restriction problem originates from directionless unification and global biunification was thought to be undecidable until the recent research linked above.

You may wish to view the context of the above comment.

ML’s value restriction will disallow parametric polymorphism in (formerly thought to be rare but maybe more prevalent) cases where it would otherwise be sound (i.e. type safe) to do so such as especially for partial application of curried functions (which is important in functional programming), because the alternative typing solutions create a stratification between functional and imperative programming as well as break encapsulation of modular abstract types. Haskell has an analogous dual monomorphisation restriction. OCaml has a relaxation of the restriction in some cases. I elaborated about some of these details.

EDIT: my original intuition as expressed in the above quote (that the value restriction may be obviated by subtyping) is incorrect. The answers IMO elucidate the issue(s) well and I’m unable to decide which in the set containing Alexey’s, Andreas’, or mine, should be the selected best answer. IMO they’re all worthy.

Lento

Answer 1

As I explained before, the need for the value restriction -- or something similar -- arises when you combine parametric polymorphism with mutable references (or certain other effects). That is completely independent from whether the language has type inference or not or whether the language also allows subtyping or not. A canonical counter example like

let r : ∀A.Ref(List(A)) = ref [] in
r := ["boo"];
head(!r) + 1

is not affected by the ability to elide the type annotation nor by the ability to add a bound to the quantified type.

Consequently, when you add references to F<: then you need to impose a value restriction to not lose soundness. Similarly, MLsub cannot get rid of the value restriction. Scala enforces a value restriction through its syntax already, since there is no way to even write the definition of a value that would have polymorphic type.

Subshrub

Sorry to be argumentative but Scala’s syntax doesn’t prevent me from writing val r : List[A] = Nil yet rather the type checker complains that “not found: type A”. Yet Scala doesn’t enforce the other value restrictions seen in ML, as observed for example when I successfully compiled in the REPL def id[A](x:A):A = x def f[A](x:A):A = id(id(x)). – Lento

@ShelbyMooreIII, the equivalent thing you cannot write in Scala would be var r[A] : List[A] = Nil. The def form always defines a function, so doesn't need any further restriction. – Subshrub

Studying an example, I now agree the problem doesn’t arise due to lack of subtyping, inference nor annotations, but solely because let binding enables instantiating r (only once) outside the function yet lexically scoped within the function’s parametric polymorphism. Perhaps that’s what you mean by syntactically enabling the combination of “parametric polymorphism with mutable references”? Implying Scala isn’t parametically polymorphic? Scala has mutable references, so which of your criteria doesn’t Scala have? – Lento

@ShelbyMooreIII, Scala has both and it has a syntactic limitation that subsumes the value restriction, see comment above. – Subshrub

If in Scala I place var r : List[A] within the lexical scope of a function parametrised on A, then A is polymorphic w.r.t. to every quantification of that function’s type variables, i.e. every call (aka application) of said function from external lexical scope. I think your intention is that var r : ∀A.List[A] (aka var r[A] : List[A]) would be polymorphic w.r.t. to every application of said function even if applied in an internal lexical scope? So then let binding is an irrelevant detail of implicit closure with memoization? Do I understand correctly now? – Lento

@ShelbyMooreIII, more accurately, the former isn't a polymorphic value, but a monomorphic value in the scope of some surrounding type or type parameter. There is no problem with that, and that's exactly what the value restriction in ML will produce. I don't understand your question about let bindings, but closures and memoization are semantically irrelevant implementation details. – Subshrub

Ty. I know you’re the expert, but afaics it’s as polymorphic as the (type variables of the) function is, and I doubt you’d argue a type parametrised function isn’t parametrically polymorphic. Monomorphic seems an overloaded term (often meaning to specialize the function implementation without changing it’s invariant shape), thus IMO isn’t as descriptive for a layman. You say Scala’s restriction is exactly same, but I already showed an example in my first comment of restriction in MiltonML that doesn’t hold in Scala. I’m interested if anyone knows what’s the tradeoff between the two approaches? – Lento

Oic, the example I provided for Scala is inherently doing the Eta expansion of val id: 'a -> 'a = fn x => x val f: 'a -> 'a = fn z => (id id) z, which also isn’t value restricted in ML. The issue was order-of-evaluation and memoization of id id wherein val f: 'a -> 'a = id id was evaluating one of the id only once when constructing f. So is Scala’s design choice as restrictive as value restriction in ML? Or is it exactly value restriction? – Lento

@ShelbyMooreIII, I said Scala's syntactic limitation subsumes the value restriction, so it is even stronger: in ML I can define let l = [] as a polymorphic value just fine, but I can't in Scala. Monomorphic isn't overloaded at all, it's defined by where the binders/quantifiers for type variables are. Something is polymorphic when it has a quantified type. Unfortunately, ML does not usually make the quantifiers explicit in its syntax, only in its typing rules. – Subshrub

The original source of my confusion (caused significantly by my lack of experience with the syntax+semantics of both of Scala and ML) about no polymorphic values in Scala was because I didn’t discern the unavailability of val r[A] : List[A] = Nil is the same restriction as val f[A] : A -> A = id(id), because I hadn’t realized the implicit Eta expansion equivalence when using def f[A](x:A):A = id(id(x)) instead in Scala. So Scala being more restrictive yet more regular, doesn’t allow either of the aforementioned values, yet ML allows the former in some but not all cases where it’s safe. – Lento

Oic if type parameter A is quantified at the function call site, a val r : List[A] in the function body is monomorphic w.r.t. to the function and the polymorphism of A is only for the function undivided. So the monomorphisation specialization of a function’s typeclass bound(s) at the call site in adhoc polymorphism (and specialization of C++ templates) means the body of the function is monomorphic w.r.t. to the polymorphism. Existentials (aka Rust’s trait objects) bind typeclass bounds on the object (not function) so thus dynamic dispatch (polymorphism) can’t monomorphise the function. – Lento

I presume the vast majority of programmers find these details bewildering, thus I presume we’d need a simplification of concepts to bring such PLs to the mainstream. Scala’s restriction being more regular is K.I.S.S. principled. P.S. I’ve never used ML and only yesterday used a ML repl for the first time (i.e. I was doing it all in my head from reading examples/specs before that). And Scala I’ve mostly only toyed with in a repl on and off over the years. Even I hadn’t updated my C++ experience since 1999. I was coming at this from nearly an entire lack of experience with both Scala and ML. – Lento

Thank you for helping me learn this issue. Fyi, I have completely rewritten my answer to gather the understanding I gained. Perhaps you can check it for errors if you have any time and interest. My problem now is I don’t know which answer to select as the best, and I contrasted the merits of the 3 answers in the opening part of my answers. Cheers. Hopefully our effort can serve as a learning resource for readers. – Lento

Answer 2

It's much simpler than that. In Scala values can't have polymorphic types, only methods can. E.g. if you write

val id = x => x

its type isn't [A] A => A.

And if you take a polymorphic method e.g.

 def id[A](x: A): A = x

and try to assign it to a value

 val id1 = id

again the compiler will try (and in this case fail) to infer a specific A instead of creating a polymorphic value.

So the issue doesn't arise.

EDIT:

If you try to reproduce the http://mlton.org/ValueRestriction#_alternatives_to_the_value_restriction example in Scala, the problem you run into isn't the lack of let: val corresponds to it perfectly well. But you'd need something like

val f[A]: A => A = {
  var r: Option[A] = None
  { x => ... }
}

which is illegal. If you write def f[A]: A => A = ... it's legal but creates a new r on each call. In ML terms it would be like

val f: unit -> ('a -> 'a) =
    fn () =>
       let
          val r: 'a option ref = ref NONE
       in
          fn x =>
          let
             val y = !r
             val () = r := SOME x
          in
             case y of
                NONE => x
              | SOME y => y
          end
       end

val _ = f () 13
val _ = f () "foo"

which is allowed by the value restriction.

That is, Scala's rules are equivalent to only allowing lambdas as polymorphic values in ML instead of everything value restriction allows.

Subgenus

1. "but doesn’t explicitly state that values are restricted" It's under "3.3 Non-value types" 2. "i.e. A subtype of ⊥ and supertype of ⊤" is exactly the opposite 3. [A >: Nothing <: Any] is not the inferred type, it's part of it, just like Int => is not a type. – Subgenus

Also, there are versions of ML with subtyping, e.g. lambda-the-ultimate.org/node/5393. It doesn't affect polymorphic values: "Since the typing rules for MLsub are just those of ML with an extra (SUB) rule, any expression typeable in ML is trivially typeable in MLsub with the same type." – Subgenus

Where you wrote “is exactly the opposite”, you were pointing out a typo where I transposed ⊥ and ⊤. But that correction doesn’t obviate my claim “can’t be populated”. When I replied before, I thought you might have been referring to the type List[A] having opposite covariance restrictions direction from A. Just noticed the typo. Thanks. Yet I’ve explained above combined with my answer there’s no way to construct a value with a type of List[A] such that the type of A is [A >: Nothing <: Any]. As you implied, that type is only meaningful in the context of the function. – Lento

"ML type 'a list ref isn’t a type of a polymorphic value 'a" and "the type of A is [A >: Nothing <: Any]" seem to be category errors to me: not even wrong. 'a and A are type variables, not expressions, they don't have types. – Subgenus

'a list is a type (scheme) of a polymorphic value [], though. – Subgenus

I've added an explanation how that example would work in Scala and more direct comparison between Scala's "no polymorphic values" restriction and the value restriction. – Subgenus

Your added example of a new instance of reference r created for each quantification of the type variable A, obviates the type safety issue in both Scala & ML. ML’s feature (unavailable in Scala) declares a reference type which as (re-)quantified by its lexical scope even due to re-applications from inside said scope, doesn’t create new instances if evaluation order of r’s construction is outside the said reapplication via for example the let binding. – Lento

I’ve deleted my noisy comments but they’re archived. Your explanation confused me. Andreas finally made it clear to me when he differentiated val r[A] : List[A] (aka ∀A.List[A]) from val r : List[A] thus emphasizing the quantification of the lexical scope. Now I’m trying to understand what advantages and disadvantages ML has with that feature, and the respective tradeoffs for Scala not having it? Can you elaborate? – Lento

The original source of my confusion (caused significantly by my lack of experience with the syntax+semantics of both of Scala and ML) about no polymorphic values in Scala was because I didn’t discern the unavailability of val r[A] : List[A] = Nil is the same restriction as val f[A] : A -> A = id(id), because I hadn’t realized the implicit Eta expansion equivalence when using def f[A](x:A):A = id(id(x)) instead in Scala. So Scala being more restrictive yet more regular, doesn’t allow either of the aforementioned values, yet ML allows the former in some but not all cases where it’s safe. – Lento

Thank you for helping me learn this issue. Fyi, I have completely rewritten my answer to gather the understanding I gained. Perhaps you can check it for errors if you have any time and interest. My problem now is I don’t know which answer to select as the best, and I contrasted the merits of the 3 answers in the opening part of my answers. Cheers. Hopefully our effort can serve as a learning resource for readers. – Lento

Answer 3

EDIT: this answer was incorrect before. I have completely rewritten the explanation below to gather my new understanding from the comments under the answers by Andreas and Alexey.

_{The edit history and the history of archives of this page at archive.is provides a recording of my prior misunderstanding and discussion. Another reason I chose to edit rather than delete and write a new answer, is to retain the comments on this answer. IMO, this answer is still needed because although Alexey answers the thread title correctly and most succinctly—also Andreas’ elaboration was the most helpful for me to gain understanding—yet I think the layman reader may require a different, more holistic (yet hopefully still generative essence) explanation in order to quickly gain some depth of understanding of the issue. Also I think the other answers obscure how convoluted a holistic explanation is, and I want naive readers to have the option to taste it. The prior elucidations I’ve found don’t state all the details in English language and instead (as mathematicians tend to do for efficiency) rely on the reader to discern the details from the nuances of the symbolic programming language examples and prerequisite domain knowledge (e.g. background facts about programming language design).}

---

The value restriction arises where we have mutation of referenced¹ type parametrised objects². The type unsafety that would result without the value restriction is demonstrated in the following MLton code example:

val r: 'a option ref = ref NONE
val r1: string option ref = r
val r2: int option ref = r
val () = r1 := SOME "foo"
val v: int = valOf (!r2)

The NONE value (which is akin to null) contained in the object referenced by r can be assigned to a reference with any concrete type for the type parameter 'a because r has a polymorphic type a'. That would allow type unsafety because as shown in the example above, the same object referenced by r which has been assigned to both string option ref and int option ref can be written (i.e. mutated) with a string value via the r1 reference and then read as an int value via the r2 reference. The value restriction generates a compiler error for the above example.

A typing complication arises to prevent³ the (re-)quantification (i.e. binding or determination) of the type parameter (aka type variable) of a said reference (and the object it points to) to a type which differs when reusing an instance of said reference that was previously quantified with a different type.

Such (arguably bewildering and convoluted) cases arise for example where successive function applications (aka calls) reuse the same instance of such a reference. IOW, cases where the type parameters (pertaining to the object) for a reference are (re-)quantified each time the function is applied, yet the same instance of the reference (and the object it points to) being reused for each subsequent application (and quantification) of the function.

Tangentially, the occurrence of these is sometimes non-intuitive due to lack of explicit universal quantifier ∀ (since the implicit rank-1 prenex lexical scope quantification can be dislodged from lexical evaluation order by constructions such as let or coroutines) and the arguably greater irregularity (as compared to Scala) of when unsafe cases may arise in ML’s value restriction:

Andreas wrote:

Unfortunately, ML does not usually make the quantifiers explicit in its syntax, only in its typing rules.

Reusing a referenced object is for example desired for let expressions which analogous to math notation, should only create and evaluate the instantiation of the substitutions once even though they may be lexically substituted more than once within the in clause. So for example, if the function application is evaluated as (regardless of whether also lexically or not) within the in clause whilst the type parameters of substitutions are re-quantified for each application (because the instantiation of the substitutions are only lexically within the function application), then type safety can be lost if the applications aren’t all forced to quantify the offending type parameters only once (i.e. disallow the offending type parameter to be polymorphic).

The value restriction is ML’s compromise to prevent all unsafe cases while also preventing some (formerly thought to be rare) safe cases, so as to simplify the type system. The value restriction is considered a better compromise, because the early (antiquated?) experience with more complicated typing approaches that didn’t restrict any or as many safe cases, caused a bifurcation between imperative and pure functional (aka applicative) programming and leaked some of the encapsulation of abstract types in ML functor modules. I cited some sources and elaborated here. Tangentially though, I’m pondering whether the early argument against bifurcation really stands up against the fact that value restriction isn’t required at all for call-by-name (e.g. Haskell-esque lazy evaluation when also memoized by need) because conceptually partial applications don’t form closures on already evaluated state; and call-by-name is required for modular compositional reasoning and when combined with purity then modular (category theory and equational reasoning) control and composition of effects. The monomorphisation restriction argument against call-by-name is really about forcing type annotations, yet being explicit when optimal memoization (aka sharing) is required is arguably less onerous given said annotation is needed for modularity and readability any way. Call-by-value is a fine tooth comb level of control, so where we need that low-level control then perhaps we should accept the value restriction, because the rare cases that more complex typing would allow would be less useful in the imperative versus applicative setting. However, I don’t know if the two can be stratified/segregated in the same programming language in smooth/elegant manner. Algebraic effects can be implemented in a CBV language such as ML and they may obviate the value restriction. IOW, if the value restriction is impinging on your code, possibly it’s because your programming language and libraries lack a suitable metamodel for handling effects.

Scala makes a syntactical restriction against all such references, which is a compromise that restricts for example the same and even more cases (that would be safe if not restricted) than ML’s value restriction, but is more regular in the sense that we’ll not be scratching our head about an error message pertaining to the value restriction. In Scala, we’re never allowed to create such a reference. Thus in Scala, we can only express cases where a new instance of a reference is created when it’s type parameters are quantified. Note OCaml relaxes the value restriction in some cases.

Note afaik both Scala and ML don’t enable declaring that a reference is immutable¹, although the object they point to can be declared immutable with val. Note there’s no need for the restriction for references that can’t be mutated.

The reason that mutability of the reference type¹ is required in order to make the complicated typing cases arise, is because if we instantiate the reference (e.g. in for example the substitutions clause of let) with a non-parametrised object (i.e. not None or Nil⁴ but instead for example a Option[String] or List[Int]), then the reference won’t have a polymorphic type (pertaining to the object it points to) and thus the re-quantification issue never arises. So the problematic cases are due to instantiation with a polymorphic object then subsequently assigning a newly quantified object (i.e. mutating the reference type) in a re-quantified context followed by dereferencing (reading) from the (object pointed to by) reference in a subsequent re-quantified context. As aforementioned, when the re-quantified type parameters conflict, the typing complication arises and unsafe cases must be prevented/restricted.

Phew! If you understood that without reviewing linked examples, I’m impressed.

---

¹ _{IMO to instead employ the phrase “mutable references” instead of “mutability of the referenced object” and “mutability of the reference type” would be more potentially confusing, because our intention is to mutate the object’s value (and its type) which is referenced by the pointer— not referring to mutability of the pointer of what the reference points to. Some programming languages don’t even explicitly distinguish when they’re disallowing in the case of primitive types a choice of mutating the reference or the object they point to.}

² _{Wherein an object may even be a function, in a programming language that allows first-class functions.}

³ _{To prevent a segmentation fault at runtime due to accessing (read or write of) the referenced object with a presumption about its statically (i.e. at compile-time) determined type which is not the type that the object actually has.}

⁴ _{Which are NONE and [] respectively in ML.}

Lento

@AluanHaddad providing an ML-like value restriction is not a desirable feature. Value restriction is an undesirable restriction. So ‘provide’ isn’t the correct verb. I appreciate your comment because I probably should have clarified what ML’s value restriction is and that it’s an undesirable restriction of the language. Maybe I will edit the question. Also I didn’t know much about value restriction until recently also, and I may still be ignorant. :-) – Lento

Shows how much I know... So that is the thing that confounds my F# programs! Thank you for that. I learned something interesting. – Cytosine

@AluanHaddad, I added a summary about value restriction to the question. – Lento

Excellent, reading :) interesting discussion on GitHub as well. Some of it's pretty over my head but you made a lot of good points about closures. Personally I think they're the most effective form of encapsulation – Cytosine

Possibility exists for many mistakes and oversights. Expert review welcomed. I’m not the expert, more like the instigator or agitator. :-) Cheers. – Lento

Several languages have recently received proposals that would make closures less syntactically convenient. For example, capture lists proposed for C# and Spores proposed for Scala. I think they miss the mark because, if a function has a nonempty closure environment, that's because the logic needs to reference that environment. Making it syntactically more difficult doesn't help because you would need to rewrite your function to one with different semantics anyway because if you captured something it was because you used it. – Cytosine

@AluanHaddad I completely rewrote my answer because it was incorrect. If you have any time and interest, I’m interested to know if this new explanation helps you to more deeply wrap your mind around the value restriction issue? I find that explaining the issue holistically is quite abstruse no matter how I distill it. – Lento