# Python Type Hints are Turing Complete

Ori Roth

###### Abstract

Grigore showed that Java generics are Turing complete by describing a
reduction from Turing machines to Java subtyping. We apply Grigore’s algorithm
to Python type hints and deduce that they are Turing complete. In addition, we
present an alternative reduction in which the Turing machines are simulated in
real time, resulting in significantly lower compilation times. Our work is
accompanied by a Python implementation of both reductions that compiles Turing
machines into Python subtyping machines.

##  1 Introduction

Python enhancement proposal (PEP) 484 introduced optional type hints to the
Python programming language, together with a complete gradual type system
[11]. Tools such as Mypy [5] use type hints to check whether Python programs
are correctly typed. However, certain programs cause Mypy to enter an infinite
loop (we show an example below). We argue that the reason behind these
failures is not a Mypy bug, but a deeper issue in the Python type system. We
use Grigore’s reduction from Turing machines (TMs) to nominal subtyping with
variance [3] to prove that type hints are, in fact, Turing complete. In other
words, checking whether a Python program is correctly typed is as hard as the
halting problem.

###  1.1 Nominal Subtyping with Variance

Subtyping is a type system decision problem. Given types $t$ and $s$, the type
system should decide whether type $t$ is a subtype of $s$,

$t<:s,$

meaning that every $t$ object is also a member of $s$. For example, every
string is an object,
${{\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@language\footnotesize{\@listingGroup{ltx_lst_keyword
ltx_lst_keywords2}{\color[rgb]{0.50,0.00,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.50,0.00,0.33}str}}}}}}<:\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@language\footnotesize{\@listingGroup{ltx_lst_keyword
ltx_lst_keywords2}{\color[rgb]{0.50,0.00,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.50,0.00,0.33}object}}}}}}$,
but not every object is a string,
${{\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@language\footnotesize{\@listingGroup{ltx_lst_keyword
ltx_lst_keywords2}{\color[rgb]{0.50,0.00,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.50,0.00,0.33}str}}}}}}\nless:\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@language\footnotesize{\@listingGroup{ltx_lst_keyword
ltx_lst_keywords2}{\color[rgb]{0.50,0.00,0.33}\definecolor[named]{pgfstrokecolor}{rgb}{0.50,0.00,0.33}object}}}}}}$.
Subtyping is found, e.g., in variable assignments:

⬇

1x: t = ...

2y: s = x #
t$\color[rgb]{0.25,0.50,0.37}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.50,0.37}<:$s

The second assignment compiles if and only if $t<:s$.

Object-oriented languages such as Scala, C#, and Python use _nominal subtyping
with variance_ [4]. _Nominal_ means that subtyping is guided by inheritance.
Type c1 is a subtype of type c2 if class c1 is a descendant of c2:

⬇

1class s: ...

2class t(s): ...

3x: t = ...

4y: s = x # ✓

_Variance_ enables variability in type arguments. By default, type t[v] is a
subtype of t[w] if and only if ${{\text{\hbox{\pagecolor{lighter-
grey}\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@language\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame{\@listingGroup{ltx_lst_identifier}{v}}}}}}}=\text{\hbox{\pagecolor{lighter-
grey}\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@language\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame{\@listingGroup{ltx_lst_identifier}{w}}}}}}}$.
If t’s type parameter is covariant, then v can be any subtype of w,
${{\text{\hbox{\pagecolor{lighter-
grey}\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@language\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame{\@listingGroup{ltx_lst_identifier}{v}}}}}}}<:\text{\hbox{\pagecolor{lighter-
grey}\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@language\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame{\@listingGroup{ltx_lst_identifier}{w}}}}}}}$;
If it is contravariant, then ${{\text{\hbox{\pagecolor{lighter-
grey}\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@language\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame{\@listingGroup{ltx_lst_identifier}{v}}}}}}}:>\text{\hbox{\pagecolor{lighter-
grey}\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@language\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame{\@listingGroup{ltx_lst_identifier}{w}}}}}}}$.
In Python, variance is specified in an argument to TypeVar (the constructor of
type parameters). For example, the following Python program uses
contravariance and is correctly typed:

⬇

1X = TypeVar("X", contravariant=True)

2class t(Generic[X]): ...

3x: t[int] = t[object]() # ✓
(int$\color[rgb]{0.25,0.50,0.37}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.50,0.37}<:$object)

Kennedy and Pierce showed that nominal subtyping with variance is undecidable
[4] using a reduction from the Post correspondence problem (PCP) [8]. Their
work focused on three subtyping features (characteristics):

  1. 1.

_Contravariance_ : The presence of contravariant type parameters, as described
above.

  2. 2.

_Expansively recursive inheritance_ : The closure of types under the
inheritance relation and type decomposition
(${{\text{\hbox{\pagecolor{lighter-
grey}\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@language\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame{\@listingGroup{ltx_lst_identifier}{t}}[{\@listingGroup{ltx_lst_identifier}{v}}]}}}}}\rightarrow\text{\hbox{\pagecolor{lighter-
grey}\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@language\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame{\@listingGroup{ltx_lst_identifier}{v}}}}}}}$)
is unbounded. (The concept of expansive inheritance was introduced by Viroli
using a different definition [12].)

  3. 3.

