Периодически на хабре можно встретить статьи о том, какие невероятные вещи можно сделать на шаблонах C++: конечные автоматы, лямбда-исчисление, машина Тьюринга и многое другое.


Параметризованные типы в Java традиционно считаются лишь пародией на шаблоны C++ (несмотря на то, что их даже сравнивать как-то некорректно), и причины этого несложно понять. Тем не менее не всё так плохо, и компилятор Java можно заставить производить во время проверки типов любые вычисления, лишь бы хватило оперативной памяти. Конкретный способ это сделать был описан в ноябре 2016-го года в этой прекрасной публикации. Его я и хотел бы объяснить.


Для затравки приведу следующий код. Корректен ли он? Предлагаю скомпилировать и проверить, угадали ли вы результат.


class Sample {

    interface BadList<T> extends List<List<? super BadList<? super T>>> {}

    public static void main(String[] args) {
        BadList<? super String> badList = null;
        List<? super BadList<? super String>> list = badList;
    }
}

Узнать ответ

Компилятор выбросит java.lang.StackOverflowError независимо от размера стэка.


Разберёмся, почему компилятор ведёт себя именно так (я бы не назвал это багом), как понимание данных причин может быть полезно и причём тут машина Тьюринга.




1. О ковариантности и контравариантности


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


List<Integer> integerList = new ArrayList<>();
List<Number> numberList = new ArrayList<>();

Обычно подобного хватает, но есть проблема — тип элементов жёстко зафиксирован. У нас нет возможности использовать объект integerList там, где нужен List<Number>, поскольку вставка в такой список элемента типа Double сломала бы его целостность. И наоборот, нельзя использовать numberList там, где ожидается List<Integer>, поскольку это приведёт к ClassCastException при чтении элементов списка в случае, если в нём попадутся не целые числа. Конечно, для решения второй проблемы можно использовать такую маленькую хитрость:


<T extends Number> Number firstNum(List<T> xs) {
    return xs.get(0);
}

Я называю это хитростью, потому что такой подход требует введения дополнительного типа T. Более того, проблему вставки подобным способом не решить в принципе. Альтернативный и, на мой взгляд, более правильный вариант этого метода должен выглядеть так:


Number firstNum(List<? extends Number> xs) {
    return xs.get(0);
}

Говорят, что такие типы ковариантны своим параметрам. Это значит, что если A является подтипом B, то List<A> (как и List<? extends A>) является подтипом List<? extends B>, а значит между ними разрешено присваивание. Побочный эффект — такой список будет доступен только для чтения и целостность никаких объектов мы нарушить не сможем.
Для случая записи есть другая конструкция:


void addOne(List<? super Integer> xs) {
    xs.add(1);
}

List<? super Integer> описывает совокупность списков, в которые можно добавлять целые числа, то есть его подтипами являются List<Integer>, List<Number> и List<Object> (плюс List<? super Integer>, List<? super Number> и List<? super Object> соответственно). Подобные классы контравариантны своим параметрам, то есть если A является супертипом B, то List<A> является подтипом List<? super B>. Ситуация прямо противоположная ковариантному случаю.


Сосредоточимся на контравариантных типах.




2. Формализация подмножества контравариантных типов


Итак, определим, какие именно типы в Java нас интересуют. Введём понятие индуктивно:


  • параметр типа t — это тип;
  • если C — это класс с одним параметром и t — это тип, то запись $Ct$ — это тоже тип. Обозначать он будет сокращение для такой записи: C<? super t>.

Более сложные типы будут записываться как $C_1C_2...C_nt$, что соответствует такому коду:
C1<? super C2<? super ...Cn<? super t>...>>


Определим отношение наследования. Итак, пусть есть тип
interface C<T> extends C1<C2<? super ...Cn<? super t>...>>, в таком случае будем говорить, что для любого типа или класса без параметров X выполнено следующее отношение наследования: $CX<::C_1C_2...C_nX$. Символом $<::^*$ обозначим транзитивное замыкание отношения $<::$ (то есть, помимо прямого, ещё и косвенное наследование через цепочку классов).
У отношения $<::^*$ есть одно полезное свойство — ацикличность. Так как в Java нет множественного наследования, то мы можем заявлять, что:


  • если $t<::^*Cu$ и $t<::^*Cu'$, то $u=u'$;
  • в частности, если $Cu<::^*Cu'$, то $u=u'$.

Теперь можно наконец ввести отношение является подтипом "$<:$".


  1. Для любого типа T считаем, что он является собственным подтипом: $T <: T$.
  2. Если выполнено отношение наследования $CT_1<::^*C_1C_2...C_nT_1$ и известно, что $T_2<:T_1$, то выполняется $CT_1<:C_1C_2...C_nT_2$ (я не ошибся с порядком $T_1$ и $T_2$, это всё контравариантность).

В этом месте появляется существенное ограничение. Чтобы отношение $<:$ совпадало со стандартным способом определения подтипов в Java, необходимо, чтобы в пункте 2 значение n было нечётным.


Почему должно быть именно так

Полного формального доказательства я приводить не буду, оно было бы неуместно длинным. Правильнее будет рассмотреть ситуацию на примерах.


n=1:
interface S<T> extends C<T> {}
В данном случае не вызывает вопросов то, что S<? super X> является подтипом C<? super X>, поскольку это является прямой подстановкой параметра T.


