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

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

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

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

<p>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} &amp;
         \judge{\Gamma}{B}{m} }
       { \judge{\Gamma}{A \times B}{n + m} }
  \qquad
  \rule{ \judge{\Gamma}{A}{n} &amp;
         \judge{\Gamma}{B}{n} }
       { \judge{\Gamma}{A + B}{n + 1} }
$$
$$
  \rule{ \judge{\Gamma}{A}{m} &amp;
         \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}
       }
$$</p>

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

<p>References are interesting -- pointers are always one word, but they
can point to values of any size. This lets programmers <em>implement</em>
polymorphism to arbitrary objects by boxing, but doesn't <em>require</em>
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.) </p>

<p>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 </p>

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

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

<p>Type checking for systems like this is also not very hard; the
algorithm in my ICFP paper with Joshua Dunfield, <a href="https://arxiv.org/abs/1306.6032" rel="nofollow noreferrer"><em>Complete and Easy
Bidirectional Typechecking for Higher Rank
Polymorphism</em></a> applies to this case
with almost no changes. </p>

CC BY-SA 3.0
2017-02-14T03:34:59.533Z
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. :)
Jon Purdy
CC BY-SA 3.0
2017-02-13T11:06:14.630Z
2017-02-16T10:12:02.943Z
2017-02-16T10:12:02.943Z
Neel Krishnaswami
<p>This seems to be closer to a compilation problem than a "theoretical computer science" problem, so you're probably better off asking elsewhere.</p>

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

<p>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 <code>f&lt;T&gt;</code>, 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, ...</p>

CC BY-SA 3.0
2017-02-13T03:57:43.313Z
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
Jon Purdy
CC BY-SA 3.0
2017-02-13T09:15:36.073Z
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.
Martin Berger
CC BY-SA 3.0
2017-02-12T20:56:13.863Z
2017-02-12T20:56:13.863Z
Stefan
<p>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.</p>

<p>I think I understand how to <em>check</em> 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 <code>f&lt;T&gt;</code>, if the program invokes only <code>f&lt;Int32&gt;</code> and <code>f&lt;Char&gt;</code>, then only those specialisations appear in the compiled program. (I’m assuming whole-program compilation for now.)</p>

<p>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?</p>

<p>My first thought was to somehow encode rank-<em>n</em> 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.</p>

CC BY-SA 3.0
2017-02-16T22:19:17.550Z
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.
fread2281
CC BY-SA 3.0
2017-02-16T23:16:29.860Z
@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.
Jon Purdy
<type-theory><type-inference><polymorphism>
Higher-rank polymorphism over unboxed types
Jon Purdy
# Higher-rank polymorphism over unboxed types

(Asked by: username_0 on 2017-02-11)

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`, if the program invokes only `f` and `f`, 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.

**Tags:** type-theory, type-inference, polymorphism

> **Comments:**
> **username_1**: 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.  
> **username_0**: @username_1: 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.  

---

## 2 answers

### Answer by username_2 on 2017-02-13. Score: 6 | Accepted answer

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*](https://arxiv.org/abs/1306.6032) applies to this case
with almost no changes.

> **Comments:**
> **username_0**: 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. :)  

---

### Answer by username_3 on 2017-02-12. Score: 1

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

> **Comments:**
> **username_0**: 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  
> **username_4**: 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.  

---

