What was wrong with SML?

You really can simulate laziness in a strict language at the small cost of wrapping things in lambdas yourself -- you don't have to figure out what operations you can do yourself so long as you make everything that should be deferred deferrable (for example, if you're trying to do monadic fixedpoints you need to be careful). If you create your own lazy data structures, if your language supports it you can even have those thunks be forced for you automatically. For example, lazy streams (infinite lists) in Python with memoized thunks:

    class Thunk:
        def __init__(self, f):
            self.evaluated = False
            self.val = f
        def __call__(self):
            if not self.evaluated:
                self.val = self.val()
                self.evaluated = True
            return self.val

    class Cons:
        def __init__(self, x, xs):
            assert isinstance(xs, Thunk)
            self.head = x
            self._tail = xs
        @property
        def tail(self):
            return self._tail()
        def nth(self, n):
            for _ in range(n):
                self = self.tail
            return self.head

    ones = Cons(1, Thunk(lambda: ones))

    print([ones.nth(i) for i in range(10)])
    # [1, 1, 1, 1, 1, 1, 1, 1, 1, 1]

    def lazy_map(xs, f):
        return Cons(f(xs.head), Thunk(lambda: lazy_map(xs.tail, f)))

    nats = Cons(0, Thunk(lambda: lazy_map(nats, lambda x: x + 1)))

    print([nats.nth(i) for i in range(10)])
    # [0, 1, 2, 3, 4, 5, 6, 7, 8, 9]

    def lazy_zip(xs, ys, f):
        return Cons(f(xs.head, ys.head), Thunk(lambda: lazy_zip(xs.tail, ys.tail, f)))

    fibs = Cons(0, Thunk(lambda: Cons(1, Thunk(lambda: lazy_zip(fibs, fibs.tail, lambda x, y: x + y)))))

    print([fibs.nth(i) for i in range(10)])
    # [0, 1, 1, 2, 3, 5, 8, 13, 21, 34]

I think laziness is pretty cool, but it does mix up two notions that turn out to be individually important: data and codata. Mixing them together makes a language's type system logically inconsistent, in the sense that you can't use Curry-Howard isomorphism anymore (nonempty types true propositions). Data is, essentially, anything you can do structural recursion on and evaluate in finite time, no matter the evaluation strategy. Codata is fuzzier to me, but the canonical example of codata is the lambda abstraction. Haskell smears a layer of codata over all its algebraic datatypes (data) to make everything lazy.

I once took advantage of this in a light way when designing a compiler targeting C in Haskell, with a goal of making beautiful-ish C code. The language, unlike C, was expression-based, so everything could evaluate to a value. The step that lowered expressions into C syntax returned a struct with multiple fields, each giving a piece of C syntax depending on how the expression was going to be used in context -- was the value of the expression going to be used? or just its side-effect? Then, due to laziness, only one of the fields of the struct would actually be evaluated. (It also handled other cases: lvalues and whether the expression's value was going to be immediately stored somewhere, since then the expression could use that location directly rather than creating a temporary variable if it might have needed one.)

> For example, if Int8 = -10 and UInt16 = 5, and I’m expecting an answer of -5, then I’ll need to be more explicit to get the number I’m looking for. If I’m expecting [65531], then the implicit promotion works fine.

That depends on what you're hoping to do with the number you're looking for. If you wanted -5 as an Int16, the bit pattern would be 1111 1111 1111 1011 or 0xFFFB.

If you wanted 65531 as a UInt16, the bit pattern for that is 1111 1111 1111 1011 or 0xFFFB. You're getting the same result either way. And any values you compute from that result [that is, by arithmetic] are going to be unaffected by whether you labeled the result "Int16" or "UInt16", because that's just a label. If you labeled 0xFFFB a "Snerf", the arithmetic would still be the same.

There are only a very restricted set of places where you need to be explicit about whether you think of your variable as an Int or a UInt:

1. When you're widening it.

2. When you're doing a right shift.

3. When you're formatting it for display to a human.

Interestingly we used OCaml in the first semester (by the professor's choice) in late 2003, and I hated it and failed the course. A year later I retook the course and as it was some other professor's turn it was SML, which I kinda liked. I did revisit OCaml more than 10 years later and actually enjoyed it, so maybe it was a bit of "wrong place, wrong time" but as I heard from some users it should have evolved quite a bit in those 10 years. (I am 95% sure it was not functional programming per se, but I never figured out what exactly was the culprit, I guess a dose of "I know how to code" was involved).

All these explanations seem somewhat confused to me because they don’t pin down what the variables represent. In a traditional formulation of Hindley-Milner, there are two distinct notions of a “variable”: (1) a bound variable under a quantifier, or (2) a metavariable, also known as a unification variable, introduced by the type inference algorithm.

Bound variables are variables that either the programmer wrote explicitly in their program or variables introduced by generalization. They appear underneath a quantifier, as in the type

    ∀ a. a -> a

which makes the quantification explicit. However, both SML and Haskell make the placement of quantifiers implicit by default, which is somewhat syntactically convenient, but it obscures this distinction.

In HM, a bound variable only unifies with itself, so if we use `~` to mean “unifies with”, then `a ~ a` holds but neither `a ~ Bool` nor `a ~ b` do, assuming `a` and `b` are bound variables. However, bound variables do not actually get involved in typechecking unless the programmer wrote them in their program explicitly, because when a polymorphic binding is used, the typechecker instantiates it, replacing bound variables with metavariables.

There is no way for the programmer to write metavariables in their types, because metavariables are, as their name suggests, a metalanguage concept introduced by the typechecking machinery, not a part of the underlying language of types. This makes writing them down in a way that clearly distinguishes them from bound type variables somewhat difficult, so I will adopt the convention of using Greek letters to represent metavariables. This means we can instantiate the above type to get

    α -> α

which is a very different type! In particular, while bound variables only unify with themselves, metavariables unify with anything so `α ~ α`, `α ~ Bool`, `α ~ a`, and `α ~ β` all hold. However, a metavariable can only unify with something other than itself once, because the process of unification effectively mutates the typechecking context by globally replacing the metavariable with the type it unified with. That is, if typechecking requires the unification `α ~ Bool`, then our function type `α -> α` becomes `Bool -> Bool`, since we perform the unification by globally replacing α with Bool.

All of this stuff might seem a bit fiddly, since we’re explaining metavariables in terms of internal details of a typechecking algorithm. But indeed, that’s the point: metavariables are an invention of the typechecking algorithm, a mechanism used to implement type inference. They aren’t really types, they’re “holes” in types that have yet to be filled in by the type inference process. So when you ask a question like “is `Bool -> Bool` a subtype of `α -> α`”, your question is somewhat meaningless, as it depends on what α means for whatever typechecking algorithm you’re discussing, and pure HM does not really have any notion of subtyping (just instantiation and unification).

If we introduce more sophisticated type systems that do have subtyping, then we have the machinery to talk about things like covariance and contravariance. But in HM, no such relation exists, so any notions of subtyping, covariance, and contravariance exist only in our heads, not in the type system itself. Still, we can informally establish a notion of subtyping by saying that if S is a subtype of T, written `S

    (∀ a. a -> a)  Bool)

holds. The answer is certainly yes, as we can always instantiate the former to get the latter (which is what you refer to as specialization). But that quantifier is crucial, because it’s what allows us to do the instantiation! If we just have

    (a -> a)  Bool)

then the relation no longer holds, as `a` is a bound variable that is only a subtype of itself, and we no longer have the freedom to instantiate it. So when reasoning about types involving variables, it’s wise to keep the quantifiers explicit, otherwise you may come to the wrong conclusions.

> 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.