n=3:
interface S<T> extends C1<C2<C3<? super T>>> {}
Докажем, что верно $SX <: C_1C_2C_3X$:


  • возьмём тип $Z$ такой, что $X<:Z$;
  • из этого следует, что $C_3Z<:C_3X$;
  • следовательно $C_2C_3X<:C_2C_3Z$;
  • следовательно $C_1C_2C_3Z<:C_1C_2C_3X$;
  • так как C1<C2<? super C3<? super Z>>> это подтип $C_1C_2C_3Z$, то он является и подтипом $C_1C_2C_3X$;
  • а это означает, что и S<Z> является подтипом $C_1C_2C_3X$;
  • если в качестве Z рассмотреть Capture#1 of (? super X), то мы получаем истинность $SX <: C_1C_2C_3X$. Такой вывод справедлив благодаря JLS 4.10.2, цитирую:
    Given a generic type declaration $C<F_1,..., F_n>$ (n > 0), the direct supertypes of the parameterized type $C<R_1,..., R_n>$ where at least one of the $R_i (1\leq i\leq n)$ is a wildcard type argument, are the direct supertypes of the parameterized type $C<X_1,..., X_n>$ which is the result of applying capture conversion to $C<R_1,..., R_n>$ (§5.1.10)

n=2:
interface S<T> extends C1<C2<? super T>> {}
Предположим, что $SX <: C_1C_2X$:


  • в таком случае существует тип Z = Capture of (? super X) (т.е. $X<:Z$) такой, что S<Z> является подтипом $C_1C_2X$;
  • данное место может показаться спорным. Я утверждаю, что поскольку S<Z> является подтипом C1<C2<? super Z>>, то C1<C2<? super Z>> тоже является подтипом $C_1C_2X$;
  • из предыдущего пункта следует, что $C_2X<:C_2Z$;
  • следовательно $Z<:X$, что точно не является правдой. Мы пришли к противоречию.

Случаи n>2 рассматриваются аналогичным образом.


Теперь можно сформулировать следующую теорему, которая позже будет доказана:


Теорема 1
Не существует алгоритма, который для любых двух заданных типов $T_1$ и $T_2$ смог бы определить, является ли верным высказывание $T_1<:T_2$.

Другими словами, в общем случае в Java невозможно определить, является ли один тип подтипом другого.




3. Что будем понимать под машиной Тьюринга


Машина Тьюринга $\tau$ — это пятёрка $(Q, q_I, q_H, \Sigma, \delta)$, где $Q$ — это конечное множество состояний, $q_I\in Q$ — это начальное состояние, $q_H\in Q$ — это конечное состояние, $\Sigma$ — это конечный алфавит и $\delta:Q\times\Sigma_\bot\rightarrow Q\times\Sigma\times\{\bf{L}, \bf{S}, \bf{R}\}$ — это функция перехода. $\bot$ — это дополнительный символ, не содержащийся в $\Sigma$.


Конфигурация машины Тьюринга — это четвёрка $(q, \alpha, b, \gamma)$, в которой $q\in Q$ — это текущее состояние, $\alpha\in\Sigma^*$ — это левая часть ленты, $b\in\Sigma_\bot$ — это текущий символ и $\gamma\in\Sigma^*$ — это правая часть ленты.


Шаг выполнения машины $\tau$ отображает множество конфигураций само в себя следующим образом:


  • $(q, \alpha a, b, \gamma)\rightarrow(q', \alpha, a, b'\gamma)$ для $\delta(q, b) = (q', b', \bf{L})$;
  • $(q, \alpha, b, \gamma)\rightarrow(q', \alpha, b', \gamma)$ для $\delta(q, b) = (q', b', \bf{S})$;
  • $(q, \alpha, b, c\gamma)\rightarrow(q', \alpha b', c, \gamma)$ для $\delta(q, b) = (q', b', \bf{R})$.

Так же учитываются граничные случаи (символ $\epsilon$ здесь означает пустую строку). Они показывают, что по достижении конца строки (слева или справа) к ней автоматически дописывается символ $\bot$:


  • $(q, \epsilon, b, \gamma)\rightarrow(q', \epsilon, \bot, b'\gamma)$ для $\delta(q, b) = (q', b', \bf{L})$;
  • $(q, \alpha, b, \epsilon)\rightarrow(q', \alpha b', \bot, \epsilon)$ для $\delta(q, b) = (q', b', \bf{R})$.

Запуск машины на входе $\alpha_I$ — это последовательность шагов выполнения, начинающаяся с конфигурации $(q_I, \epsilon, \bot, \alpha_I)$. Если $\tau$ достигает $q_H$, то мы говорим, что машина $\tau$ завершается (halts) на входе $\alpha_I$. Если же функция перехода не позволяет сделать следующий шаг выполнения, будем считать, что машина $\tau$ ломается на входе $\alpha_I$.




4. Subtyping Machines


Начнём связывать воедино имеющиеся у нас понятия. Цель — сопоставить шаги выполнения машины Тьюринга с процессом проверки типов в Java. Положим, что у нас есть такой запрос:

$C_1C_2...C_mZ<:D_1D_2...D_nZ$


Это утверждение, истинность или ложность которого предлагается доказать. Для удобства введём две альтернативные формы записи:

$\begin{array}{ll} &ZC_mC_{m-1}...C_1\blacktriangleleft D_1D_2...D_nZ\\ =&ZD_nD_{n-1}...D_1\blacktriangleright C_1C_2...C_mZ\\ \end{array}$


Введём два вида правил выполнения $\cdot\rightsquigarrow\cdot$ для наших машин:
  • $(ZC_m...C_1\blacktriangleleft Z)\rightsquigarrow\bullet$, если $C_1...C_mZ<::^*Z$;
  • $(ZC_m...C_1\blacktriangleleft D_1...D_nZ)\rightsquigarrow(ZE_p...E_2\blacktriangleright D_2...D_nZ)$, если $C_1...C_mZ<::^*D_1E_2...E_pZ$.

$\bullet$ — это специальная конфигурация, называемая завершающей (halting).
Отметим, что имея правило наследования $C_1t<::D_1E_2...E_pt$ и подставляя тип $t:=C_2...C_mZ$, мы получаем следующее правило выполнения:

$\begin{array}{ll} &ZC_m...C_2C_1\blacktriangleleft D_1D_2...D_nZ\\ \rightsquigarrow&ZC_m...C_2E_p...E_2\blacktriangleright D_2...D_nZ\\ \end{array}$


