Wnioskowanie typu na podstawie typów produktów

Pracuję nad kompilatorem dla języka konkatenatywnego i chciałbym dodać obsługę wnioskowania typu. Rozumiem Hindleya-Milnera, ale nauczyłem się teorii typów, więc nie jestem pewien, jak ją dostosować. Czy następujący system jest dźwiękowy i można go w sposób zdecydowanie wywnioskować?

Termin jest literałem, kompozycją terminów, cytatem terminu lub prymitywem.

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

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

Wszystkie terminy oznaczają funkcje. Dla dwóch funkcji i , $e_1$ $e_2$ $e_1\:e_2 = e_2 \circ e_1$ , to znaczy zestawienie oznacza skład odwrotny. Literały oznaczają funkcje niladyczne.

Terminy inne niż skład mają podstawowe zasady dotyczące typów:

\frac{}{x : ι} [Lit] \frac{Γ ⊢ e : σ}{Γ ⊢ [e] : \forall α . α \to σ \times α} [Quot], α not free in Γ

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

Szczególnie nie ma zasad stosowania, ponieważ brakuje im języków konkatenatywnych.

Typ jest literałem, zmienną typu lub funkcją od stosów do stosów, gdzie stos jest zdefiniowany jako krotka zagnieżdżona z prawej strony. Wszystkie funkcje są domyślnie polimorficzne w odniesieniu do „reszty stosu”.

\begin{aligned} τ & ::= ι | α | ρ \to ρ \\ ρ & ::= () | τ \times ρ \\ σ & ::= τ | \forall α . σ \end{aligned}

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

To pierwsza rzecz, która wydaje się podejrzana, ale nie wiem dokładnie, co jest z nią nie tak.

Aby pomóc czytelności i obniżyć nawiasach, będę zakładać, że $a\:b = b \times (a)$ w schematach typów. Użyję również dużej litery do zmiennej oznaczającej stos, a nie do pojedynczej wartości.

Istnieje sześć prymitywów. Pierwsze pięć jest dość nieszkodliwe. dupprzyjmuje najwyższą wartość i tworzy dwie jej kopie. swapzmienia kolejność dwóch najwyższych wartości. popodrzuca najwyższą wartość. quoteprzyjmuje wartość i tworzy cytat (funkcję), który ją zwraca. applystosuje ofertę do stosu.

\begin{aligned} d u p & :: \forall A b . A b \to A b b \\ s w a p & :: \forall A b c . A b c \to A c b \\ p o p & :: \forall A b . A b \to A \\ q u o t e & :: \forall A b . A b \to A (\forall C . C \to C b) \\ a p p l y & :: \forall A B . A (A \to B) \to B \end{aligned}

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

Ostatni kombinator composepowinien wziąć dwa cytaty i zwrócić rodzaj ich konkatenacji, czyli . W statycznie typowanym języku konkatenatywnymCattypjest bardzo prosty. $[e_1]\:[e_2]\:\mathtt{compose} = [e_1\:e_2]$ compose

c o m p o s e :: \forall A B C D . A (B \to C) (C \to D) \to A (B \to D)

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

Jednak ten typ jest zbyt restrykcyjny: wymaga, aby produkcja pierwszej funkcji dokładnie odpowiadała zużyciu drugiej. W rzeczywistości musisz założyć różne typy, a następnie je zunifikować. Ale jak byś napisał ten typ?

c o m p o s e :: \forall A B C D E . A (B \to C) (D \to E) \to A \dots

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

Jeśli pozwolisz oznaczać różnicę dwóch typów, to myślę, że możesz napisać typ poprawnie. $\setminus$ compose

c o m p o s e :: \forall A B C D E . A (B \to C) (D \to E) \to A ((D ∖ C) B \to ((C ∖ D) E))

$\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))$

Jest wciąż stosunkowo prosta: composewykonuje funkcję i jeden . Jego wynik zużywa na szczycie zużycia niewyprodukowanego przez , i daje na szczycie produkcji niewykorzystanego przez . Daje to regułę dla zwykłego składu. $f_1 : B \to C$ $f_2 : D \to E$ $B$ $f_2$ $f_1$ $D$ $f_1$ $f_2$

