Type inference with product types

Question

I’m working on a compiler for a concatenative language and would like to add type inference support. I understand Hindley–Milner, but I’ve been learning the type theory as I go, so I’m unsure of how to adapt it. Is the following system sound and decidably inferable?

A term is a literal, a composition of terms, a quotation of a term, or a primitive.

$$ e ::= x \:\big|\: e\:e \:\big|\: [e] \:\big|\: \dots $$

All terms denote functions. For two functions $e_1$ and $e_2$, $e_1\:e_2 = e_2 \circ e_1$, that is, juxtaposition denotes reverse composition. Literals denote niladic functions.

The terms other than composition have basic type rules:

$$ \dfrac{}{x : \iota}\text{[Lit]} \\ \dfrac{\Gamma\vdash e : \sigma}{\Gamma\vdash [e] : \forall\alpha.\:\alpha\to\sigma\times\alpha}\text{[Quot]}, \alpha \text{ not free in } \Gamma $$

Notably absent are rules for application, since concatenative languages lack it.

A type is either a literal, a type variable, or a function from stacks to stacks, where a stack is defined as a right-nested tuple. All functions are implicitly polymorphic with respect to the “rest of the stack”.

$$ \begin{aligned} \tau & ::= \iota \:\big|\: \alpha \:\big|\: \rho\to\rho \\ \rho & ::= () \:\big|\: \tau\times\rho \\ \sigma & ::= \tau \:\big|\: \forall\alpha.\:\sigma \end{aligned} $$

This is the first thing that seems suspect, but I don’t know exactly what’s wrong with it.

To help readability and cut down on parentheses, I’ll assume that $a\:b = b \times (a)$ in type schemes. I’ll also use a capital letter for a variable denoting a stack, rather than a single value.

There are six primitives. The first five are pretty innocuous. dup takes the topmost value and produces two copies of it. swap changes the order of the top two values. pop discards the top value. quote takes a value and produces a quotation (function) that returns it. apply applies a quotation to the stack.

$$ \begin{aligned} \mathtt{dup} & :: \forall A b.\: A\:b \to A\:b\:b \\ \mathtt{swap} & :: \forall A b c.\: A\:b\:c \to A\:c\:b \\ \mathtt{pop} & :: \forall A b.\: A\:b \to A \\ \mathtt{quote} & :: \forall A b.\: A\:b \to A\:(\forall C. C \to C\:b) \\ \mathtt{apply} & :: \forall A B.\: A\:(A \to B) \to B \\ \end{aligned} $$

The last combinator, compose, ought to take two quotations and return the type of their concatenation, that is, $[e_1]\:[e_2]\:\mathtt{compose} = [e_1\:e_2]$. In the statically typed concatenative language Cat, the type of compose is very straightforward.

$$ \mathtt{compose} :: \forall A B C D.\: A\:(B \to C)\:(C \to D) \to A\:(B \to D) $$

However, this type is too restrictive: it requires that the production of the first function exactly match the consumption of the second. In reality, you have to assume distinct types, then unify them. But how would you write that type?

$$ \mathtt{compose} :: \forall A B C D E. A\:(B \to C)\:(D \to E) \to A \dots $$

If you let $\setminus$ denote a difference of two types, then I think you can write the type of compose correctly.

$$ \mathtt{compose} :: \forall A B C D E.\: A\:(B \to C)\:(D \to E) \to A\:((D \setminus C)\:B \to ((C \setminus D)\:E)) $$

This is still relatively straightforward: compose takes a function $f_1 : B \to C$ and one $f_2 : D \to E$. Its result consumes $B$ atop the consumption of $f_2$ not produced by $f_1$, and produces $D$ atop the production of $f_1$ not consumed by $f_2$. This gives the rule for ordinary composition.

$$ \dfrac{\Gamma\vdash e_1 : \forall A B.\: A \to B \quad \Gamma\vdash e_2 : \forall C D. C \to D}{\Gamma\vdash e_1 e_2 : ((C \setminus B)\:A \to ((B \setminus C)\:D))}\text{[Comp]} $$

However, I don’t know that this hypothetical $\setminus$ actually corresponds to anything, and I’ve been chasing it around in circles for long enough that I think I took a wrong turn. Could it be a simple difference of tuples?

$$ \begin{align} \forall A. () \setminus A & = () \\ \forall A. A \setminus () & = A \\ \forall A B C D. A B \setminus C D & = B \setminus D \textit{ iff } A = C \\ \text{otherwise} & = \textit{undefined} \end{align} $$

Is there something horribly broken about this that I’m not seeing, or am I on something like the right track? (I’ve probably quantified some of this stuff wrongly and would appreciate fixes in that area as well.)

Answer 1

The following rank-2 type $$\text{compose}:\forall ABC\delta. \delta\ (\forall \alpha.\alpha\ A\to \alpha B)\ (\forall \beta.\beta\ B\to \beta C) \to \delta\ (\forall \gamma.\gamma\ A\to \gamma C)$$ seems to be sufficiently general. It is much more polymorphic than the type proposed in the question. Here variable quantify over contiguous chunks of stack, which captures multi-argument functions.

Greek letters are used for the rest-of-the-stack variables for clarity only.

It expresses the constraints that the output stack of the first element on the stack needs to be the same as the input stack of the second element. Appropriately instantiating the variable $B$ for the two actually arguments is the way of getting the constraints to work properly, rather than defining a new operation, as you propose in the question.

Type checking rank-2 types is undecidable in general, I believe, though some work has been done that gives good results in practice (for Haskell):

• Simon L. Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich, Mark Shields: Practical type inference for arbitrary-rank types. J. Funct. Program. 17(1): 1-82 (2007)

The type rule for composition is simply:

$$ \dfrac{\Gamma\vdash e_1:\forall \alpha. \alpha\ A\to \alpha\ B\qquad \Gamma\vdash e_1:\forall \alpha. \alpha\ B\to \alpha\ C} {\Gamma\vdash e_1\ e_2:\forall \alpha.\alpha\ A\to\alpha\ C} $$

To get the type system to work in general, you need the following specialisation rule:

$$ \dfrac{\Gamma\vdash e:\forall \alpha. \alpha\ A \to \alpha\ B} {\Gamma\vdash e:\forall \alpha.C\ A\to \alpha\ C\ B} $$