mmmodularity!

» by Scott Kilpatrick

Update: Now using MathJax to render mathy things nicely.

$\newcommand{\int}{\mathrm{int}}\newcommand{\bool}{\mathrm{bool}}\newcommand{\string}{\mathrm{string}}$In this post I provide background information on an idea that I’ll explain in the next post. People familiar with Hindley-Milner and type classes won’t get much out of this, except maybe the last part.

Hindley-Milner: the sacrosanct type system for functional programming

The Hindley-Milner type system (HM) comes in two flavors, declarative and algorithmic. The former axiomatizes (as a hypothetical judgment defined by inference rules) the notion of “well-typed” programs while the latter — known as “Algorithm W”, and also referred to as “type inference” — describes a mechanical process for computing the (principal) type of a program. Their coexistence is not superfluous: unlike the algorithm, the declarative system serves as a minimal, human-readable (and machine-provable) specification of the types of programs. 

Perhaps counterintuitively, these two flavors don’t precisely capture the same notions. Algorithm W, introduced in Damas-Milner (1982),¹ computes only the principal type of the given expression, whereas the specification characterizes all possible types (including the principal type) of that expression. This distinction carries little significance, however, because of the following properties: The soundness property of W asserts that every type computed is indeed a valid type of the program; the completeness property asserts that if a program has some type in the specification, then W computes a more general type for that program — once again, the principal type. An important consequence of these properties is that the two approaches agree on which expressions have any type at all.

As a quick example, consider the identity function in HM, written $\lambda x.x$. (Note that no type for the “function parameter” $x$ is specified; this type-free style is one of the hallmarks of HM.) The declarative type system says that this expression has type $\int \rightarrow \int$ … and $\bool \rightarrow \bool$ and so on. Algorithm W computes $a \rightarrow a$, for some type variable $a$, as the type of this expression, and the soundness property ensures that the specification agrees.

Type classes and the problem of too many types

The specification considers more than merely the principal type as valid types of a program. So what? In straight-up HM the computational behavior of a program doesn’t depend on any particular type that it inhabits; e.g. the identity function $\lambda x.x$ behaves as the identity function despite whichever type we point out that it inhabits. When you extend HM with type classes,² however, the behavior of programs do indeed depend on which types they inhabit. The code that is executed at run-time depends on the type assigned to the program during compile-time.

In the words of Odersky, Wadler, and Wehr, “under Hindley-Milner, a program is untypeable only if it may have no meaning; under type classes, a program may be untypeable because it has too many meanings.”

As a classical example, consider the standard functions $show$ and $read$ which convert into and out of string representations. The type of $show$ says that, given an implementation of how things of type $a$ can be converted to strings, show performs the conversion on an $a$-thing, and the type of $read$ is similar. The expressions $show~5$ and $not~(read \mathtt{“True”})$, as expected, will use the $\int$- and $\bool$-specific implementations at run-time, respectively; even $not (read \mathtt{“5”})$ is still well-typed since we certainly know how to read into bools (though at run-time it will fail to convert $\mathtt{“5”}$ to a $\bool$).

More enigmatic expressions are also possible, such as $show (read \mathtt{“5”})$. Because we can $read$ and $show$ $\int$s, $read$ and $show$ have the types $\string \rightarrow \int$ and $\int \rightarrow \string$ respectively. Similarly, because we can read and show bools, they also have the types $\string \rightarrow \bool$ and $\bool \rightarrow \string$. For this expression, both the int- and bool-interpretations are completely valid, which implies, in both cases, that the entire expression has type $\string$. This expression is well-typed but its computational behavior depends on the specifics of how it is well-typed — with ints or with bools, yielding distinct executions. We call such expressions ambiguous.

Strange typing of ambiguous programs

The declarative specification of type systems based on type classes (such as all formal models of Haskell) naively characterizes ambiguous programs as well-typed. What, then, does the algorithm have to say about ambiguous programs?

For the “show-read” example above, the algorithm would produce the type $\forall a. (\mathrm{Show}~a, \mathrm{Read}~a) \Rightarrow \string$ which says, roughly, “given an implementation for showing and reading some type $a$, this is a $\string$.” In a sense, this type is more general than string, and indeed the specification would assign this type as well; in fact this is the program’s principal type.

But! The algorithm does not actually compute the above type for the “show-read” program. Because the type variable $a$ appears in the type class constraints $\mathrm{Show}~a$ and $\mathrm{Read}~a$ but not the “body type” string, the algorithm determines that this program must be ambiguous and thus rejects the program. The type system has now, perversely, accepted a program through the specification but rejected it through the algorithm. The vital completeness property of the algorithm, discussed above, no longer holds.

The failure of the algorithm to accept ambiguous programs does not accurately describe the problem. Instead, it’s the failure of the specification: it shouldn’t be accepting ambiguous programs in the first place since they exhibit distinct computational behaviors depending on which particular type they inhabit. One could weaken the specification to avoid these programs, but, so the saying goes, one would then violate the simplicity of the specification, thus defeating the purpose of separating it from the algorithm. (Hint for the next post: I came up with an idea for a specification that does this while retaining the simplicity.)

For the time being, we just live without a complete algorithm; or we just live with a slightly too permissive specification, depending on how you look at it.³

* * *

¹ Several others had discovered essentially the same algorithm albeit in different contexts. Says Hindley — one of those authors — in 1988: ”There must be a moral to this story of continual re-discovery; perhaps someone along the line should have learned to read. Or someone else learn to write.”
² Jones’ work on qualified types, e.g. his ESOP’92 paper, offer the most HM-like presentation of type classes. His report on coherence discusses the ambiguity issue in more detail.
³ For a clearer elaboration of this unsatisfying solution to ambiguity, see Sections 6 and 9.6 of Vytiniotis et al.’s current JFP draft.