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 universa

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