Mono- vs. polymorphic let

In the lecture, we covered type inference for generic polymorphism in a typed calculus with higher-order functions, including recursive functions and let-bindings. That was good enough to show the central role of unification for such kind of type inference. I mentioned, however, that the presented version is not the famous ML-type inference (or Hindley-Milner-Damas system). Not because of this or that feature missing (like: are tuples covered, yes or no), or notational or presentational differences. Our system is simpler in a significant way: we left out polymorphic lets and worked with monomorphic lets instead. Here I sketch what would be needed repair that shortcoming i.e., I try to sketch what additional “features” the Hindley-Milner-Damas system has, without going into all details or showing the system itself. One can find many presentations (in textbooks, on the internet etc.).

What does monomorphic resp. polymorphic let mean?

We clarified in the lecture the notions of monomorphism and polymorphism (for type systems). A type system is monomorphic, if any well-typed program has exactly one type. Of course, ill-typed programs have no type (unless one defines it in such a way that there is a specific “error type”, but let’s not do that). A type system is polymorphic, if it’s not monomorphic, i.e., there can be programs with more than one type. Being monomorpic makes a type system very “rigid” and unflexible. Basically all static type sytems are polymorphic in one way or the other. According to a well-known classification, one can distinguishes 4 kinds of polymorphism, subtyping polymorphism, generic polymorphism, overloading, and coercion. Here, we are talking about generic polymorphism.

Our (Curry-style) type system we started with, the one without type variables, is polymorphic. It’s polymorphic, even if there are no type variables. I stress that, because sometimes one may see statements “for polymorphism, one needs type variables”, or that the simply typed lambda is called the monophic lambda calculus (we are doing basically the simply typed lambda calculus plus recursion). The latter name probably to highlight the difference between what is called the polymorphic lambda calculus (PLC or system F), or the systems with Ml-style polymorphism, which is weaker than the PLC.

But actually, the system we took as starting point (without type variables) is technically polymorphic. To qualify such systems wtithout type variables as monomorpic is not altogether wrong. There are at least no polymorphic types, for that one needs type variables.¹ So the STL definitely has only monoprhic types (but the type system is polymorphic). So be called polymorphic in proper manner, one would indeed need type variables, to reflect the polymorphism of the type system properly in the types themselves. So the statement “for polymorphism one needs type variables” is defendable, because without type variables it does not enable to make use of the polymorphism (and type inference does not work as well)

And we should not forget: we are disucssing here the Curry-style variant. If one takes the Church-style variant of the STL, then it is factually true: that system is monomorphic (but there is also no need for type inference or type reconstruction).

¹

Now, what about lets? The let-construct is important indeed, it’s the way in the calculus to give “names” to function abstractions, and thus to reuse them. Procedural abstraction, i.e., abstracting a funtionality into a function, is central in all mildly high-level programming languages. If one can apply a function only once, functional abtraction is mostly pointless. Also, if one can define polymorphic functions, i.e., functions whose functional type contains type variables, but can make only monomorphic use, that reduces the attractiveness of that form of polymorphism somewhat. The function may be polymorphically typed, and can call such a function multiple times, but the usage is monomorphic. Each call of the function must be on arguments of the same type. That would not make the feature useless. For instance, a library could offer some sorting function on lists of type² list 'a -> 'list 'a, different client code bases could use that function differently, in one program for sorting strings, another program for sorting something else. But in the same global program, the use has to be monomorphic. That’s still useful, but quite limited.

Why are lets monomorphic in our system?

The augmented type system has type variables, so a sorting function can have the polymorphic type list 'a -> list 'a, so why is the let monomorphic? That’s a consequence of the global nature of type variables and the unification constraints. When one uses a function, that leads to a constraint in the corresponding type variable. For instance, if one uses the sorting function on strings, that instantiates the above variable 'a to string, and that is a global choice. Any other usage of the function in the sorting function will lead to failure when trying to solve the contradictory constraints.

The core of the problem is the gobal nature of the type variables: making a choice at one point of usage restricts all other usages. One way out is the working with bound type variables, more precisely with universally quantified ones. So, instead of list 'a -> list 'a, the sorting function is of forall 'a. list 'a -> list 'a (or $\forall \alpha. \alpha \rightarrow \alpha$ in math notation). Constraint solving is about finding a solution for the free variables, so bound variables, like universally quantified one, are not subject to substitution.

Of course, conceptually, list 'a -> list 'a is “meant” as universally quantified, it specifies a function working polymorphically for all concrete types, “same” as the explicitly quantified version. However, the quantification is the “trick” needed to avoid the global choices for type variables, and this avoidance enables polymorphic lets.

The types with universal quantifiers added are known in the context of ML polymorphism also as poly-types or type schemes.

Poly-types resp. type schemes

The language or syntax of types becomes more comples, it consists of two layers. On top of the types as covered by the lecture, i.e., the usual type constructors and type variables, there is a second layer, the type schemes or poly-types, which can be quantified. More precisely, one can use quantifiers only “in front of” mono-types. That’s called prenex quantified types. Quantifiers cannot be used nested inside a type. That makes the type structure stricly layered: the “lower” layer of mono-types, and, separate from that, the layer of type schemes. That layering is directly visible in the grammar for types and type schemes.