Так же в силу контравариантности используемых типов справедливо такое правило:

$\begin{array}{ll} &ZC_m...C_1N\blacktriangleleft ND_1...D_nZ\\ \rightsquigarrow&ZC_m...C_1\blacktriangleright D_1...D_nZ\\ \end{array}$


Используя введённые правила, можно понять, что происходит при проверке типов в примере из начала статьи (они полностью соответствуют алгоритму проверки типов Java на выделенном нами подмножестве контравариантных типов). В нём задано отношение наследования $BadList\;t<::List\;List\;BadList\;t$ и запрос $BadList\;String<:List\;BadList\;String$.
Цепочка правил выполнения будет следующей:

$\begin{array}{ll} &String\;BadList\blacktriangleleft List\;BadList\;String\\ \rightsquigarrow&String\;BadList\;List\;List\blacktriangleleft List\;BadList\;String\\ \rightsquigarrow&String\;BadList\;List\blacktriangleright BadList\;String\\ \rightsquigarrow&String\;BadList\;List\blacktriangleright List\;List\;BadList\;String\\ \rightsquigarrow&String\;BadList\blacktriangleleft List\;BadList\;String\\ \rightsquigarrow&... \end{array}$


Как видно, проверка типов зацикливается, этим и обусловлено переполнение стэка во время компиляции. В общем виде описанный процесс можно выразить таким образом:
Выражение $C_1...C_mZ<:D_1...D_nZ$ истинно тогда и только тогда, когда существует завершающийся процесс выполнения $(ZC_m...C_1\blacktriangleleft D_1...D_nZ)\rightsquigarrow^*\bullet$.

Пример посложнее


Рассмотрим следующую таблицу классов:


$\begin{array}{rllrll} Q^Lt&<::&LNQ^LLNt&Q^Rt&<::&LNQ^RLNt\\ Q^Lt&<::&EQ^{LR}Nt&Q^Rt&<::&EQ^{RL}Nt\\ Et&<::&Q^{LR}NQ^REEt&Et&<::&Q^{RL}NQ^LEEt\\ \end{array}$


Соответствующий исходный код
interface N<T> {}
interface L<T> {}

interface QLR<T> {}
interface QRL<T> {}

interface E<T> extends
          QLR<N<? super QR<? super E<? super E<? super T>>>>>,
          QRL<N<? super QL<? super E<? super E<? super T>>>>> {}
interface QL<T> extends
          L<N<? super QL<? super L<? super N<? super T>>>>>,
          E<QLR<? super N<? super T>>> {}
interface QR<T> extends
          L<N<? super QR<? super L<? super N<? super T>>>>>,
          E<QRL<? super N<? super T>>> {}

Проследим за выполнением машины на входе $Q_REEZ<:LNLNEEZ$ (сокращённый вариант):

$\begin{array}{ll} &ZEEQ^R\blacktriangleleft LNLNEEZ\\ \rightsquigarrow&ZEENLQ^R\blacktriangleleft LNEEZ\\ \rightsquigarrow&ZEENLNLQ^R\blacktriangleleft EEZ\\ \rightsquigarrow&ZEENLNLNQ^{RL}\blacktriangleright EZ\\ \rightsquigarrow&ZEENLNL\blacktriangleright Q^LEEZ\\ \rightsquigarrow&ZEENL\blacktriangleright Q^LLNEEZ\\ \rightsquigarrow&ZEE\blacktriangleright Q^LLNLNEEZ\\ \rightsquigarrow&ZE\blacktriangleleft Q^{LR}NLNLNEEZ\\ \rightsquigarrow&ZEEQ^R\blacktriangleleft LNLNEEZ\\ \rightsquigarrow&...\\ \end{array}$


Подробный вариант

$\begin{array}{lll} &ZEEQ^R\blacktriangleleft LNLNEEZ\\ \rightsquigarrow&ZEENLQ^RNL\blacktriangleleft LNLNEEZ&(Q^Rt<:LNQ^RLNt)\\ \rightsquigarrow&ZEENLQ^RN\blacktriangleright NLNEEZ\\ \rightsquigarrow&ZEENLQ^R\blacktriangleleft LNEEZ\\ \rightsquigarrow&ZEENLNLQ^RNL\blacktriangleleft LNEEZ&(Q^Rt<:LNQ^RLNt)\\ \rightsquigarrow&ZEENLNLQ^RN\blacktriangleright NEEZ\\ \rightsquigarrow&ZEENLNLQ^R\blacktriangleleft EEZ\\ \rightsquigarrow&ZEENLNLNQ^{RL}E\blacktriangleleft EEZ&(Q^Rt<:EQ^{RL}Nt)\\ \rightsquigarrow&ZEENLNLNQ^{RL}\blacktriangleright EZ\\ \rightsquigarrow&ZEENLNLNQ^{RL}\blacktriangleright Q^{RL}NQ^LEEZ&(Et<:Q^{RL}NQ^LEEt)\\ \rightsquigarrow&ZEENLNLN\blacktriangleleft NQ^LEEZ\\ \rightsquigarrow&ZEENLNL\blacktriangleright Q^LEEZ\\ \rightsquigarrow&ZEENLNL\blacktriangleright LNQ^LLNEEZ&(Q^Lt<:LNQ^LLNt)\\ \rightsquigarrow&ZEENLN\blacktriangleleft NQ^LLNEEZ\\ \rightsquigarrow&ZEENL\blacktriangleright Q^LLNEEZ\\ \rightsquigarrow&ZEENL\blacktriangleright LNQ^LLNLNEEZ&(Q^Lt<:LNQ^LLNt)\\ \rightsquigarrow&ZEEN\blacktriangleleft NQ^LLNLNEEZ\\ \rightsquigarrow&ZEE\blacktriangleright Q^LLNLNEEZ\\ \rightsquigarrow&ZEE\blacktriangleright EQ^{LR}NLNLNEEZ&(Q^Lt<:EQ^{LR}Nt)\\ \rightsquigarrow&ZE\blacktriangleleft Q^{LR}NLNLNEEZ\\ \rightsquigarrow&ZEEQ^RNQ^{LR}\blacktriangleleft Q^{LR}NLNLNEEZ&(Et<:Q^{LR}NQ^REEt)\\ \rightsquigarrow&ZEEQ^RN\blacktriangleright NLNLNEEZ\\ \rightsquigarrow&ZEEQ^R\blacktriangleleft LNLNEEZ\\ \rightsquigarrow&...\\ \end{array}$


