4 ms·

I'm not really convinced by the author's first example. While an element of type bool is an instance of type a, an element of type bool -> bool is not an instan

I'm not really convinced by the author's first example. 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. The issue is precisely an issue of variance, which is mentioned in reference to Scala, but somehow it's glossed over. The type a -> a is covariant in its second argument, but contravariant in its first argument. As a result, you cannot "specialize" it to bool -> bool, because specialization is really another name for covariance. Another name for contravariance is "generalization". If you ask for something of type "bool -> b", and someone provides you with some function f of type "a -> b", then you're happy. The map f is indeed an instance of "bool -> b": it can eat anything, so it can eat booleans. But with type a -> a, you cannot do what I just did: type "a" is already the most general one, and you cannot do better. 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. If Haskell can prevent the following code, then I don't see why SML couldn't have prevented the authors' code: do m <- STRef id m <- not m 42

lexi-lambda 4y ago
> 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 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.
- kragen 4y ago
  Thank you!
_delirium 4y ago
This is pretty fundamental to the Hindley-Milner system of parametric polymorphism (which I believe was the first such system?). The 'a is treated as a universally quantified type variable that can be unified with concrete types [1]. 'a=int and 'a=bool are two possible ways to unify the type variable, yielding int->int and bool->bool as signatures that unify with 'a->'a. Similarly 'a list -> 'a means a function that takes a list of some type, and returns an element of the same type (the built-in List.hd function is an example), while 'a list -> 'b is a looser type signature meaning "takes a list of some type, and returns some value, not necessarily of the same type", so int list -> int and int list -> bool would both fit the 2nd schema. This is all sound if the language is pure, which ML originally was. There's also a relevant discussion at Stackoverflow. [2] [1] This is a fairly concise summary of the quantification rules: https://jgbm.github.io/eecs662f17/Notes-on-HM.html https://jgbm.github.io/eecs662f17/Notes-on-HM.html [2] "Does Scala have a value restriction like ML, if not then why?" https://stackoverflow.com/questions/48594769/does-scala-have-a-value-restriction-like-ml-if-not-then-why https://stackoverflow.com/questions/48594769/does-scala-have...
CoderPuppy 4y ago
SML doesn't have subtyping or variance AFAIK so that can't really explain the issue. The way I like to look at it is to translate to System F. The standard translation would give: let m : ∀α. ref (α → α) = Λα. ref [α → α] (λx. x) in (m [bool]) := not; print ((!(m [int])) 23) end This actually has different behavior because the ref allocation is under a big lambda (Λ). Each time it is applied it would generate a new ref cell. So it would generate a `ref (bool → bool)` starting with `λx. x` and assign `not` to it. Then generate a separate `ref (int → int)` (again starting with `λx. x`) and dereference and apply it. Thus this would print `23`. (The naive model of) SML runs into problems because it erases the big lambdas and so evaluates `Λα. ref [α → α] (λx. x)` to a single ref cell of type `∀α. ref (α → α)` Sidenote: Variance does have some relation here, I couldn't think of a way to trigger bad behavior without a type that uses the type variable invariantly.
jasonhansel 4y ago
The point AFAICT isn't that the type checker sees "bool -> bool" as an instance of "a -> a". Instead, the issue is that during type inference, when the compiler sees "m := not", it will infer that a == bool, i.e. that "m = ref (fn x ⇒ x)" was really "m = ref (fn (x:bool) ⇒ x)". But then it will forget that inference when type checking "print ((!m) 23)"; there it will infer that a == int, and that the original definition of m was really "m = ref (fn (x:int) ⇒ x)". Essentially the issue is that type inference forgets that it already solved for "a" and can't assign it to both "int" and "bool".
kragen 4y ago
As I explained in https://news.ycombinator.com/item?id=31222098 https://news.ycombinator.com/item?id=31222098, I don't think this explanation is correct. You're right that bool → bool is not a subtype of α → α, and that function types are contravariant on their argument type. But because function types are not also covariant on their return type, the same logic would tell us that α → α is neither a subtype of bool → bool nor a supertype. In fact, though, α → α is a subtype of bool → bool, for reasons that have nothing to do with covariance and contravariance. We can define a function whose argument is of type bool → bool; here in OCaml: # let abool f = not (f true) ;; val abool : (bool -> bool) -> bool = <fun> And we can define a function of type α → α: # let f = fun x -> x ;; val f : 'a -> 'a = <fun> And that function is perfectly acceptable as the argument to abool, or indeed in any other context where we need a function of type bool → bool: # abool f ;; - : bool = false Thus α → α is a subtype of bool → bool, and also int → int, string → string, etc. And this is not because the value restriction has been sneakily applied behind our backs; f and abool still have their original types: # abool ;; - : (bool -> bool) -> bool = <fun> # f ;; - : 'a -> 'a = <fun> And we can still apply abool to a function that's unashamedly bool → bool: # abool (fun x -> not (not x)) ;; - : bool = false # not ;; - : bool -> bool = <fun> # abool not ;; - : bool = true So specialization is not another name for covariance, and you absolutely can specialize α → α to bool → bool.
- kragen 4y ago
  I wrote, "But because function types are not also covariant on their return type," but that should have been, "But because function types are also covariant on their return type."