This stratification, types one the one hand and, on top of that, type schemes, is pretty important. It also affects what the variables, quantified or not, stand for. Type variables, so much is clear, represent “types”. But it’s crucial that type variables here represent mono-types and especially do not represent poly-types. So, substitutions are mappings from type variables to mono-types. Related to that: universal quantifiers express universality or polymorphic behavior for all mono-types and not for all types in general. In particular, the quantifier in a poly-type is not meant as “for all types including myself”. Allowing that form of self-reference or recursion in quantification would mean a quantum leap in expressivity. And it would make type inference undecidable, also in that sense the laying is essential.

What practical consequence does that restriction have? It means, one can have polymorphic functions, also let-bound, but one cannot have polymorphic functions as arguments to functions. So, one has higher-order function and one has polymorphic functions, but polymorphism is first-order only.

We don’t present the type system or the corresponding ML-type inference system here, there are many accessible presentations in text books and on the internet. Just a few more remarks: the core of the algortithms is term unification, as we did for the rules for the monomorphic let. The new thing is how to make use of the quantifiers, i.e., the polytypes. One can see it like that: let’s assume a let-binding and what is being defined is a poly-morphic function, like let sort = (fn l => [code]) with plausble type of the abstraction as list 'a -> list 'a. The, the functional variable sort is remembered in the context no with this type, but with the corresponding poly-type, it, universally quantified. One has to be a bit careful there. In general situation, one cannot just quantify simply all variables mentioned in the type of the right-hand side of the let-bound variables. There could be variables mentioned that are relevant also in the larger context, and of course one cannot just switch their status from being a free variable to a bound one, breaking the connection betwenn the context and the local definition. So in general, the algorthim would prenex-quantify the mono-type as much as possible, when dealing with lets. That’s the treatment when defining a function, resp. giving a name to a function. What should be done when using the function? In the mono-let setting that’s where unification is done, resp. when unification constraints are generated. Now, the function name is typed by a poly-type which quantified variables. What is done then is: one gets rid of the quantifier, by using a free variable. Best is a fresh one (and that’s what the algo would do), and only after that, one starts unifying. In that way, different calls of the same function will chose (for the same bound variable) difference fresh free variables and this way, the different instances are not “coupled”. In this way, one can make polymorphic use of the function!

PLC, second-order lambda calculus, and System F

As discussed, ML polymorphism is rectricted considerable: polymorphims is first-order: one can have polymorphic functions, one can have higher-order functions, for instance functions that take other functions as argument, but one cannot have polymorphic functions as argument to other functions. That may be a good compromise in practice, but is still a severe restriction. The restriction is captured by the statification between mono-types and poly-types. If one gives up that layering, one has only types, which contain variables, which can be universally quantified, and the quantifiers can also be used in non-prenex position (i.e., inside a type). The corresponding system is known under different names, System F, the polymorpic $\lambda$-calculus, or the second-order $\lambda$-calculus.

The name, polymorpgic lambda calculus explains itself, the alternative name “System F” or “Système F” in French, is due to historic reasons (given by one of its inventors, Girard). The terminology PLC comes from Reynolds, who came up with that calculus independently.

The word “second-order lambda calculus” may need some explanation. It’s not about that one has “second-order functions”. Already the simply typed lambda calculus allows higher-order functions. The second-orderness refers to the expressivenes of the types. The type system features quantification over type variables, and the quantification is actually pretty powerful.

In particular, the quantification in a type of the form $\forall \alpha. T$ ranges over all types, and that includes that universally quantified type itself! That form is self-referentiality is called impredicative in this context. It also goes beyond first-order logic. There, one has relations and sets on the one hand and “objects” or “things” one can quantify about. Like $\forall x. x+1 \geq x$, where the quantification is intended to range natural numbers, say, and $+$ and $\geq$ can be interpreted as operations and relations on natural numbers, but one cannot get a property by quantifying over formulas or properties themselves. Impredicativity is expressive, and “dangerous” as well, It’s related to constructitions like “the set of all sets”, when considering that the “collection” of sets as a set itself is a well-known source of paradoxies. Like: the set of sets that don’t contain themselves is contradictory.

Anyay, second-order logic allows to quantify over sets or properties, in an analogous way that the types of the PLC allow to quantify over types, and that analogy is the reason why the calculus is also called second-order lambda calculus. Actually, the connection between logics and types is (much) deeper than a mere analogy. The connection is called the Curry-Howard isomorphism (and an mathematical isomorphism is much deeper than an analogy, indeed). But this is beyond this text about polymorphic-lets. At any rate: ML-style polymorphism is predicative, not impredicative.

Polymorphic recursion

Footnotes

¹ Implicitly, when I say polymorphism, I mean parametric polymorphism, the one we are tackling. Other kinds of polymorphism are typically formulated without introducing type variables.

² To be polymorphic, the sorting function should take as input not just the list to be sorted, but also the comparison function. So more realistically, the type should be something like ('a -> 'a -> bool) -> list 'a -> 'list 'a. For simplicity, that aspect is suppressed.