Данный запрос тоже приводит к зацикливанию проверки типов, но теперь это уже нетривиальный цикл. Мы реализовали полноценное блуждание "треугольника" в обе стороны по нашей импровизированной ленте. Убедиться, что проверка типов зацикливается, можно на следующем коде:


interface Z {}

class Main {
    L<? super N<? super L<? super N<? super E<? super E<? super Z>>>>>>
    doit(QR<? super E<? super E<? super Z>>> v) {
        return v;
    }
}



5. Построение машины Тьюринга


Имея машину Тьюринга $\tau$ и входную ленту $\alpha_I$, построим типы $t_1$ и $t_2$ таким образом, что $t_1<:t_2$ тогда и только тогда, когда $\tau$ останавливается на входе $\alpha_I$.
Для каждого состояния $q_s\in Q$ введём 6 классов: $Q_s^{wL}$, $Q_s^{wR}$, $Q_s^L$, $Q_s^R$, $Q_s^{LR}$ и $Q_s^{RL}$; для каждого символа $a\in\Sigma$ построим класс $L_a$. Символ $\bot$ из определения машины Тьюринга для удобства будем записывать как $\#$, ему будет соответствовать класс $L_\#$. Так же дополнительно введём 4 класса: $N$, $E$, $M^L$ и $M^R$.