- lexi-lambda 4y ago
  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 <: T`, then an expression of type S can be used wherever an expression of type T is expected. Given that, we can ask whether (∀ a. a -> a) <: (Bool -> 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 -> 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.

lexi-lambda 4y ago

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

kragen 4y ago
Thank you!

_delirium 4y ago

This is pretty fundamental to the Hindley-Milner system of parametric polymorphism (which I believe was the first such system?). The 'a is treated as a universally quantified type variable that can be unified with concrete types [1]. 'a=int and 'a=bool are two possible ways to unify the type variable, yielding int->int and bool->bool as signatures that unify with 'a->'a. Similarly 'a list -> 'a means a function that takes a list of some type, and returns an element of the same type (the built-in List.hd function is an example), while 'a list -> 'b is a looser type signature meaning "takes a list of some type, and returns some value, not necessarily of the same type", so int list -> int and int list -> bool would both fit the 2nd schema. This is all sound if the language is pure, which ML originally was. There's also a relevant discussion at Stackoverflow. [2] [1] This is a fairly concise summary of the quantification rules: https://jgbm.github.io/eecs662f17/Notes-on-HM.html https://jgbm.github.io/eecs662f17/Notes-on-HM.html [2] "Does Scala have a value restriction like ML, if not then why?" https://stackoverflow.com/questions/48594769/does-scala-have-a-value-restriction-like-ml-if-not-then-why https://stackoverflow.com/questions/48594769/does-scala-have...

CoderPuppy 4y ago

SML doesn't have subtyping or variance AFAIK so that can't really explain the issue. The way I like to look at it is to translate to System F. The standard translation would give: let m : ∀α. ref (α → α) = Λα. ref [α → α] (λx. x) in (m [bool]) := not; print ((!(m [int])) 23) end This actually has different behavior because the ref allocation is under a big lambda (Λ). Each time it is applied it would generate a new ref cell. So it would generate a `ref (bool → bool)` starting with `λx. x` and assign `not` to it. Then generate a separate `ref (int → int)` (again starting with `λx. x`) and dereference and apply it. Thus this would print `23`. (The naive model of) SML runs into problems because it erases the big lambdas and so evaluates `Λα. ref [α → α] (λx. x)` to a single ref cell of type `∀α. ref (α → α)` Sidenote: Variance does have some relation here, I couldn't think of a way to trigger bad behavior without a type that uses the type variable invariantly.

jasonhansel 4y ago

The point AFAICT isn't that the type checker sees "bool -> bool" as an instance of "a -> a". Instead, the issue is that during type inference, when the compiler sees "m := not", it will infer that a == bool, i.e. that "m = ref (fn x ⇒ x)" was really "m = ref (fn (x:bool) ⇒ x)". But then it will forget that inference when type checking "print ((!m) 23)"; there it will infer that a == int, and that the original definition of m was really "m = ref (fn (x:int) ⇒ x)". Essentially the issue is that type inference forgets that it already solved for "a" and can't assign it to both "int" and "bool".

kragen 4y ago

As I explained in https://news.ycombinator.com/item?id=31222098 https://news.ycombinator.com/item?id=31222098, I don't think this explanation is correct. You're right that bool → bool is not a subtype of α → α, and that function types are contravariant on their argument type. But because function types are not also covariant on their return type, the same logic would tell us that α → α is neither a subtype of bool → bool nor a supertype. In fact, though, α → α is a subtype of bool → bool, for reasons that have nothing to do with covariance and contravariance. We can define a function whose argument is of type bool → bool; here in OCaml: # let abool f = not (f true) ;; val abool : (bool -> bool) -> bool = <fun> And we can define a function of type α → α: # let f = fun x -> x ;; val f : 'a -> 'a = <fun> And that function is perfectly acceptable as the argument to abool, or indeed in any other context where we need a function of type bool → bool: # abool f ;; - : bool = false Thus α → α is a subtype of bool → bool, and also int → int, string → string, etc. And this is not because the value restriction has been sneakily applied behind our backs; f and abool still have their original types: # abool ;; - : (bool -> bool) -> bool = <fun> # f ;; - : 'a -> 'a = <fun> And we can still apply abool to a function that's unashamedly bool → bool: # abool (fun x -> not (not x)) ;; - : bool = false # not ;; - : bool -> bool = <fun> # abool not ;; - : bool = true So specialization is not another name for covariance, and you absolutely can specialize α → α to bool → bool.

kragen 4y ago
I wrote, "But because function types are not also covariant on their return type," but that should have been, "But because function types are also covariant on their return type."
lexi-lambda 4y ago
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 <: T`, then an expression of type S can be used wherever an expression of type T is expected. Given that, we can ask whether (∀ a. a -> a) <: (Bool -> 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 -> 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.