I have a language in which types are unboxed by default, with type inference based on Hindley–Milner. I’d like to add higher-rank polymorphism, mainly for working with existential types.

I think I understand how to check these types, but I’m not sure what to do when compiling. Currently, I compile polymorphic definitions by generating specialisations, much like C++ templates, so that they can work with unboxed values. E.g., given a definition of f<T>, if the program invokes only f<Int32> and f<Char>, then only those specialisations appear in the compiled program. (I’m assuming whole-program compilation for now.)

But when passing a polymorphic function as an argument, I don’t see how I can generate the right specialisation statically, because the function could be selected at runtime. Do I have no choice but to use a boxed representation? Or is there a way around the issue?

My first thought was to somehow encode rank-n polymorphism as rank 1, but I don’t believe it’s possible in general because a formula in constructive logic doesn’t necessarily have a prenex normal form.

  • $\begingroup$ An alternative is to reduce the amount of boxing needed by storing bitmaps for which arguments of a function and words in memory are pointers. Then a polymorphic function/struct is actually polymorphic over a pointer or an arbitrary word of data, and structs can store their last field (even if it's polymorphic) inline. Those bitmaps can also be used by the GC to avoid the need for tagwords for non-sum types. $\endgroup$
    – fread2281
    Feb 16 '17 at 22:19
  • $\begingroup$ @fread2281: I actually used to do something like that in an older version of the language. I don’t currently generate tags for non-sum types, and there’s no GC. I think that’s compatible with Neel K’s approach as well. $\endgroup$
    – Jon Purdy
    Feb 16 '17 at 23:16

I've thought a bit about this. The main issue is that in general, we don't know how big a value of polymorphic type is. If you don't have this information, you have have to get it somehow. Monomorphisation gets this information for you by specializing away the polymorphism. Boxing gets this information for you by putting everything into a representation of known size.

A third alternative is to keep track of this information in the kinds. Basically, what you can do is to introduce a different kind for each data size, and then polymorphic functions can be defined over all types of a particular size. I'll sketch such a system below.

$$ \newcommand{\bnfalt}{\;\;|\;\;} \newcommand{\rule}[2]{{\mathord{\array{#1}} \over {\mathord{#2}}}} \newcommand{\judge}[3]{{#1} \vdash {#2} : {#3}} $$ $$ \begin{array}{llcl} \mbox{Kinds} & \kappa & ::= n \\ \mbox{Type constructors} & A & ::= & \forall a:\kappa.\; A \bnfalt \alpha \bnfalt A \times B \bnfalt A + B \bnfalt A \to B \\ & & | & \mathsf{ref}\;A \bnfalt \mathsf{Pad}(k) \bnfalt \mu \alpha:\kappa.\; A\\ \end{array} $$

Here, the high level idea is that the kind of a type tells you how many words it takes to lay out an object in memory. For any given size, it's easy to be polymorphic over all types of that particular size. Since every type -- even polymorphic ones -- still has a known size, compilation isn't any harder than it is for C.

The kinding rules turn this English into math, and should look something like this: $$ \rule{ \alpha:n \in \Gamma} { \judge{\Gamma}{\alpha}{n} } \qquad \rule{ \judge{\Gamma, \alpha:n}{A}{m} } { \judge{\Gamma}{\forall \alpha:n.\; A}{m} } $$ $$ \rule{ \judge{\Gamma}{A}{n} & \judge{\Gamma}{B}{m} } { \judge{\Gamma}{A \times B}{n + m} } \qquad \rule{ \judge{\Gamma}{A}{n} & \judge{\Gamma}{B}{n} } { \judge{\Gamma}{A + B}{n + 1} } $$ $$ \rule{ \judge{\Gamma}{A}{m} & \judge{\Gamma}{B}{n} } { \judge{\Gamma}{A \to B}{1} } \qquad \rule{ \judge{\Gamma}{A}{n} } { \judge{\Gamma}{\mathsf{ref}\;A}{1} } $$ $$ \rule{ } { \judge{\Gamma}{\mathsf{Pad}(k)}{k} } \qquad \rule{ \judge{\Gamma, \alpha:n}{A}{n} } { \judge{\Gamma}{\mu \alpha:n.\; A}{n} } $$

So the forall quantifier requires you to give the kind you are ranging over. Likewise, pairing $A \times B$ is an unboxed pair type, which just lays out an $A$ next to a $B$ in memory (like a C struct type). Disjoint unions take two values of the same size, and then add a word for a discriminator tag. Functions are closures, represented as usual by a pointer to a record of the environment and the code.

References are interesting -- pointers are always one word, but they can point to values of any size. This lets programmers implement polymorphism to arbitrary objects by boxing, but doesn't require them to do so. Finally, once explicit sizes are in play, it's often useful to introduce a padding type, which uses space but doesn't do anything. (So if you want to take the disjoint union of an int and a pair of ints, you'll need to add padding the first int, so that the object layout is uniform.)

Recursive types have the standard formation rule, but note that recursive occurences have to be the same size, which means you usually have to stick them in a pointer to make the kinding work out. Eg, the list datatype could be represented as

$$ \mu \alpha:1.\; \mathsf{ref}\;(\mathsf{Pad}(2) + \mathsf{int} \times \alpha) $$

So this points to an empty list value, or a pair of an int and a pointer to another linked list.

Type checking for systems like this is also not very hard; the algorithm in my ICFP paper with Joshua Dunfield, Complete and Easy Bidirectional Typechecking for Higher Rank Polymorphism applies to this case with almost no changes.

  • $\begingroup$ Cool, I think this neatly covers my use case. I was aware of using kinds to reason about value representations (like GHC’s * vs. #), but hadn’t considered doing it this way. It seems reasonable to restrict higher-ranked quantifiers to types of known size, and I think this would also let me generate per-size specialisations statically, without needing to know the actual type. Now, time to re-read that paper. :) $\endgroup$
    – Jon Purdy
    Feb 14 '17 at 3:34

This seems to be closer to a compilation problem than a "theoretical computer science" problem, so you're probably better off asking elsewhere.

In the general case, indeed, I think there is no other solution than using a boxed representation. But I also expect that in practice there are many different alternative options, depending on the specifics of your situation.

E.g. the low-level representation of unboxed arguments can usually be categorized into very few alternatives, e.g. integer-or-similar, floating-point, or pointer. So for a function f<T>, maybe you really only need to generate 3 different unboxed implementations and you can represent the polymorphic one as a tuple of those 3 functions, so instantiating T to Int32 is just selecting the first element of the tuple, ...

  • $\begingroup$ Thanks for your help. I wasn’t really sure where to ask, since a compiler spans from high-level theory down to low-level engineering, but I figured people around here would have some ideas. It’s looking like boxing may indeed be the most flexible approach here. After reading your answer and thinking on it more, the only other reasonable solution I’ve been able to come up with is to give up some flexibility and require polymorphic arguments to be known statically, e.g., by passing them as type parameters themselves. It’s tradeoffs all the way down. :P $\endgroup$
    – Jon Purdy
    Feb 13 '17 at 3:57
  • 4
    $\begingroup$ The OP's question contains perfectly valid TCS problems, like how to do type inference when Damas-Hindley-Milner is extended with higher rank types. In general rank-2 polymorphism has decidable type-inference but for rank k>2 type-inference is undecidable. Whether the Damas-Hindley-Milner restriction changes this, I don't know. Finally just about everything modern compilers do should be part of TCS, but usually isn't because the compiler implementors are ahead of theoreticians. $\endgroup$ Feb 13 '17 at 9:15

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.