Вывод типа с типами продукта

Я работаю над компилятором для конкатенативного языка и хотел бы добавить поддержку вывода типов. Я понимаю Хиндли-Милнера, но я изучаю теорию типов по ходу дела, поэтому не знаю, как ее адаптировать. Является ли следующая система надежной и достоверной?

Термин - это литерал, композиция терминов, цитата из термина или примитив.

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

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

Все термины обозначают функции. Для двух функций и , , то есть, сопоставление обозначает обратную композицию. Литералы обозначают ниладические функции. $e_1$ $e_2$ $e_1\:e_2 = e_2 \circ e_1$

Термины, отличные от состава, имеют основные правила типа:

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

Заметно отсутствуют правила для применения, поскольку в конкатенативных языках их нет.

Тип - это литерал, переменная типа или функция из стеков в стеки, где стек определяется как кортеж с правым вложением. Все функции неявно полиморфны по отношению к «остальной части стека».

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

Это первое, что кажется подозрительным, но я не знаю точно, что с ним не так.

Чтобы улучшить читаемость и сократить скобки, я предполагаю, что в схемах типов. Я также буду использовать заглавную букву для переменной, обозначающей стек, а не одно значение. $a\:b = b \times (a)$

Есть шесть примитивов. Первые пять довольно безобидны. dupпринимает верхнее значение и производит две его копии. swapизменяет порядок двух верхних значений. popотбрасывает верхнее значение. quoteпринимает значение и создает цитату (функцию), которая его возвращает. applyприменяет цитату к стеку.

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

Последний комбинатор composeдолжен взять две кавычки и вернуть тип их конкатенации, то есть . В статически типизированном конкатенативном языке Cat этот тип очень прост. $[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)$

Однако этот тип слишком ограничен: он требует, чтобы производство первой функции точно совпадало с потреблением второй. В действительности вы должны принимать разные типы, а затем объединять их. Но как бы вы написали этот тип?

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$

Если вы позволите обозначать разницу двух типов, то я думаю, что вы можете написать тип правильно. $\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))$

Это по - прежнему относительно просто: composeпринимает функцию и один . Его результат потребляет поверх потребления не произведенного , и производит поверх производства не потребленного . Это дает правило для обычного состава. $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]}$

Тем не менее, я не знаю, что этот гипотетический самом деле соответствует чему-либо, и я достаточно долго гонялся за ним по кругу, так что, думаю, я ошибся. Может ли это быть простой разницей в кортежах? $\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}$

Есть ли что-то ужасно сломанное в этом, чего я не вижу, или я нахожусь на чем-то вроде правильного пути? (Я, вероятно, ошибочно определил некоторые из этих вещей, и был бы признателен за исправления в этой области).

programming-languages logic compilers type-theory type-checking Джон Перди
источник

Как вы используете переменные в вашей грамматике? Этот вопрос должен помочь вам разобраться с «подтипом», который вам нужен.

Джмад

@jmad: Я не уверен, что понимаю вопрос. Переменные типа существуют только для формального определения схем типов, а сам язык вообще не имеет переменных, только определения, которые могут быть [взаимно] рекурсивными.

Джон Перди

Справедливо. Можете ли вы сказать, почему (возможно, с примером) правило для composeслишком ограничено? У меня сложилось впечатление, что это хорошо, как это. (например, ограничение может быть обработано объединением, как для применения, как в λ-исчислении)

C = D

$C=D$

jmad

@jmad: конечно. Рассмотрим twiceопределение как dup compose apply, которое берет цитату и применяет ее дважды. [1 +] twiceвсе в порядке: вы составляете две функции типа . Но это не так: если , проблема в том, что , поэтому выражение запрещено, хотя оно должно быть допустимым и иметь типа . Конечно, решение состоит в том, чтобы поместить классификатор в нужное место, но я в основном задаюсь вопросом, как на самом деле написать тип без некоторого циклического определения.

ι \to ι

$\iota\to\iota$ [pop] twice

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

$\forall A b.\:f_1, f_2 : A\:b\to A$

A \neq A b

$A \neq A\:b$

\forall A b . A b b \to A

$\forall A b.\:A\:b\:b\to A$ compose

Джон Пурди

Следующий тип ранга-2 представляется достаточно общим. Это намного более полиморфно, чем тип, предложенный в вопросе. Здесь переменная квантифицируется по непрерывным фрагментам стека, который захватывает функции с несколькими аргументами.

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

Греческие буквы используются для переменных остальной части стека только для ясности.

Он выражает ограничения, что выходной стек первого элемента в стеке должен быть таким же, как входной стек второго элемента. Соответствующее создание экземпляра переменной для двух фактически аргументов - это способ заставить ограничения работать должным образом, а не определять новую операцию, как вы предлагаете в этом вопросе. $B$

Я считаю, что проверка типов типа ранга 2 в общем неразрешима, хотя была проделана некоторая работа, которая дает хорошие результаты на практике (для Haskell):

Саймон Л. Пейтон Джонс, Димитриос Витиниотис, Стефани Вейрих, Марк Шилдс: Практический вывод типов для типов произвольного ранга. J. Funct. Программа. 17 (1): 1-82 (2007)

Правило типа для композиции просто:

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

Чтобы система типов работала в целом, вам нужно следующее правило специализации:

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

Дэйв Кларк
источник

Спасибо, это было очень полезно. Этот тип подходит для функций с одним аргументом, но он не поддерживает несколько аргументов. Например, dup +должен иметь тип потому что имеет тип . Но вывод типа при отсутствии аннотаций является абсолютным требованием, поэтому ясно, что мне нужно вернуться к чертежной доске. У меня есть идея для другого подхода, и я буду писать об этом, если это сработает.

ι \to ι

$\iota\to\iota$ +

ι ι \to ι

$\iota\:\iota\to\iota$

Джон Перди

Типы стека количественно определяют фрагменты стека, поэтому проблем с двумя аргументами не возникает. Я не уверен, как это относится dup +, так как это не использует compose, как вы определили это выше.

Дэйв Кларк

Э, верно, я имел в виду [dup] [+] compose. Но я читаю как ; сказать ; тогда у вас есть а не . Вложение не является правильным, если вы не переверните стек так, чтобы верх был последним (самым глубоким вложенным) элементом.

α B

$\alpha\:B$

B \times α

$B\times\alpha$

B = ι \times ι

$B=\iota\times\iota$

(ι \times ι) \times α

$(\iota\times\iota)\times\alpha$

ι \times (ι \times α)

$\iota\times(\iota\times\alpha)$

Джон Перди

Возможно, я строю свой стек в неправильном направлении. Я не думаю, что вложенность имеет значение, пока пары, составляющие стек, не появляются в языке программирования. (Я планирую обновить свой ответ, но сначала нужно провести небольшое исследование.)

Дэйв Кларк

Да, вложение - это в значительной степени деталь реализации.

Джон Перди

Вывод типа с типами продукта

Ответы: