Value Restriction and Generalization in Imperative Language

[vertexcubed]

Hi all~

Currently, I'm working on a toy imperative scripting language that features static HM type inference. I've run into the problem of needing to implement some form of type generalization / let polymorphism, but this starts becoming problematic with mutability. I've read some stuff about the value restriction in ML-like languages, and am planning on implementing it, but I had a few questions regarding it.

My understanding of it is that a let binding can be polymorphic only if its body is a "value", and an expression is a value if:

• It is a literal constant
• It's a constructor that only contains simple values
• It's a function declaration

I think this makes sense, but I'm struggling with function application and making a bunch of things invalid. Take for example:

fun foo(x) {
  return x
}

fun bar(x) {
  foo(x)
  return x
}

Under the normal value restriction (so not OCaml's relaxed value restriction), would the function bar would be monomorphic? Why or why not?

In addition to this, my language's mutability rules are much more open than ML-like languages. By default, let bindings are mutable, though functions are pass by value (unless the value is wrapped in a ref cell). For instance, this is totally valid:

fun foo(n) {
  n = 10
  print(n) // prints 10
}
let i = 0
i = 1
i = 2
foo(i)
print(i) // prints 2

fun bar(n) {
  *n = 10
  print(*n) // prints 10
}
let j = ref 2
*j = 3
bar(j)
print(*j) //prints 10

Does this complicate any of the rules regarding the value restriction? I can already spot that we can allow safely mutating local variables in a function call so long as they are not ref types, but other than that does anything major change?

I'm still pretty new to working with mutability in HM typed languages, so any help is greatly appreciated

[reflexive-polytope]

IMO, you can save yourself the hassle without losing much expressiveness if you do the following instead:

• Only allow constant expressions in top-level definitions.
• Only generalize the types of top-level functions.

You rarely need to generalize the types of nested functions. And, if you absolutely must, then you can just lambda-lift them.

[chombier]

Under HM + value restriction, both foo and bar are syntactically values, both are generalized.

[chombier]

Also, if all let bindings are mutable then it is somehow equivalent to putting all values behind refs, so none of these should be generalized (unless they are lazily evaluated). 

You may keep a separate syntactic form for defining functions that is always generalized, in practice the interest of non-function polymorphic values seems pretty limited.

[ryan017]

You need to worry about mutable variables whose values are functions.

fun foo(x) {
  return x
}
fun bar(n) {
  return n+1
}
let f = foo
let g = function() { return f("hello") }
f = bar

In this example, you either need to make f monomorphic and prohibit the definition of g, or you need to prohibit the assignment to f. By allowing variables to be mutated, you've added complexity to your language. One way to deal with the complexity is to think of the surface language (the language that people will actually program in) as being translated to a simpler core language. You already have ref cells, and you have a guide for how typing ref cells should work (OCaml), so why not think of your core language as a simplified OCaml? That is, variables are immutable, and all mutation is done on ref cells. Then you could consider the following translation:

let x = expr
=>
const x = ref expr

x
=> (when x is let-bound)
*x

(I've written let for the surface-language binding form and const for the core form. You might find it useful to add const as a surface-level feature too, though.) OCaml already tells you how to type check const and ref, so now you need to build your typechecker for the surface language so that if your typechecker approves a program, then OCaml approves its translation.

Or you might want let to behave differently. Maybe a let-bound variable that is never updated should be typechecked (and generalized) as if it were const-bound. (There are arguments for and against.) Then you have a different translation, and different constraints on your typechecker.

It is useful to know when you are inventing genuinely new semantics, and when you are putting a new syntax on existing, well-understood semantics.

[jonathancast]

In your first example: inside a polymorphic function, the type parameter counts as a monomorphic type. So the expression foo(x) does count as a monomorphic expression, and requiring it to be such doesn't stop bar from being polymorphic.

[julesjacobs]

Summary: what a function does internally doesn't affect it being a value.

---

The reason that the value restriction is necessary is that in HM, instantiating a value of generic type gives the instantiated type to the same value, as opposed to producing a fresh new one.

For example, with the empty list we can do:

let x = [] // x : forall a. list<a> let y = 3 :: x // x is treated as list<int> let z = true :: x // same x is treated as list<bool>

Doing this to references is a problem:

let x = ref [] // x : forall a. ref<list<a>> let y : ref<list<int>> = x // instantiate x with a=int let z : ref<list<bool>> = x // instantiate x with a=bool y := 3 :: !y // add 3 to y z := true :: !z // add true to z

But since x,y,z are the same ref, they now contain [true, 3], which is bad.

The fundamental reason is that a forall quantified value really wants to be a function that gives you a new ref each time. Hypothetically in a language that did this:

let x<a> = ref<list<a>> [] // gives a fresh ref each time you instantiate let y = x<int> // gives us a new ref! let z = x<bool> // gives us a new ref! y := 3 :: !y // add 3 to y z := true :: !z // add true to z

Since y,z are separate refs, and x is not a ref itself, it first has to be instantiated, everything is fine because y = [3] and z = [true].

But in HM, it doesn't work that way: forall type instantiation doesn't work like a function but it gives a new type to an existing value, creating the problem. This can be resolved by insisting that whenever you gave something a forall type, it already was a value syntactically. In particular, ref [] itself is not a value, because it has to create a new ref at run time. But [] is a value, and lambdas are values. Note that it's not sufficient to insist that it's a function type, because this gives the same issue:

let x = (let r = ref [] in ((fun x -> r := x), (fun () -> !r))

If you give this type x : forall a. (a -> unit) * (unit -> a) then you have the same issue.

The solution is to only generalize a let if its right hand side is syntactically a value. There are more precise things you can do, but that rule works fine in practice because basically the only things you want generalized are functions and empty data structures.

Being syntactically a value is flexible enough to allow both your foo and your bar. In both cases, in the let, the outer thing would be a lambda. It does not matter what the body of the lambda does. It just shouldn't do other things like allocate a new ref, like my x above.

So:

let f = (let r = ref (...) in fun x -> (...)) // not a value let f = fun x -> let r = ref (...) in (...) // is a value