\frac{Γ ⊢ e_{1} : \forall A B . A \to B Γ ⊢ e_{2} : \forall C D . C \to D}{Γ ⊢ e_{1} e_{2} : ((C ∖ B) A \to ((B ∖ C) D))} [Comp]

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

Jednak nie wiem, czy ta hipotetyczna rzeczywistości coś odpowiada, i ją w kółko na tyle długo, że myślę, że źle skręciłem. Czy może to być zwykła różnica krotek? $\setminus$

\begin{aligned} \forall A . () ∖ A & = () \\ \forall A . A ∖ () & = A \\ \forall A B C D . A B ∖ C D & = B ∖ D iff A = C \\ otherwise & = undefined \end{aligned}

$\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.)

— Jon Purdy
źródło

How do you use variables in your grammar? This question should help you in handling the "subtyping" you seem to need.

— jmad

@jmad: I’m not sure I understand the question. Type variables are just there for the sake of formally defining type schemes, and the language itself doesn’t have variables at all, just definitions, which can be [mutually] recursive.

— Jon Purdy

Fair enough. Can you say why (perhaps with an example) the rule for compose is too restrictive? I have the impression that this is fine like this. (e.g. the restriction

C = D

$C=D$ could be handled by unification like for application in like in the λ-calculus)

— jmad

@jmad: Sure. Consider twice defined as dup compose apply, which takes a quotation and applies it twice. [1 +] twice is fine: you’re composing two functions of type

ι \to ι

$\iota\to\iota$ . But [pop] twice is not: if

\forall A b . f_{1}, f_{2} : A b \to A

$\forall A b.\:f_1, f_2 : A\:b\to A$ , the problem is that

A \neq A b

$A \neq A\:b$ , so the expression is disallowed even though it ought to be valid and have type

\forall A b . A b b \to A

$\forall A b.\:A\:b\:b\to A$ . The solution is of course to put the qualifier in the right place, but I’m mainly wondering how to actually write the type of compose without some circular definition.

— Jon Purdy

The following rank-2 type

compose : \forall A B C δ . δ (\forall α . α A \to α B) (\forall β . β B \to β C) \to δ (\forall γ . γ A \to γ C)

$\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:

\frac{Γ ⊢ e_{1} : \forall α . α A \to α B Γ ⊢ e_{1} : \forall α . α B \to α C}{Γ ⊢ e_{1} e_{2} : \forall α . α A \to α C}

$\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:

\frac{Γ ⊢ e : \forall α . α A \to α B}{Γ ⊢ e : \forall α . C A \to α C B}

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

— Dave Clarke
źródło

Thanks, this was very helpful. This type is correct for functions of a single argument, but it doesn’t support multiple arguments. For instance, dup + should have type

ι \to ι

$\iota\to\iota$ because + has type

ι ι \to ι

$\iota\:\iota\to\iota$ . But type inference in the absence of annotations is an absolute requirement, so clearly I need to go back to the drawing board. I have an idea for another approach to pursue, though, and will blog about it if it works out.

— Jon Purdy

The stack types quantify over stack fragments, so there is no problem dealing with two argument functions. I'm not sure how this applies to dup +, as that does not use compose, as you defined it above.

— Dave Clarke

Er, right, I meant [dup] [+] compose. But I read

α B

$\alpha\:B$ as

B \times α

$B\times\alpha$ ; say

B = ι \times ι

$B=\iota\times\iota$ ; then you have

(ι \times ι) \times α

$(\iota\times\iota)\times\alpha$ and not

ι \times (ι \times α)

$\iota\times(\iota\times\alpha)$ . The nesting isn’t right, unless you flip the stack around so that the top is the last (deepest nested) element.

— Jon Purdy

I may be building my stack in the wrong direction. I don't think the nesting matters, so long as the pairs building up the stack do not appear in the programming language. (I'm planning to update my answer, but need to do a little research first.)

— Dave Clarke

Yeah, nesting is pretty much an implementation detail.

— Jon Purdy