mmmodularity!

» by Scott Kilpatrick

In the last post I discussed the ambiguity and incompleteness of the Hindley-Milner type system with type classes. I also mentioned that I would follow it up with an idea I was pursuing, which, as it turns out, I’m no longer pursuing. This time I’ll motivate the idea by explaining why I was led to it in the first place. The last post describes, really, the post hoc motivation for it, whereas this post describes the actual motivation. 

A yucky specification of principal type

Note: Throughout this post I sling around the word “impredicativity” a lot. If anyone notices that my understanding of it isn’t quite right, please let me know!

For our revised take on modular type classes, we depend on the principal type of certain expressions (for reasons I won’t quite get into now). One way to specify this is with a rule like $$\frac{\Gamma \vdash e : \tau \qquad (\forall \tau’ .\; \Gamma \vdash e : \tau’ \quad\Rightarrow\quad \vdash \tau’ \le \tau)}{\Gamma \vdash \cdots e \cdots :\; \cdots \tau \cdots}\rlap{(\ast)}$$ wherein $\tau$ must be the principal type of $e$ in context $\Gamma$.

Notice that the second premise of $(\ast)$ involves the typing relation itself in a negative position. Inductive pedants (like the Coq type checker) know this is a big, red flag in an inductive definition. That negative occurrence means that the generating function denoted by the inference rule(s) for the relation might not have a least fixed point — that’s a problem, ‘cause inductive definitions are defined as least fixed points. But since the typing relation is “invoked” on a structurally smaller “argument” in the premise than in the conclusion ($e \in \cdots e \cdots$), the relation is still well-defined. It could (probably) be defined as a $\mathtt{Fixpoint}$ in Coq, but not an $\mathtt{Inductive}$ — which comes equipped with nice properties like a free inductive proof principle (again, which may or may not even hold for this relation). (Question: Does such a negative occurrence always entail that the relation is impredicative?)

Defining a typing relation with the rule $(\ast)$ is complicated for technical reasons (and aesthetic reasons too, if you ask me) and mired in questions of impredicativity. How can we rephrase the typing for this expression to circumvent that complexity and uncertainty? By constructively (or perhaps, predicatively) defining what it means for an expression to have a principal type rather than defining it as “the type that is more general than all other types.” Then we could cleanly appeal to that notion of principal typing in the rule $(\ast)$. (We’d have to take care, however, to preclude circularity in our definitions of normal typing and principal typing.)

As it turns out, replacing impredicative definitions has some precedent: See the excellent responses by Andrej Bauer and Neel Krishnaswami to a mathoverflow user who asks, essentially, why bother going the extra mile to define an object predicatively rather than impredicatively. And just today Gil explained that he is devising a new logical relation for program equivalence that pushes out the impredicativity; in his case, he needs the definition of the relation to be a monotonic function in order to guarantee the existence of a greatest fixed point.

Back to Hindley-Milner

We’ve seen how the declarative specification of HM with type classes “over-characterizes” ambiguous programs like $show~(read~”1”)$, while the type inference (or type checking) algorithm, Algorithm W, rejects them outright — due to the syntactic ambiguity of their types.

Generally, this incompleteness is viewed as a minor niggle and not something to worry about. Never one to turn down the chance to worry about something, I determined to fix this “problem.” If the declarative specification of HM typing only characterized principal typings, then it would precisely coincide with Algorithm W and it would never consider ambiguous programs to be well-typed.

As I mentioned before, it’s well known that one could merely shove Algorithm W into the declarative specification, achieving the desired result at the expense of a convenient, readable specification. But if we can construct the nice, predicative definition of a principal typing relation, then we can use that for the HM specification. What smoothes out the technical specifics of our modular type classes work would also do the same for basic properties of the Hindley-Milner type system with type classes! That would be nice.

Now that I’ve motivated the construction of a principal typing relation for Hindley-Milner, I need to explain my ideas for defining it. Unfortunately, they didn’t quite pan out. I believe the French phrase is c’est la vie, which translates to “oh, grad school.” Stay tuned for the exciting conclusion to this month’s episode of “Promising Ideas that Led to Nothing but Might be Continued Later!”