Выглядит немного похоже на последний пример. Дальше будет примерное описание их смысла и конкретный способ эмуляции функции перехода соответствующей машины Тьюринга.


  • $Q_s^{wL}$ и $Q_s^{wR}$ — это по сути типы $Q^L$ и $Q^R$ из последнего примера. Большую часть времени они блуждают (wander) вдоль ленты. Смысл типов $Q_s^{LR}$ и $Q_s^{RL}$ тоже сохраняется: они нужны для разворота на конце ленты. Единственное исключение — момент, когда $Q_s^{wX}$ ($X$ это $L$ или $R$) встречается с соответствующим ему $M^X$: он при этом "превращается" в $Q^X$. $Q_H^{wX}$ — класс для завершающего состояния, обрабатываемый особым образом.
    Полное описание выглядит так:


    $\begin{array}{rllrlll} Q_s^{wL}t&<::&L_aNQ_s^{wL}L_aNt&Q_s^{wR}t&<::&L_aNQ_s^{wR}L_aNt&\forall q_s\in Q, a\in\Sigma\cup\{\#\}\\ Q_s^{wL}t&<::&M^RNQ_s^{wL}M^RNt&Q_s^{wR}t&<::&M^LNQ_s^{wR}M^LNt&\forall q_s\in Q\\ Q_s^{wL}t&<::&M^LNQ_s^Lt&Q_s^{wR}t&<::&M^RNQ_s^Rt&\forall q_s\in Q\\ Q_s^{wL}t&<::&EQ_s^{LR}Nt&Q_s^{wR}t&<::&EQ_s^{RL}Nt&\forall q_s\in Q\setminus\{q_H\}\\ Q_H^{wL}t&<::&EEZ&Q_H^{wR}t&<::&EEZ\\ Et&<::&Q_s^{LR}NQ_s^{wR}EEt&Et&<::&Q_s^{RL}NQ_s^{wL}EEt&\forall q_s\in Q\\ \end{array}$


  • $Q_s^{L}$ и $Q_s^{R}$ указывают машине, что пришло время для очередного шага выполнения. Соответственно, для каждого правила $\delta(q_1,a_1)\rightarrow(q_2,a_2,\bf{X})$ в машине Тьюринга $\tau$ мы строим специальное отношение наследования. При этом не забываем об особых правилах работы с классом $L_\#$:


    $\begin{array}{rlll} Q_s^{R}t&<::&L_aNQ_{s'}^{wR}L_bNM^LNt&\forall (q_s, a)\rightarrow(q_{s'}, b, \bf{L})\\ Q_s^{R}t&<::&L_aNQ_{s'}^{wR}M^LNL_bNt&\forall(q_s, a)\rightarrow(q_{s'}, b, \bf{S})\\ Q_s^{R}t&<::&L_aNQ_{s'}^{wR}M^RNL_bNt&\forall(q_s, a)\rightarrow(q_{s'}, b, \bf{R})\\ Q_s^{R}t&<::&L_\#NQ_{s'}^{wR}L_\#NL_bNM^LNt&\forall(q_s, \bot)\rightarrow(q_{s'}, b, \bf{L})\\ Q_s^{R}t&<::&L_\#NQ_{s'}^{wR}L_\#NM^LNL_bNt&\forall(q_s, \bot)\rightarrow(q_{s'}, b, \bf{S})\\ Q_s^{R}t&<::&L_\#NQ_{s'}^{wR}L_\#NM^RNL_bNt&\forall(q_s, \bot)\rightarrow(q_{s'}, b, \bf{R})\\ \end{array}$


    $\begin{array}{rlll} Q_s^{L}t&<::&L_aNQ_{s'}^{wL}M^LNL_bNt&\forall (q_s, a)\rightarrow(q_{s'}, b, \bf{L})\\ Q_s^{L}t&<::&L_aNQ_{s'}^{wL}M^RNL_bNt&\forall(q_s, a)\rightarrow(q_{s'}, b, \bf{S})\\ Q_s^{L}t&<::&L_aNQ_{s'}^{wL}L_bNM^RNt&\forall(q_s, a)\rightarrow(q_{s'}, b, \bf{R})\\ Q_s^{L}t&<::&L_\#NQ_{s'}^{wL}L_\#NM^LNL_bNt&\forall(q_s, \bot)\rightarrow(q_{s'}, b, \bf{L})\\ Q_s^{L}t&<::&L_\#NQ_{s'}^{wL}L_\#NM^RNL_bNt&\forall(q_s, \bot)\rightarrow(q_{s'}, b, \bf{S})\\ Q_s^{L}t&<::&L_\#NQ_{s'}^{wL}L_\#NL_bNM^RNt&\forall(q_s, \bot)\rightarrow(q_{s'}, b, \bf{R})\\ \end{array}$


    Данные отношения выглядят довольно-таки хитро, тем не менее в них можно проследить ряд закономерностей. Механику работы каждого я разбирать не буду, рассмотрим лишь часть.
    $(q_s, a)\rightarrow(q_{s'}, x, \bf{R})$:


    $\begin{array}{ll} &...Q_s^R\blacktriangleleft L_aNL_bN...\\ \rightsquigarrow&...NL_xNM^RQ_{s'}^{wR}\blacktriangleleft L_bN...\\ \rightsquigarrow&...wandering...\\ \rightsquigarrow&...NL_xQ_{s'}^{wR}\blacktriangleleft M^RNL_bN...\\ \rightsquigarrow&...NL_xQ_{s'}^{R}\blacktriangleleft L_bN...\\ \rightsquigarrow&...\\ \end{array}$


    $(q_s, a)\rightarrow(q_{s'}, x, \bf{S})$:


    $\begin{array}{ll} &...Q_s^R\blacktriangleleft L_aNL_bN...\\ \rightsquigarrow&...NL_xNM^LQ_{s'}^{wR}\blacktriangleleft L_bN...\\ \rightsquigarrow&...wandering...\\ \rightsquigarrow&...NL_xNM^L\blacktriangleright Q_{s'}^{wL}L_bN...\\ \rightsquigarrow&...NL_x\blacktriangleright Q_{s'}^{L}L_bN...\\ \rightsquigarrow&...\\ \end{array}$


    $(q_s, a)\rightarrow(q_{s'}, x, \bf{L})$:


    $\begin{array}{ll} &...NL_bQ_s^R\blacktriangleleft L_aNL_yN...\\ \rightsquigarrow&...NL_bNM^LNL_xQ_{s'}^{wR}\blacktriangleleft L_yN...\\ \rightsquigarrow&...wandering...\\ \rightsquigarrow&...NL_bNM^L\blacktriangleright Q_{s'}^{wL}L_xNL_yN...\\ \rightsquigarrow&...NL_b\blacktriangleright Q_{s'}^{L}L_xNL_yN...\\ \rightsquigarrow&...\\ \end{array}$


    Остальные 9 случаев расписываются аналогичным образом.



6. Fluent interface


Вернёмся в реальный мир. Мы же про Java говорим, а значит наши рассуждения должны в итоге привести к написанию какого-либо кода, желательно полезного.
В мире ООП есть такое понятие, как текучий интерфейс. Вы, возможно, никогда не встречали этого названия, но наверняка видели его реализацию в коде. По сути это просто каскадный вызов методов, использование которого нацелено на повышение читаемости, ну или ещё чего нибудь. Выглядит вот так:


String s = new StringBuilder(a)
        .append(b)
        .append(c)
        .toString();

На подобную цепочку вызовов можно взглянуть новым образом — как на слово. В данном примере мы имеем алфавит {append, toString} и слово append append toString.
Предположим, что мы хотим попросить компилятор Java валидировать нашу цепочку вызовов, проверяя, принадлежит ли соответствующее слово заранее определённой грамматике. Например, не допускать слова длиной более 10 символов. Понятно, что для класса StringBuilder ничего подобного сделать уже не выйдет, зато можно попробовать для своих собственных интерфейсов.


Пусть, для примера, мы хотим валидировать цепочки вызовов методов a, b и c. Так же пусть у нас есть машина Тьюринга, которая умеет валидировать слова соответствующего языка (subtyping machine со всеми её интерфейсами прилагается).
Наша цель — сделать так, чтобы для цепочки вызовов a().b().c() компилятор запускал такой запрос: $ZEENL_\#NM^LNL_aNL_bNL_cNL_\#Q_I^{wR}\blacktriangleleft EEZ$.


Для этого напишем следующий класс:


abstract class B<T> {
    static B<ML<? super N<? super
                LHash<? super N<? super
                E<? super E<? super Z>>>>>>> start;
    abstract QWRStart<? super LHash<? super N<? super T>>> stop();
    abstract B<La<? super N<? super T>>> a();
    abstract B<Lb<? super N<? super T>>> b();
    abstract B<Lc<? super N<? super T>>> c();
}

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


Если приглядеться, то можно заметить, что тип выражения B.start.a().b().c().stop, записываемый таким образом:


QWRStart<? super LHash<? super N<? super
         Lc<? super N<? super Lb<? super N<? super La<? super N<? super
         ML<? super N<? super LHash<? super N<? super
         E<? super E<? super Z>>>>>>>>>>>>>>>

полностью повторяет левую часть требуемого запроса. То есть, следующая строка кода на самом деле запустит требуемую машину Тьюринга во время работы алгоритма проверки типов:


E<? super E<? super Z>> res = B.start.a().b().c().stop;



7. Безопасный Builder


Добрались! Имея такой богатый инструментарий, пришло время создать что-нибудь внятное.
Помнится, прочитав эту статью, я подумал: "Интересная идея!". Так вот, сейчас моя очередь делать безопасный Builder. Внешний вид класса B из предыдущей части диктует некоторые ограничение, поэтому мой Builder будет чуть-чуть многословный.


Итак, я хочу иметь следующий код, который мог бы валидироваться компилятором:


User user = build(user()
        .withFirstName("John")
        .withLastName("Doe")
        .please()
);

Требования будут самыми простыми — чтобы оба поля были инициализированы, причём именно в таком порядке и не больше одного раза (я прекрасно понимаю, что такую простую задачу можно решить более подходящими методами; пример с грамматикой посложнее будет позже).


Машина Тьюринга для такого случая будет весьма простой. В ней всего 5 состояний: Start, First, Last, Finish и Halt. Алфавит будет содержать 3 символа: FirstName, LastName и Hash.
Функция перехода выглядит следующим образом:


$(Start, Hash)\rightarrow(First, Hash, \bf{R})$
$(First, FirstName)\rightarrow(Last, FirstName, \bf{R})$
$(Last, LastName)\rightarrow(Finish, LastName, \bf{R})$
$(Finish, Hash)\rightarrow(Halt, Hash, \bf{R})$


Довольно-таки прямолинейно. Машина остановится только на входе $FirstName, LastName$.


Исходный код, описывающий эту машину (будет лежать внутри UserBuilder)
public interface N<X> {}
public interface ML<X> {}
public interface MR<X> {}

public interface LFirstName<X> {}
public interface LLastName<X> {}
public interface LHash<X> {}

public interface E<X> extends
        QLRStart<N<? super QWRStart<? super E<? super E<? super X>>>>>,
        QRLStart<N<? super QWLStart<? super E<? super E<? super X>>>>>,
        QLRFirst<N<? super QWRFirst<? super E<? super E<? super X>>>>>,
        QRLFirst<N<? super QWLFirst<? super E<? super E<? super X>>>>>,
        QLRLast<N<? super QWRLast<? super E<? super E<? super X>>>>>,
        QRLLast<N<? super QWLLast<? super E<? super E<? super X>>>>>,
        QLRFinish<N<? super QWRFinish<? super E<? super E<? super X>>>>>,
        QRLFinish<N<? super QWLFinish<? super E<? super E<? super X>>>>>,
        QLRHalt<N<? super QWRHalt<? super E<? super E<? super X>>>>>,
        QRLHalt<N<? super QWLHalt<? super E<? super E<? super X>>>>> {}

public interface QLRStart<X> {}
public interface QWLStart<X> extends
        ML<N<? super QLStart<? super X>>>,
        MR<N<? super QWLStart<? super MR<? super N<? super X>>>>>,
        LFirstName<N<? super QWLStart<? super LFirstName<? super
                N<? super X>>>>>,
        LLastName<N<? super QWLStart<? super LLastName<? super
                N<? super X>>>>>,
        LHash<N<? super QWLStart<? super LHash<? super N<? super X>>>>>,
        E<QLRStart<? super N<? super X>>> {}

public interface QRLStart<X> {}
public interface QWRStart<X> extends
        MR<N<? super QRStart<? super X>>>,
        ML<N<? super QWRStart<? super ML<? super N<? super X>>>>>,
        LFirstName<N<? super QWRStart<? super LFirstName<? super
                N<? super X>>>>>,
        LLastName<N<? super QWRStart<? super LLastName<? super
                N<? super X>>>>>,
        LHash<N<? super QWRStart<? super LHash<? super N<? super X>>>>>,
        E<QRLStart<? super N<? super X>>> {}

public interface QLRFirst<X> {}
public interface QWLFirst<X> extends
        ML<N<? super QLFirst<? super X>>>,
        MR<N<? super QWLFirst<? super MR<? super N<? super X>>>>>,
        LFirstName<N<? super QWLFirst<? super LFirstName<? super
                N<? super X>>>>>,
        LLastName<N<? super QWLFirst<? super LLastName<? super
                N<? super X>>>>>,
        LHash<N<? super QWLFirst<? super LHash<? super N<? super X>>>>>,
        E<QLRFirst<? super N<? super X>>> {}

public interface QRLFirst<X> {}
public interface QWRFirst<X> extends
        MR<N<? super QRFirst<? super X>>>,
        ML<N<? super QWRFirst<? super ML<? super N<? super X>>>>>,
        LFirstName<N<? super QWRFirst<? super LFirstName<? super
                N<? super X>>>>>,
        LLastName<N<? super QWRFirst<? super LLastName<? super
                N<? super X>>>>>,
        LHash<N<? super QWRFirst<? super LHash<? super N<? super X>>>>>,
        E<QRLFirst<? super N<? super X>>> {}

public interface QLRLast<X> {}
public interface QWLLast<X> extends
        ML<N<? super QLLast<? super X>>>,
        MR<N<? super QWLLast<? super MR<? super N<? super X>>>>>,
        LFirstName<N<? super QWLLast<? super LFirstName<? super
                N<? super X>>>>>,
        LLastName<N<? super QWLLast<? super LLastName<? super
                N<? super X>>>>>,
        LHash<N<? super QWLLast<? super LHash<? super N<? super X>>>>>,
        E<QLRLast<? super N<? super X>>> {}

public interface QRLLast<X> {}
public interface QWRLast<X> extends
        MR<N<? super QRLast<? super X>>>,
        ML<N<? super QWRLast<? super ML<? super N<? super X>>>>>,
        LFirstName<N<? super QWRLast<? super LFirstName<? super
                N<? super X>>>>>,
        LLastName<N<? super QWRLast<? super LLastName<? super
                N<? super X>>>>>,
        LHash<N<? super QWRLast<? super LHash<? super N<? super X>>>>>,
        E<QRLLast<? super N<? super X>>> {}

public interface QLRFinish<X> {}
public interface QWLFinish<X> extends
        ML<N<? super QLFinish<? super X>>>,
        MR<N<? super QWLFinish<? super MR<? super N<? super X>>>>>,
        LFirstName<N<? super QWLFinish<? super LFirstName<? super
                N<? super X>>>>>,
        LLastName<N<? super QWLFinish<? super LLastName<? super
                N<? super X>>>>>,
        LHash<N<? super QWLFinish<? super LHash<? super N<? super X>>>>>,
        E<QLRFinish<? super N<? super X>>> {}

public interface QRLFinish<X> {}
public interface QWRFinish<X> extends
        MR<N<? super QRFinish<? super X>>>,
        ML<N<? super QWRFinish<? super ML<? super N<? super X>>>>>,
        LFirstName<N<? super QWRFinish<? super LFirstName<? super
                N<? super X>>>>>,
        LLastName<N<? super QWRFinish<? super LLastName<? super
                N<? super X>>>>>,
        LHash<N<? super QWRFinish<? super LHash<? super N<? super X>>>>>,
        E<QRLFinish<? super N<? super X>>> {}

public interface QLRHalt<X> {}
public interface QWLHalt<X> extends
        ML<N<? super QLHalt<? super X>>>,
        MR<N<? super QWLHalt<? super MR<? super N<? super X>>>>>,
        LFirstName<N<? super QWLHalt<? super LFirstName<? super
                N<? super X>>>>>,
        LLastName<N<? super QWLHalt<? super LLastName<? super
                N<? super X>>>>>,
        LHash<N<? super QWLHalt<? super LHash<? super N<? super X>>>>>,
        E<E<? super User>> {}

public interface QRLHalt<X> {}
public interface QWRHalt<X> extends
        MR<N<? super QRHalt<? super X>>>,
        ML<N<? super QWRHalt<? super ML<? super N<? super X>>>>>,
        LFirstName<N<? super QWRHalt<? super LFirstName<? super
                N<? super X>>>>>,
        LLastName<N<? super QWRHalt<? super LLastName<? super
                N<? super X>>>>>,
        LHash<N<? super QWRHalt<? super LHash<? super N<? super X>>>>>,
        E<E<? super User>> {}

public interface QLStart<X> extends
        LHash<N<? super QWLFirst<? super LHash<? super N<? super
                LHash<? super N<? super MR<? super N<? super X>>>>>>>>> {}
public interface QRStart<X> extends
        LHash<N<? super QWRFirst<? super LHash<? super N<? super
                MR<? super N<? super LHash<? super N<? super X>>>>>>>>> {}

public interface QLFirst<X> extends
        LFirstName<N<? super QWLLast<? super LFirstName<? super N<? super
                MR<? super N<? super X>>>>>>> {}
public interface QRFirst<X> extends
        LFirstName<N<? super QWRLast<? super MR<? super N<? super
                LFirstName<? super N<? super X>>>>>>> {}

public interface QLLast<X> extends
        LLastName<N<? super QWLFinish<? super LLastName<? super N<? super
                MR<? super N<? super X>>>>>>> {}
public interface QRLast<X> extends
        LLastName<N<? super QWRFinish<? super MR<? super N<? super
                LLastName<? super N<? super X>>>>>>> {}

public interface QLFinish<X> extends
        LHash<N<? super QWLHalt<? super LHash<? super N<? super
                MR<? super N<? super LHash<? super N<? super X>>>>>>>>> {}
public interface QRFinish<X> extends
        LHash<N<? super QWRHalt<? super LHash<? super N<? super
                ML<? super N<? super LHash<? super N<? super X>>>>>>>>> {}

public interface QLHalt<X> {}
public interface QRHalt<X> {}

Классы User и UserBuilder реализованы следующим образом (осталось только заполнить многоточия):


public class User {
    private final String firstName;
    private final String lastName;

    private User(UserBuilder<?> builder) {
        this.firstName = builder.firstName;
        this.lastName  = builder.lastName;
    }

    public String getFirstName() {
        return firstName;
    }

    public String getLastName() {
        return lastName;
    }

    public static User build(E<? super E<? super User>> e) {
        ...
    }

    public static UserBuilder<ML<? super N<? super LHash<? super N<? super
                                 E<? super E<? super User>>>>>>> user() {
        return new UserBuilder<>();
    }

    public static class UserBuilder<X> {
        private String firstName;
        private String lastName;

        public UserBuilder<LFirstName<? super N<? super X>>>
        withFirstName(String firstName) {
            this.firstName = firstName;
            return (UserBuilder<LFirstName<? super N<? super X>>>) this;
        }

        public UserBuilder<LLastName<? super N<? super X>>>
        withLastName(String lastName) {
            this.lastName = lastName;
            return (UserBuilder<LLastName<? super N<? super X>>>) this;
        }

        public QWRStart<? super LHash<? super N<? super X>>> please() {
            ...
        }

        // interfaces
        ...
    }
}

  • сперва заполним метод build.
    Его параметр — это объект типа E<? super E<? super User>>, а у интерфейса E своих методов нет. Значит для того, чтобы достать из e собранный объект типа User, нам понадобится что-то дополнительное. К счастью, подсказка спрятана в самом типе, достаточно только вспомнить правило PECS (Producer Extends, Consumer Super). Поэтому изменим описание интерфейса E:


    public interface E<X> extends Consumer<X>, ...

    Теперь у объекта e есть метод void accept(E<? super User>), принимающий другой объект E. И это уже будет Consumer для желанного нами объекта User. Если исходить из предположения, что вызов e.accept(callback) приведёт внутри к срабатыванию колбэка, то реализация метода build станет такой:


    public static User build(E<? super E<? super User>> e) {
        User[] ref = { null };
        E<? super User> callback = user -> ref[0] = user;
        e.accept(callback);
        return ref[0];
    }

    Осталось только обеспечить требуемое предположение;


  • метод please должен вернуть реализацию интерфейса QWRStart, которая должна в итоге быть приведена к типу E<? super E<? super User>>. Тут уже ничего, кроме грубой силы, применить не удастся (помним, что QWRStart наследует интерфейс E):
    public QWRStart<? super LHash<? super N<? super X>>> please() {
        return (QWRStart) o -> {
            E<? super User> e = (E<? super User>) o;
            e.accept(new User(this));
        };
    }

Целиком пример можно найти на гитхабе.


Чтобы не быть голословным, далее я привожу пример машины Тьюринга посложнее. Такая машина, грубо говоря, проверяет парность скобок, т.е. выражение ()(()()) является валидным, а выражение ()())(() — невалидным. Только открывающая и закрывающая скобки заменены символами A и B (x — дополнительный символ, означающий, что скобка на этом месте уже проверена).
Функция перехода будет следующей:


$(Start, Hash)\rightarrow(Scan, Hash, \bf{R})$


$(Scan, B)\rightarrow(Back, x, \bf{L})$
$(Scan, Hash)\rightarrow(Check, Hash, \bf{L})$
$(Scan, A)\rightarrow(Scan, A, \bf{R})$
$(Scan, x)\rightarrow(Scan, x, \bf{R})$


$(Back, A)\rightarrow(Scan, x, \bf{R})$
$(Back, B)\rightarrow(Back, B, \bf{L})$
$(Back, x)\rightarrow(Back, x, \bf{L})$


$(Check, Hash)\rightarrow(Halt, Hash, \bf{S})$
$(Check, x)\rightarrow(Check, x, \bf{L})$


Поиграться с данной машиной, или погенерировать свои, можно всё там же на гитхабе.
Да, генератор кода по описанию машины Тьюринга присутствует.


Для данной грамматики следующий код спокойно скомпилируется:


E<? super E<? super String>> e = start.A().A().B().B().stop();

а вот этот уже нет:


E<? super E<? super String>> e = start.B().A().B().A().stop();



8. Заключение


Содержательная часть на этом закончена. Мы узнали, как можно заставить компилятор валидировать цепочки вызовов согласно произвольному заранее заданному алгоритму.


Но можно — не значит нужно.
Во-первых, слишком много дополнительно объявленных классов, да и сигнатуры методов класса Builder выглядят очень сложно.
Во-вторых, компилятору понадобится гораздо больше памяти, чтобы не падать на сложных выражениях. В первую очередь — гораздо более глубокий стэк.
В-третьих, сложная диагностика ошибок. Типичный вывод компилятора выглядит как-то так (для краткости стёр названия пакетов):


incompatible types: QWRStart<capture#1 of ? super LHash<? super N<? super LFirstName<? super N<? super LLastName<? super N<? super ML<? super N<? super LHash<? super N<? super E<? super E<? super User>>>>>>>>>>>>> cannot be converted to E<? super E<? super User>>

Уровень информативности нулевой. Если хочется найти ошибку, то остаётся только два варианта:


  • пристально вглядываться в код;
  • в отдельной программе запускать соответствующую машину Тьюринга и следить за тем, что она делает. Не самое приятное занятие.

Тогда зачем это всё? Ответов, опять же, несколько:


  • for fun;
  • это может быть полезно исследователям и авторам новых языков программирования. Выбор системы типов — это одно из ключевых решений при проектировании нового языка.

Разработчики Kotlin, к примеру, знали, что в Java легко составить типы, проверка которых приведёт к экспоненциально долгому времени компиляции, и ввели т.н. Non-Expansive Inheritance Restriction. Поясню на минимальном примере:


interface A<T>
interface B<T> : A<B<Anything<T>>>

Это код на Kotlin, который не скомпилируется. А всё из-за того, что в параметрах суперинтерфейса для класса B присутствует тот же класс B, но там в параметрах уже не просто T, а более сложный тип. Определение не совсем точное и уж тем более не исчерпывающее, но идея должная быть понятна.


Цель проста — избежать "слишком сложных" типов, тем самым гарантируя высокую скорость компиляции. Из-за данного ограничения описанный способ запуска машин Тьюринга на Kotlin реализовать невозможно. В таком случае есть шанс, что проверка типов в Kotlin гарантированно завершается за конечное время.


С другой стороны, если все интерфейсы для машины Тьюринга объявить в Java-файлах, то компилятор Kotlin сделает ровно то же, что и компилятор Java — запустит соответствующую машину. Так что если учесть, что Kotlin используется не в изоляции от Java, то можно заключить, что и его система типов полна по Тьюрингу.




Ссылки


  1. Оригинальная публикация (Radu Grigore. Java Generics are Turing Complete).
  2. Авторская реализация генератора интерфейсов и примеры.
  3. Моя реализация на github.

Комментарии (7)


  1. Apx
    25.08.2017 01:55
    +1

    И как часто вам приходилось с такими вот финтами ушами играться, что это породило данную статью)) Просто розовые пони и драконы не существуют — точно также как и ваши примеры в реальной работе. Или статья заключается именно в этом?


  1. ibessonov Автор
    25.08.2017 08:20
    +7

    Результат интересен именно как исследование. В реальной работе же полезно знать о ковариантности и контравариантности, всё остальное для души.


    1. Evlikat
      25.08.2017 09:02
      -1

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


  1. amarao
    25.08.2017 13:58
    +1

    Разумеется, в программе надо реализовать обработку ошибок. Если программа хочет вывести ошибку, она должна сформировать её (из имён классов) и вывести на экран. В тьюринг-машине надо реализовать байт-код, который бы поддерживал exception'ы, функции с параметрами, классы, наследование, темплетизацию…


  1. Aquahawk
    25.08.2017 15:50
    +1

    Для typescript тоже тьюринг полноту системы типов доказали вроде как. github.com/Microsoft/TypeScript/issues/14833


  1. DarkGenius
    28.08.2017 20:49

    В первой формуле раздела Subtyping Machines в правой части индекс разве не n?


    1. ibessonov Автор
      28.08.2017 21:19

      Всё верно, там должен быть индекс n. Спасибо!
      EDIT: поправил формулу в публикации