_Multiple instantiation inheritance_ : Class t is allowed to derive class
s[$\cdot$] multiple times using different type arguments:

⬇

1class t(s[object], s[int]): ... # not legal in Python

Kennedy and Pierce proved that subtyping becomes decidable when contravariance
or expansive inheritance are removed, but they were uncertain about the
contribution of multiple instantiation inheritance to undecidability.

###  1.2 Subtyping Machines

Ten years later, Grigore showed that Java subtyping is Turing complete using a
direct reduction from TMs [3]. This reduction uses a subset of Java that
conforms to Kennedy and Pierce’s nominal subtyping with variance. Grigore’s
result settles Kennedy and Pierce’s open problem since Java does not support
multiple instantiation inheritance [7, §8.1.5]. (Intuitively, multiple
instantiation inheritance corresponds to non-deterministic subtyping [4, 9],
so while it was useful in the PCP reduction, it is redundant in the TM
reduction because deterministic TMs are as expressive as non-deterministic
TMs.)

Grigore’s reduction can be described as a function

$e(M,w)=\Delta\cdot q$ (1)

that encodes TM $M$ and input word $w$ as program $P=\Delta\cdot q$ consisting
of class table $\Delta$ and subtyping query $q$. The encoding ensures that TM
$M$ accepts $w$ if and only if query $q$ type-checks against $\Delta$.

The idea behind the reduction is to encode the TM configuration in the
subtyping query $q$. Recall that the configuration of TM $M$ comprises _(i)_
the content of the memory tape, _(ii)_ the location of the machine head on the
tape, and _(iii)_ the current state of the machine’s finite control. For
example, Figure 1 illustrates the initial configuration of $M$: The input word
$w=a_{1}a_{2}\ldots a_{m}$ is written on the tape, the machine head points to
the first letter $a_{1}$, and the current state is the initial state $q_{I}$.

$\cdots$$\bot$$\bot$$a_{1}$$a_{2}$$\cdots$$a_{m}$$\bot$$\bot$$\cdots$$q_{I}$
Figure 1: The initial configuration of a Turing machine

To explain how configurations are encoded as subtyping queries, let us first
introduce some syntax (adopted from Grigore’s paper). We write a generic type
A<B<C>> as $ABC$ for short. The use of $\blacktriangleleft$ instead of $<:$ in
a subtyping query means that the type on the left-hand side should be read in
reverse (the same goes for $\blacktriangleright$ and $:>$), e.g.,
$ABC\blacktriangleleft DE$ is equivalent to $CBA<:DE$.

The initial TM configuration, depicted in Figure 1, is encoded by the
following subtyping query:

