> While an element of type bool is an instance of type a, an element of type bool -> bool is not an instance of type a -> a.
This sentence is true if you interpret `a -> a` to mean `∀ a. a -> a`, i.e. a universally-quantified type. But it is false if you interpret it to mean `α -> α` where α is an unsolved metavariable, for the reasons I describe in this comment: https://news.ycombinator.com/item?id=31238081
> The issue is precisely an issue of variance, which is mentioned in reference to Scala, but somehow it's glossed over.
Not so! The issue is the incompatibility of mutable references and value polymorphism, which variance alone does not solve. For example, in Scala, you cannot write something like
val xs[A]: ArrayBuffer[A] = ArrayBuffer[A]()
because if you could do that, then you could write
val bools: ArrayBuffer[Bool] = xs[Bool]
bools += true
val ints: ArrayBuffer[Int] = xs[Int]
ints.last
and all hell breaks loose. Note that variance does not in any way save you here—the type variable `A` is always covariant, so this code is variance-correct. Scala prevents this by only permitting polymorphic
functions, so you would have to write the above example like this, instead:
def xs[A](): ArrayBuffer[A] = ArrayBuffer[A]()
Now everything is okay, because if you call this function twice, you get two different buffers. This is precisely what the ML value restriction enforces.
> Another name for contravariance is "generalization".
Maybe this is true in some sense of the word, though I’ll admit I’ve never seen “generalization” used in this way. But in Hindley-Milner type systems, “generalization” is a term of art that means something fairly specific, namely the implicit introduction of universal quantification, so using it in this context to mean something else may be a little confusing.
> If SML accepted something of type "bool -> bool" for an instance of type "a -> a", then it was a fundamental error. But this doesn't mean that the whole thing should have been thrown out and replaced with monads. In fact, I don't really get how monads have anything to do with the problem at hand.
I sort of agree—introducing monadic structure has essentially nothing fundamental to do with this particular problem. However, it is incidentally true that the monadic encoding of mutable state in Haskell sidesteps the problem. To see why, suppose we translate the Scala example from above into Haskell. Suppose we have a constructor like this:
newArrayBuffer :: forall a. IO (ArrayBuffer a)
Note that this is itself a polymorphic value—it isn’t a function! But since it’s wrapped in `IO`, it isn’t itself a polymorphic buffer, just a recipe to create one. If we wanted to trigger the bad behavior, we’d need to be able to create a definition with a type like this:
xs :: forall a. ArrayBuffer a
But that isn’t possible to obtain from `newArrayBuffer`, even though Haskell allows polymorphic values. That’s because, in the type of `newArrayBuffer`, the `forall` is outside the `IO` constructor, so in order to actually use it in a computation using `>>=`, we have to instantiate `a` to some concrete type. In other words, `IO` plays precisely the same role here that a nullary function does in Scala: it ensures each instantiation is
generative, i.e. it returns a distinct buffer.
So Haskell doesn’t need a value restriction because, in a sense, everything impure is subject to a value restriction, with `IO` playing the role of the nullary function type, and that includes anything that contains mutable state. But since Haskell relies on this property of `IO` to preserve safety `unsafePerformIO` can subvert the type system. We can write
xs :: forall a. ArrayBuffer a
xs = unsafePerformIO (newArrayBuffer @a)
and we get the potential for badness again, just like in the Scala example. This is considered acceptable because `unsafePerformIO` is, well, unsafe.