Learning poly variants

1

Hi,

I am learning poly variants and wondering why i am getting an error msg for the code below.
Please help. Thank you.

let red:[> #RED] = #RED
let green:ref<[> #RED]> = ref(red)
green := #GREEN

—Error msg
[E] Line 16, column 4:
This expression’s type contains type variables that can’t be generalized:
ref<_[> #GREEN | #RED]>

  This happens when the type system senses there's a mutation/side-effect,
  in combination with a polymorphic value.
  Using or annotating that value usually solves it.

Thanks & Regards

1 Like
2

Hopefully someone else can confirm, but it seems that mutable bindings can only work with closed polymorphic variants.

For example:

let red: [> #RED] = #RED
let green: ref<[#RED | #GREEN]> = ref(red) // Closed polyvar, so no error
green := #GREEN

Or alternatively, if you use the mutable binding, it also resolves the error.

let red: [> #RED] = #RED
let green: ref<[> #RED]> = ref(red)
green := #GREEN

switch green.contents {
| #RED => Js.log("RED")
| #GREEN => Js.log("GREEN")
}

If you inspect the type of green, you will see that its type has resolved to a closed polyvar ref<[#RED | #GREEN]>

I’m not sure why that’s the case, though.

1 Like
3

This is correct. More generally, type variables in mutable contexts cannot be exported. That would be unsafe because other modules may try to assign inconsistent types to them. You get the same problem with this code:

let good = None // option<'a> is immutable so can be exported.
let bad = ref(None) // ref<option<'a>> is mutable so cannot be exported.

For poly variants, an open type like [> #RED] is itself a type variable. If you defined it with a type name, it would look like this:

type t<'a> = [> #RED] as 'a

Just like with option, the variable 'a cannot be exported in a mutable context.

There are a few ways to fix the code so it can compile:

  • Use a closed polymorphic variant type.
  • Don’t use mutability.
  • Don’t export mutable bindings. (Hide them in the interface, or only define them in a local scope.)

Because you’ve used the value in a context that only supports #RED and #GREEN, the compiler infers that the value can only be those two poly vars (basically “closing” the type). If you tried to assign a different poly var afterwards, e.g. #BLUE, then the compiler will reject it.

4 Likes
4

The answer by @johnj is excellent.

Here’s some additional background for a more general problem:

A language such as rescript want to capture as many errors as possible at compile-time. It turns out that mutable ref-cells pose problems in this space if they use polymorphism in an unconstrained fashion. In particular, you end up with runtime errors, which is a thing we’d like to avoid.

Hence, type systems in the ML family of programming languages restrict the use of polymorphism in ref-cells in certain ways in order to avoid the run-time errors. Rescript is currently in the ML family.

The restriction that’s usually used has to do with an observation about how substitution works together with polymorphism, and it addresses the crux of the problem: that ref-cells enjoy sharing in the program. Surprisingly, it turns out the problem isn’t the side-effect!

Some restrictions might be lifted partially if one finds a better way to handle the problem down the line, without jeopardizing the compile-time soundness. So one can view the restrictions as being conservative. They are safe, but they might reject certain programs which can be handled if the check was written in another way.

It’s another reason why one might not want to make mutability a prominent feature in the language: they need to have constraints imposed upon them for the program to be safe, and if they were used to a larger extent, you would have to reel in the use of polymorphism. Polymorphism turns out to be a very strong tool for programmers.

3 Likes
5

Thanks @johnj, @kevanstannard , and @jlouis . It’s insightful.