${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}ZEEL_{\\#}}N{\color[rgb]{1,0.55,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.55,0}M^{L}}N{\color[rgb]{0.525,0,0.475}\definecolor[named]{pgfstrokecolor}{rgb}{0.525,0,0.475}L_{a_{1}}}N{\color[rgb]{0.525,0,0.475}\definecolor[named]{pgfstrokecolor}{rgb}{0.525,0,0.475}L_{a_{2}}}N\cdots
N{\color[rgb]{0.525,0,0.475}\definecolor[named]{pgfstrokecolor}{rgb}{0.525,0,0.475}L_{a_{m}}}N{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}L_{\\#}}{\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}Q_{I}^{wR}}\blacktriangleleft{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}EEZ}$
(2)

Observe that the types in Equation 2 have the same colors as the machine
configuration elements in Figure 1 which they encode. For example, the type
$L_{a_{1}}$ encodes the tape symbol $a_{1}$, and both are colored in purple.
As the type on the left-hand side is written in reverse, it is possible to
obtain the content of the encoded tape by reading the $L$ types from the left
to the right. The type $EEZ$ at both ends of the query encodes an infinite
sequence of blank symbols. The machine state $q_{I}$ is encoded by the type
$Q^{wR}_{I}$, and the machine head by the type $M^{L}$ (the superscripts
vary).

Grigore referred to the subtyping query in Equation 2 as a _subtyping machine_
because when the subtyping algorithm tries to resolve it, it simulates the
computation steps of the original TM. The state type $Q_{I}$ is moved along
the tape until it reaches the head type $M^{L}$. At that point, the subtyping
algorithm simulates a single TM transition by overwriting the current tape
cell $L_{a_{1}}$, moving the machine head, and changing the machine state. The
resulting subtyping query correctly encodes the next configuration in the TM
run. This process continues until the machine accepts, and the query is
resolved, or the machine aborts and a compilation error is raised. If the
machine runs indefinitely, the subtyping algorithm does not terminate.

While TMs move the machine head to the left or right freely, subtyping
machines can change direction only when reaching the end of the tape $EEZ$.
After simulating a TM transition, the subtyping machine must reach the end(s)
of the tape, rotate, and then reach the location of the machine head $M$ in
the right orientation, before it can simulate the next transition. In general,
Grigore’s subtyping machines can make $O(m)$ operations for every computation
step of the TM they simulate, where $m$ is the number of symbols on the tape,
resulting in a substantial slowdown. For example, Grigore’s simulation of the
CYK algorithm, which usually runs in $O(n^{3})$, takes $O(n^{9})$ subtyping
deduction steps to be completed.

#### Outline

In Section 2, we apply Grigore’s reduction to Python type hints and deduce
that they are Turing complete. Section 3 introduces an alternative design for
subtyping machines that simulate the TMs in real time, i.e., make $O(1)$
operations for each TM transition. Finally, Section 4 presents our Python
implementations of Grigore’s original reduction and the new reduction and
compares their performances.

##  2 Python Subtyping is Undecidable

Type hints were introduced to the Python programming language with PEP 484
[11]. Type hints are used as annotations and are entirely optional:

⬇

1def positive(x: int) $\rightarrow$ bool:

2 return x > 0

Static analysis on type hints is not performed by the Python interpreter, but
by third-party tools. For instance, Mypy [5] is a type checker for Python type
hints (in fact, PEP 484 was originally inspired by Mypy [11]).

The type system described in PEP 484 supports declaration site nominal
subtyping with variance. Type variables are specified using a special
constructor TypeVar that can be set as covariant or contravariant. For
example, class N in LABEL:lst:infinite:subtyping has a contravariant type
parameter Z.

As PEP 484 and related PEPs do not put any restrictions on expansively
recursive inheritance (at least, that the author could find), we conclude that
Python implicitly supports expansive inheritance. For example, class C in
LABEL:lst:infinite:subtyping has expansively recursive inheritance, and it
correctly compiles in Python and Mypy (the type "C[C[X]]" is in a string
literal because it forward-references class C).

By enabling both contravariance and expansively recursive inheritance, the
designers of PEP 484 have subjected Python type hints to the same pitfalls of
nominal subtyping with variance studied by Kennedy, Pierce, and Grigore. For
example, the code in LABEL:lst:infinite:subtyping, adapted from Kennedy and
Pierce [4], shows how contravariance and expansive inheritance can be combined
to induce an infinite subtyping cycle.

⬇

1from typing import TypeVar, Generic, Any

2Z = TypeVar("Z", contravariant=True)

3class N(Generic[Z]): ...

4X = TypeVar("X")

5class C(Generic[X], N[N["C[C[X]]"]]): ...

6_: N[C[Any]] = C[Any]() # infinite subtyping

Listing 1: Contravariance, expansively recursive inheritance, and infinite
subtyping with Python type hints

Contravariance and expansive inheritance are enough to implement Grigore’s
subtyping machines, which means that Python type hints are Turing complete. In
Section 4 we present an implementation of Grigore’s reduction with Python type
hints. The resulting subtyping machines correctly run with Mypy.

Grigore explains that subtyping machines could be used to perform certain
metaprogramming tasks, and even be abused to attack the compiler [3]. Most of
these (ab)uses still apply to Python type hints with (external) type checking,
as provided by Mypy.

Kennedy and Pierce proved that nominal subtyping with variance becomes
decidable once expansive inheritance is removed [4]. Restrictions to expansive
inheritance are implemented in, e.g., the Scala programming language [6,
§5.1.5] and the .NET framework [1, §II.9.2]. See Greenman et al. [2] for a
further discussion on expansively recursive inheritance and how to deal with
it. Removing expansive inheritance, however, might not be enough to make
Python type hints decidable—a more thorough inspection of the various type
system features in PEP 484 is required to determine this. Evidently, any
modification to PEP 484 aimed at making it decidable would technically break
backward compatibility.

##  3 Real-Time Subtyping Machines

Grigore’s subtyping machines must scan the entire tape memory before they can
simulate a single TM transition. This is because the subtyping machines can
change their direction (from $\blacktriangleleft$ to $\blacktriangleright$ and
vice versa) only when reaching the end of the tape. We now present an
alternative design for subtyping machines that simulate TMs in real time,
i.e., where a single TM computation step is simulated by $O(1)$ subtyping
deductions.

Let $M=\langle Q,\Sigma,q_{I},q_{h},\delta\rangle$ be a TM, where $Q$ is the
set of machine states, $\Sigma$ is the set of tape symbols, $q_{I}$ is the
initial state, $q_{h}$ is the termination state, and

$\delta:Q\times\Sigma\rightarrow Q\times\Sigma\times\\{L,R\\}$

is the transition function. The machine head can be moved to the left ($L$) or
right ($R$). The TM accepts its input if and only if it reaches the
termination state $q_{h}$. We use the symbols $\bot,\\#\not\in\Sigma$ to
denote blank tape cells.

The new encoding of subtyping machines is shown in Table 1. The encoding
comprises ten inheritance rules _(i)_ to _(x)_ (we use a colon to denote
inheritance). To encode a TM $M$ as a subtyping machine, complete the
inheritance rules using elements from $M$ that satisfy the conditions on the
right-hand side. For example, if $M$ contains state $q_{4}\in Q$ and tape
symbol $p\in\Sigma$, then by rule _(v)_ we get the inheritance rule

$Q^{LL}_{4}x:L_{p}NQ^{L}_{4}L_{p}Nx.$

Symbol $x$ is a type parameter and symbol ? denotes the wildcard type, i.e.,
the type that is consistent with (can be substituted by) any type. In Python,
this is the Any type [11]. All the type parameters used in the encoding are
contravariant. There are ten more inheritance rules in addition to those in
Table 1, obtained by swapping $L$ and $R$ in each rule in the table.

$\begin{array}[]{llr}{\emph{(i)}{}}&Q_{s}^{L}x:L_{a}NQ_{s^{\prime}}^{L}L_{b}Nx&\delta(q_{s},a)=\langle
q_{s^{\prime}},b,L\rangle\\\
{\emph{(ii)}{}}&Q_{s}^{L}x:L_{a}Q_{s^{\prime}}^{LRR}NL_{b}Nx&\delta(q_{s},a)=\langle
q_{s^{\prime}},b,R\rangle\\\
{\emph{(iii)}{}}&Q_{s}^{L}x:L_{\\#}Q_{s^{\prime}}^{L\\#L}NL_{b}Nx&\delta(q_{s},\bot)=\langle
q_{s^{\prime}},b,L\rangle\\\
{\emph{(iv)}{}}&Q_{s}^{L}x:L_{\\#}Q_{s^{\prime}}^{L\\#R}NL_{b}Nx&\delta(q_{s},\bot)=\langle
q_{s^{\prime}},b,R\rangle\\\
{\emph{(v)}{}}&Q_{s}^{LL}x:L_{a}NQ_{s}^{L}L_{a}Nx&\forall q_{s}\in Q,\forall
a\in\Sigma\\\ {\emph{(vi)}{}}&Nx:Q_{s}^{LRR}NQ_{s}^{RR}x&\forall q_{s}\in Q\\\
{\emph{(vii)}{}}&Nx:Q_{s}^{L\\#L}Q_{s}^{RL}NL_{\\#}Nx&\forall q_{s}\in Q\\\
{\emph{(viii)}{}}&Nx:Q_{s}^{L\\#R}NQ_{s}^{RR}L_{\\#}Nx&\forall q_{s}\in Q\\\
{\emph{(ix)}{}}&Nx:Q_{s}^{LR}NQ_{s}^{R}x&\forall q_{s}\in Q\\\
{\emph{(x)}}&Q_{h}^{L}x:L_{a}N{{\text{{{?}}}}}&\forall
a\in\Sigma\cup\\{\\#\\}\\\ \end{array}$

Table 1: Real-time subtyping machines. For each inheritance rule, swap $L$ and
$R$ to get the symmetrical rule.

The roles of the types in Table 1 are mostly the same as in Grigore’s encoding
Equation 2, i.e., $L_{a}$ is a tape cell containing the symbol $a$, $N$ is a
buffer type, and $Q_{s}$ is a state type. But, the new encoding does not use a
type for the machine head ($M$ in Grigore’s encoding). This is because the
state type $Q$ also indicates the location of the machine head. The
superscripts of $Q$ imply the head’s movement direction, e.g., $Q^{LL}_{s}$
means that the head is about to go two cells to the left, $Q^{L\\#R}_{s}$
means that the head is about to move left into a blank cell and then rotate,
and so on.

The initial TM configuration is encoded by the following subtyping query:

${\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}ZNL_{\\#}}\leavevmode\hbox
to10.81pt{\vbox to10.69pt{\pgfpicture\makeatletter\hbox{\hskip
5.40332pt\lower-5.34554pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-5.40332pt}{-3.40111pt}\pgfsys@invoke{
}\hbox{{\definecolor[named]{.}{rgb}{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}\pgfsys@color@rgb@stroke{0.8}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0.8}{0}{0}\pgfsys@invoke{
}\hbox{{\definecolor[named]{.}{rgb}{0.8,0,0}\color[rgb]{0.8,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0,0}$Q_{I}^{R}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope {{}}{}{{}}{}{{}} {}{}{ {}}
{}{}
{}\pgfsys@moveto{-5.40332pt}{-5.34554pt}\pgfsys@lineto{5.40332pt}{5.34554pt}\pgfsys@lineto{5.40332pt}{-5.34554pt}\pgfsys@closepath\pgfsys@clipnext\pgfsys@discardpath\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-5.40332pt}{-3.40111pt}\pgfsys@invoke{
}\hbox{{\definecolor[named]{.}{rgb}{1,0.55,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.55,0}\pgfsys@color@rgb@stroke{1}{0.55}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{1}{0.55}{0}\pgfsys@invoke{
}\hbox{{\definecolor[named]{.}{rgb}{1,0.55,0}\color[rgb]{1,0.55,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.55,0}$Q_{I}^{R}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}{\blacktriangleleft}{\color[rgb]{0.525,0,0.475}\definecolor[named]{pgfstrokecolor}{rgb}{0.525,0,0.475}L_{a_{1}}}N{\color[rgb]{0.525,0,0.475}\definecolor[named]{pgfstrokecolor}{rgb}{0.525,0,0.475}L_{a_{2}}}N\cdots{\color[rgb]{0.525,0,0.475}\definecolor[named]{pgfstrokecolor}{rgb}{0.525,0,0.475}L_{a_{m-1}}}N{\color[rgb]{0.525,0,0.475}\definecolor[named]{pgfstrokecolor}{rgb}{0.525,0,0.475}L_{a_{m}}}N{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}L_{\\#}NZ}$
(3)

The content of the tape is encoded by the $L$ types, read from the left to the
right. The current state and the position of the machine head are encoded by
the type $Q^{R}_{I}$—the current cell is on the right ($R$) of the type, which
is also the direction of the query ($\blacktriangleleft$). The infinite blank
ends of the tape are encoded by the type $L_{\\#}NZ$. Observe that the colors
of the types in Equation 3 match the colors of the corresponding elements in
the TM in Figure 1. Type $Q^{R}_{s}$ is colored half red and half orange
because it represents both the current state and the location of the head.

To prove the correctness of the simulation, we show that the subtyping query
in Equation 3 simulates the TM transitions while preserving the encoding of
the machine tape, head, and state comprising the TM configuration. There are
three variables to be considered: the initial orientation of the head, whether
or not the current cell is blank, and whether or not the machine head changes
direction. For example, the query in Equation 3 goes to the right ($R$) and
reads a non-blank cell $L_{a_{1}}$; The next cell could be either $L_{a_{2}}$,
if the head continues right, or blank $L_{\\#}$, if it rotates.

We now cover four cases, assuming that the initial orientation is _left_ (this
is the orientation used in Table 1). The other four cases are symmetrical.
Next to each subtyping deduction step, we mention the subtyping rule used in
this step. There are two subtyping rules [4]: Super, allowing us to replace a
type with its supertype using an inheritance rule from Table 1, and Var,
allowing us to remove a single type from both sides of the query. As all type
parameters are contravariant, the query changes direction (from
$\blacktriangleleft$ to $\blacktriangleright$ and vice versa) after applying
Var a single time.

#### Case I

The head points to a _non-blank_ cell $a$, replaces it with symbol $b$, and
continues _left_. The relevant TM transition is

$\delta(q_{s},a)=\langle q_{s^{\prime}},b,L\rangle$

and the resulting subtyping query is

$\begin{array}[]{ll}{\color[rgb]{0.75,0.75,0.75}\definecolor[named]{pgfstrokecolor}{rgb}{0.75,0.75,0.75}\pgfsys@color@gray@stroke{0.75}\pgfsys@color<EMAIL_ADDRESS>Q_{s}^{L}{\color[rgb]{0.75,0.75,0.75}\definecolor[named]{pgfstrokecolor}{rgb}{0.75,0.75,0.75}\pgfsys@color@gray@stroke{0.75}\pgfsys@color<EMAIL_ADDRESS>{\color[rgb]{0.75,0.75,0.75}\definecolor[named]{pgfstrokecolor}{rgb}{0.75,0.75,0.75}\pgfsys@color@gray@stroke{0.75}\pgfsys@color<EMAIL_ADDRESS>L_{a}NQ_{s^{\prime}}^{L}L_{b}N{\color[rgb]{0.75,0.75,0.75}\definecolor[named]{pgfstrokecolor}{rgb}{0.75,0.75,0.75}\pgfsys@color@gray@stroke{0.75}\pgfsys@color@gray@fill{0.75}\cdots}&{\emph{(i)}}+(\textsc{Super})\\\
{\color[rgb]{0.75,0.75,0.75}\definecolor[named]{pgfstrokecolor}{rgb}{0.75,0.75,0.75}\pgfsys@color@gray@stroke{0.75}\pgfsys@color<EMAIL_ADDRESS>Q_{s^{\prime}}^{L}L_{b}N{\color[rgb]{0.75,0.75,0.75}\definecolor[named]{pgfstrokecolor}{rgb}{0.75,0.75,0.75}\pgfsys@color@gray@stroke{0.75}\pgfsys@color@gray@fill{0.75}\cdots}&(\textsc{Var})\times
2\\\ \end{array}$

(“${\emph{(i)}}+\textsc{Super}$” means applying rule Super with inheritance
rule _(i)_ from Table 1. “$(\textsc{Var})\times 2$” means applying rule Var
twice.) Observe that the subtyping query simulates the TM transition while
preserving the encoding: symbol $L_{a}$ is replaced by $L_{b}$, state $Q_{s}$
is replaced by $Q_{s^{\prime}}$ (the next machine state), and the head moves
to the cell on the left.

#### Case II

The head points to a _non-blank_ cell $a$, replaces it with symbol $b$, and
continues _right_. The relevant TM transition is

$\delta(q_{s},a)=\langle q_{s^{\prime}},b,R\rangle$

and the resulting subtyping query is

$\begin{array}[]{ll}{\color[rgb]{0.75,0.75,0.75}\definecolor[named]{pgfstrokecolor}{rgb}{0.75,0.75,0.75}\pgfsys@color@gray@stroke{0.75}\pgfsys@color<EMAIL_ADDRESS>Q_{s}^{L}{\color[rgb]{0.75,0.75,0.75}\definecolor[named]{pgfstrokecolor}{rgb}{0.75,0.75,0.75}\pgfsys@color@gray@stroke{0.75}\pgfsys@color<EMAIL_ADDRESS>{\color[rgb]{0.75,0.75,0.75}\definecolor[named]{pgfstrokecolor}{rgb}{0.75,0.75,0.75}\pgfsys@color@gray@stroke{0.75}\pgfsys@color<EMAIL_ADDRESS>L_{a}Q_{s^{\prime}}^{LRR}NL_{b}N{\color[rgb]{0.75,0.75,0.75}\definecolor[named]{pgfstrokecolor}{rgb}{0.75,0.75,0.75}\pgfsys@color@gray@stroke{0.75}\pgfsys@color@gray@fill{0.75}\cdots}&{\emph{(ii)}}+(\textsc{Super})\\\
{\color[rgb]{0.75,0.75,0.75}\definecolor[named]{pgfstrokecolor}{rgb}{0.75,0.75,0.75}\pgfsys@color@gray@stroke{0.75}\pgfsys@color<EMAIL_ADDRESS>Q_{s^{\prime}}^{LRR}NL_{b}N{\color[rgb]{0.75,0.75,0.75}\definecolor[named]{pgfstrokecolor}{rgb}{0.75,0.75,0.75}\pgfsys@color@gray@stroke{0.75}\pgfsys@color@gray@fill{0.75}\cdots}&(\textsc{Var})\\\
{\color[rgb]{0.75,0.75,0.75}\definecolor[named]{pgfstrokecolor}{rgb}{0.75,0.75,0.75}\pgfsys@color@gray@stroke{0.75}\pgfsys@color<EMAIL_ADDRESS>Q_{s^{\prime}}^{LRR}NL_{b}N{\color[rgb]{0.75,0.75,0.75}\definecolor[named]{pgfstrokecolor}{rgb}{0.75,0.75,0.75}\pgfsys@color@gray@stroke{0.75}\pgfsys@color@gray@fill{0.75}\cdots}&{\emph{(vi)}}~{}+(\textsc{Super})\\\
{\color[rgb]{0.75,0.75,0.75}\definecolor[named]{pgfstrokecolor}{rgb}{0.75,0.75,0.75}\pgfsys@color@gray@stroke{0.75}\pgfsys@color<EMAIL_ADDRESS>L_{b}N{\color[rgb]{0.75,0.75,0.75}\definecolor[named]{pgfstrokecolor}{rgb}{0.75,0.75,0.75}\pgfsys@color@gray@stroke{0.75}\pgfsys@color@gray@fill{0.75}\cdots}&(\textsc{Var})\times
2\\\
{\color[rgb]{0.75,0.75,0.75}\definecolor[named]{pgfstrokecolor}{rgb}{0.75,0.75,0.75}\pgfsys@color@gray@stroke{0.75}\pgfsys@color<EMAIL_ADDRESS>L_{b}N{\color[rgb]{0.75,0.75,0.75}\definecolor[named]{pgfstrokecolor}{rgb}{0.75,0.75,0.75}\pgfsys@color@gray@stroke{0.75}\pgfsys@color@gray@fill{0.75}\cdots}&{\emph{(v)}}~{}+(\textsc{Super})\\\
{\color[rgb]{0.75,0.75,0.75}\definecolor[named]{pgfstrokecolor}{rgb}{0.75,0.75,0.75}\pgfsys@color@gray@stroke{0.75}\pgfsys@color@gray@fill{0.75}\cdots}NL_{b}Q_{s^{\prime}}^{R}\blacktriangleleft{\color[rgb]{0.75,0.75,0.75}\definecolor[named]{pgfstrokecolor}{rgb}{0.75,0.75,0.75}\pgfsys@color@gray@stroke{0.75}\pgfsys@color@gray@fill{0.75}\cdots}&(\textsc{Var})\times
2\\\ \end{array}$

#### Case III

The head points to a _blank_ cell (the end of the tape), replaces it with
symbol $b$, and continues _left_. The relevant TM transition is

$\delta(q_{s},\bot)=\langle q_{s^{\prime}},b,L\rangle$

and the resulting subtyping query is

$\begin{array}[]{ll}ZNL_{\\#}\blacktriangleright
Q_{s}^{L}{\color[rgb]{0.75,0.75,0.75}\definecolor[named]{pgfstrokecolor}{rgb}{0.75,0.75,0.75}\pgfsys@color@gray@stroke{0.75}\pgfsys@color<EMAIL_ADDRESS>ZNL_{\\#}\blacktriangleright
L_{\\#}Q_{s^{\prime}}^{L\\#L}NL_{b}N{\color[rgb]{0.75,0.75,0.75}\definecolor[named]{pgfstrokecolor}{rgb}{0.75,0.75,0.75}\pgfsys@color@gray@stroke{0.75}\pgfsys@color@gray@fill{0.75}\cdots}&{\emph{(iii)}}~{}+(\textsc{Super})\\\
ZN\blacktriangleleft
Q_{s^{\prime}}^{L\\#L}NL_{b}N{\color[rgb]{0.75,0.75,0.75}\definecolor[named]{pgfstrokecolor}{rgb}{0.75,0.75,0.75}\pgfsys@color@gray@stroke{0.75}\pgfsys@color@gray@fill{0.75}\cdots}&(\textsc{Var})\\\
ZNL_{\\#}NQ_{s^{\prime}}^{RL}Q_{s^{\prime}}^{L\\#L}\blacktriangleleft
Q_{s^{\prime}}^{L\\#L}NL_{b}N{\color[rgb]{0.75,0.75,0.75}\definecolor[named]{pgfstrokecolor}{rgb}{0.75,0.75,0.75}\pgfsys@color@gray@stroke{0.75}\pgfsys@color@gray@fill{0.75}\cdots}&{\emph{(vii)}}~{}+(\textsc{Super})\\\
ZNL_{\\#}NQ_{s^{\prime}}^{RL}\blacktriangleright
NL_{b}N{\color[rgb]{0.75,0.75,0.75}\definecolor[named]{pgfstrokecolor}{rgb}{0.75,0.75,0.75}\pgfsys@color@gray@stroke{0.75}\pgfsys@color@gray@fill{0.75}\cdots}&(\textsc{Var})\\\
ZNL_{\\#}NQ_{s^{\prime}}^{RL}\blacktriangleright
Q_{s^{\prime}}^{RL}NQ_{s^{\prime}}^{L}L_{b}N{\color[rgb]{0.75,0.75,0.75}\definecolor[named]{pgfstrokecolor}{rgb}{0.75,0.75,0.75}\pgfsys@color@gray@stroke{0.75}\pgfsys@color@gray@fill{0.75}\cdots}&{\emph{(ix)}}~{}+(\textsc{Super})\\\
ZNL_{\\#}\blacktriangleright
Q_{s^{\prime}}^{L}L_{b}N{\color[rgb]{0.75,0.75,0.75}\definecolor[named]{pgfstrokecolor}{rgb}{0.75,0.75,0.75}\pgfsys@color@gray@stroke{0.75}\pgfsys@color@gray@fill{0.75}\cdots}&(\textsc{Var})\times
2\\\ \end{array}$

#### Case IV

The head points to a _blank_ cell, replaces it with symbol $b$, and continues
_right_. The relevant TM transition is

$\delta(q_{s},\bot)=\langle q_{s^{\prime}},b,R\rangle$

and the resulting subtyping query is

$\begin{array}[]{ll}ZNL_{\\#}\blacktriangleright
Q_{s}^{L}{\color[rgb]{0.75,0.75,0.75}\definecolor[named]{pgfstrokecolor}{rgb}{0.75,0.75,0.75}\pgfsys@color@gray@stroke{0.75}\pgfsys@color<EMAIL_ADDRESS>ZNL_{\\#}\blacktriangleright
L_{\\#}Q_{s^{\prime}}^{L\\#R}NL_{b}N{\color[rgb]{0.75,0.75,0.75}\definecolor[named]{pgfstrokecolor}{rgb}{0.75,0.75,0.75}\pgfsys@color@gray@stroke{0.75}\pgfsys@color@gray@fill{0.75}\cdots}&{\emph{(iv)}}~{}+(\textsc{Super})\\\
ZN\blacktriangleleft
Q_{s^{\prime}}^{L\\#R}NL_{b}N{\color[rgb]{0.75,0.75,0.75}\definecolor[named]{pgfstrokecolor}{rgb}{0.75,0.75,0.75}\pgfsys@color@gray@stroke{0.75}\pgfsys@color@gray@fill{0.75}\cdots}&(\textsc{Var})\\\
ZNL_{\\#}Q_{s^{\prime}}^{RR}NQ_{s^{\prime}}^{L\\#R}\blacktriangleleft
Q_{s^{\prime}}^{L\\#R}NL_{b}N{\color[rgb]{0.75,0.75,0.75}\definecolor[named]{pgfstrokecolor}{rgb}{0.75,0.75,0.75}\pgfsys@color@gray@stroke{0.75}\pgfsys@color@gray@fill{0.75}\cdots}&{\emph{(viii)}}~{}+(\textsc{Super})\\\
ZNL_{\\#}Q_{s^{\prime}}^{RR}\blacktriangleleft
L_{b}N{\color[rgb]{0.75,0.75,0.75}\definecolor[named]{pgfstrokecolor}{rgb}{0.75,0.75,0.75}\pgfsys@color@gray@stroke{0.75}\pgfsys@color@gray@fill{0.75}\cdots}&(\textsc{Var})\times
2\\\ ZNL_{\\#}NL_{b}Q_{s^{\prime}}^{R}NL_{b}\blacktriangleleft
L_{b}N{\color[rgb]{0.75,0.75,0.75}\definecolor[named]{pgfstrokecolor}{rgb}{0.75,0.75,0.75}\pgfsys@color@gray@stroke{0.75}\pgfsys@color@gray@fill{0.75}\cdots}&{\emph{(v)}}~{}+(\textsc{Super})\\\
ZNL_{\\#}NL_{b}Q_{s^{\prime}}^{R}\blacktriangleleft{\color[rgb]{0.75,0.75,0.75}\definecolor[named]{pgfstrokecolor}{rgb}{0.75,0.75,0.75}\pgfsys@color@gray@stroke{0.75}\pgfsys@color@gray@fill{0.75}\cdots}&(\textsc{Var})\times
2\\\ \end{array}$

The TM rejects its input when its current state is $q_{s}$, the current tape
symbol is $a$, and transition $\delta(q_{s},a)$ is not defined. In this case,
the subtyping query $L_{a}\blacktriangleright Q^{L}_{s}$ also rejects, because
there is no inheritance rule in Table 1 with which rule Super can be applied.
On the other hand, if the TM reaches state $q_{h}$ and accepts its input, then
the subtyping query $L_{a}\blacktriangleright Q^{L}_{h}$ is resolved by
applying rule _(x)_.

Note that the new simulation is clearly real-time. To simulate a single TM
transition, the subtyping machine performs at most eight subtyping deductions
(in cases II and IV).

The wildcard type used in rule _(x)_ does not appear in Kennedy and Pierce’s
system of nominal subtyping with variance. Instead of using the wildcard, the
subtyping machine could go to either side of the tape before resolving the
query, as done in Grigore’s simulation. This makes the design of the subtyping
machines more complicated, and their simulation of the TM returns to be non-
real-time—although it does not increase the computational complexity of the
simulated TM.

##  4 Implementation and Performance Experiment

This paper is accompanied by a Python implementation [10] of Grigore’s
original reduction and our new real-time simulation, introduced in Section 3.
Our implementation compiles TMs into Python subtyping machines that use the
type hints and generics described in PEP 484 [11]. Each subtyping machine
comprises a class table (Table 1) and a variable assignment that invokes a
subtyping query Equation 3. To run the subtyping machine, we run Mypy on the
generated Python code.

Mypy’s subtyping algorithm is most likely implemented using recursion. As
evidence, when running Mypy on the infinite subtyping query described in
LABEL:lst:infinite:subtyping, it does not run indefinitely but instead raises
a segmentation fault. This observation makes it possible to measure the run
time of the subtyping machine, i.e., the number of subtyping deductions it
performs, by the minimal size of the call stack required by Mypy to type-check
the machine.

Figure 2 describes the results of our experiment [10], in which we measured
the run times of subtyping machines accepting input words of various lengths.
The TM used in the experiment recognizes palindromes over $\\{a,b\\}$ and runs
in $O(n^{2})$. We compiled the TM together with random palindromes of various
lengths into subtyping machines, once using Grigore’s method and once with our
construction. Then, we used binary search to find the minimal call stack size
(in megabytes (MB)) required for Mypy to type-check the machine without
getting a segmentation fault. The results of the experiment are shown in
Figure 2.

$10$$20$$30$$40$$50$$60$$70$$80$$90$$5$$7$$9$$11$$13$Input lengthCall stack
size [MB]Grigore [3]Current work Figure 2: Run times of the palindromes
subtyping machines: Grigore’s reduction vs. the new reduction.

In theory, Grigore’s subtyping machines should run in $O(n^{3})$ due to their
inherent slowdown, while our machines are expected to run in $O(n^{2})$ since
they simulate the palindromes TM in real time. In practice, we see that our
subtyping machines are much faster than Grigore’s and require much fewer
resources to be type-checked.

## References

  * [1] ECMA International.  ECMA Standard 335: Common Language Infrastructure, 3 edition, June 2005.  Available at http://www.ecma-international.org/publications/standards/Ecma-335.htm (accessed Aug. 2022).
  * [2] Ben Greenman, Fabian Muehlboeck, and Ross Tate.  Getting f-bounded polymorphism into shape.  SIGPLAN Not., 49(6):89–99, June 2014.
  * [3] Radu Grigore.  Java generics are turing complete.  In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, page 73–85, New York, NY, USA, 2017. Association for Computing Machinery.
  * [4] Andrew Kennedy and Benjamin Pierce.  On decidability of nominal subtyping with variance.  In Int. Work. Found. & Devel. OO Lang., FOOL/WOOD‘07, Nice, France, January 2007. ACM.
  * [5] Jukka Lehtosalo, Guido van Rossum, Ivan Levkivskyi, and Michael J. Sullivan.  mypy.  Available at http://mypy-lang.org/ (accessed Aug. 2022).
  * [6] Martin Odersky, Philippe Altherr, Vincent Cremet, Gilles Dubochet, Burak Emir, Philipp Haller, Stéphane Micheloud, Nikolay Mihaylov, Adriaan Moors, Lukas Rytz, Michel Schinz, Erik Stenman, and Matthias Zenger.  Scala language specification version 2.13.  Available on: https://scala-lang.org/files/archive/spec/2.13/ (accessed Aug. 2022).
  * [7] Oracle.  The Java Language Specification, Java SE 8 Edition, February 2015.  Available at https://docs.oracle.com/javase/specs/.
  * [8] Emil Post.  A variant of a recursively unsolvable problem.  Bulletin of the American Mathematical Society, 52:264–268, 1946\.
  * [9] Ori Roth.  Study of the subtyping machine of nominal subtyping with variance.  Proc. ACM Program. Lang., 5(OOPSLA), October 2021.
  * [10] Ori Roth.  Python Typing Machines, August 2022.  https://doi.org/10.5281/zenodo.7004898.
  * [11] Guido van Rossum, Jukka Lehtosalo, and Łukasz Langa.  PEP 484—Type Hints.  Available at https://peps.python.org/pep-0484/ (accessed Aug. 2022).
  * [12] Mirko Viroli.  On the recursive generation of parametric types.  Technical report, DEIS-LIA-00-002, Universitá di Bologna, September 2000\.