Type inference with product types

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

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}
$$

StackExchange Computer Science Q#2326, answer score: 9