日本ソフトウェア科学会第 37 回大会 (2020 年度) 講演論文集

Type-check Python Programs with a Union
Type System
Senxi Li Tetsuro Yamazaki Shigeru Chiba

We propose that a simple type system and type inference can type most of the Python programs with anempirical study on real-world code. Static typing has been paid great attention in the Python languagewith its growing popularity. At the same time, what type system should be adopted by a static checker isquite a challenging task because of Python’s dynamic nature. To exmine whether a simple type system andtype inference can type most of the Python programs, we collected 806 Python repositories on GitHub andpresent a preliminary evaluation over the results. Our results reveal that most of the real-world Python
programs can be typed by an existing, gradual union type system. We discovered that 82.4% of the expressions can be well typed under certain assumptions and conditions. Besides, expressions of a union typeare around 3%, which indicates that most of Python programs use simple, literal types. Such preliminary
discovery progressively reveals that our proposal is fairly feasible.

while the eﬀectiveness of the type system has not

1 Introduction

been empirically studied. Other works such as Py-

Static typing has been paid great attention in

type implement a strong type inferencer instead of

the Python language with its growing popularity.

enforcing type annotations.

At the same time, what type system should be

As a dynamically typed language, Python excels

adopted by a static checker is quite a challenging

at rapid prototyping and its avail of metaprogram-task because of Python’s dynamic nature. Thereming and reflection. Pythonists can also customize

have been suﬃcient existing works on static typing

their own metaclasses and create classes at run-for Python. Mypy [5], one of the most famed statictime. Beside, programmers can introspect or fur-type checkers in Python, use type annotations in-ther create, modify Python objects dynamically introduced from Python 3.0 and statically typecheckany sense. However, these powerful features would

programs by giving semantics to the annotations.

be nightmare for static checkers. Modifying a class

Mypy has a powerful type system with features

attribute with eval(‘Rect.setColor("red")’) at

such as bidirectional type inference and generics,

runtime will not provide any type information to astatic checker. Therefore, the checker will complain∗ Type-check

Python Programs with a Union Type
SystemThis is an unrefereed paper. Copyrights belong to
the Author(s).
Senxi Li, Tetsuro Yamazaki, Shigeru Chiba, 東京大学 大 学 院 情 報 理 工 学 系 研 究 科, Graduate School ofInformation Science and Technology, University ofTokyo.

and raise an attribute error if the program inquires
this attibute by accessing Rect.color, or will justthrow an unknown type if the type system is gradual. The operations can hardly provide any type
information before runtime and thus a checker will
fail to typecheck that piece of code. Consequently,

it is impossible for any exising type system to type-To answer the question, we collected Python reposi-check all Python programs at a theoretical level.

tories from GitHub and analyzed their source code

While such discussion can easily drive us to anwith a static checker driven by a designed, sim-end that no existing type system can fully type-ple gradual union type system. We believe thatcheck all Python programs, the following assump-union type can handle abstraction and polymor-

tions play a substantial role in our motivation:

phism within bounds, which can meet the damand• Python programs seems easy. Being a popu-

of real-world Python code.

In addition, we ap-

lar programming language used by people fromply a type inference approach that infers function

web developers to data scientists, most of theand method types by type information from run-

Python programs shall be easy to read andtime. While runtime can only tell properties of ob-share.

As another aspect, machine learning

jects under limited conditions, we claim that vari-tasks take a significant role in Python appli-

ables, functions and objects can be correctly in-cations in recent years. In spite of their indeed

ferred and typed if runtime can consistently provide

complicated algorithms, it can be smoothly

their types.

imagined that simple data types can handle

Our preliminary result shows that our designed,

their code and many of the expressions are justsimple type system and type inference algorithms

literals like numbers and lists. Initializing a

can typecheck most of the Python programs. The

tensor with a value of List[float], function

investigation indicates that 82.4% of the expres-of mathemetical multiplication over matrix andsions in the source code are well typed under certain

vector being typed as List[List[float]] →conditions. Besides, only 3.1% of the expressions

List[float] → List[float] and so on may

are of union type. This paper also involves further

serve as evidence for our assumption.

evaluation to better analyze if such a type system• Programmers are competent and well-educated.

can satisfy Python’s need.

This hypothesis is heavily rooted in the com-

This paper proceeds in the following manner.

petent programmer hypothesis [1], which states

Section 2 discuesses our motivation and briefly re-that most software faults introduced by ex-

views benefits of static typing over dynamic typing.

perienced programmers are due to small syn-

Section 3 proposes a pseudo language and by de-tactic errors.

Furthermore, the majority of

scribing its core calculus we further discuss how our

Python programmers are believed to have asystem performs type checking. Section 4 shows

background of some statically typed languages.

our empirical study of real-world Python programs

In other words, well-educated programmers

and its results will help answer the research ques-

write programs that may obey a type systemtions that we address. Section 5 mentions related

they are familiar with implicitly, even Python

works and a conclusion with directions for future

syntatically never impedes them writing “un-work ends this paper.

typable” code. Accordingly, a simple type system for objects can type most of such Python

2 Motivation

programs.

There have been many complex type systems andThese concerns and assumptions lead us to ourtype inference algorithms proposed for Python in

research question: Is there an exising type systemorder to statically typecheck programs. However,able to type most of real-world Python programs?

they are not successful because of the dynamic na-

ture of Python. Many of the existing works ap-

ning the user code.

ply strong type systems such as callable type toAt this moment it seems that we can type Python

type functions/methods and generics to abstract

programs if a programmer carefully inject type an-objects more precisely. Type inference algorithms

notations with the usage of a well implemented

infer types with hints avaiable in the source code.

type checker. However, the situation will not let

In the following of this section, we will illustrate

us stay optimistic as long as we are engaging withhow some of existing type systems can and cannot

Python. As a powerful dynamic language, Python

type Python programs with examples.

has a strong functionality on introspection and re-

One of the primary benefits of static typing overflection, enabling programmers to introspect or fur-dynamic typing is that it helps localize errors. For

ther modify objects at runtime. Consider the fol-example, suppose a programmer misunderstands

lowing piece of code:

the use of a library function, such as a getSum function in a module arith which expects one argumentof a list of integers but instead the programmer
passes in a list of strings.
12
3
4

from arith import getSum
lst = ["sum", "the", "list"]
getSum(lst)

1
2
3
4
5
6

class Rect:
pass
def touchColor(arg: Rect) −> str:
exec("arg.color = ‘red’")return arg.color

Though this program can be seriously complained
about the bad attribute usage, the given code isabsolutely valid in Python. In the body of func-

In a purely dynamically typed language, calling thetion touchColor, the behavior of the argument arg

function in such a way will cause a runtime error.

is modified by the builtin function exec such that

Perhaps such runtime error will occur deep inside

a string is assigned to an attribute color of arg.

the body of the function in arith, which contains

Calling this function by passing in an instance of

operations that can be performed on numbers butclass Rect at runtime will return "red" just as de-not strings. On the other hand, if the programmer

signed. Nevertheless, this piece of code cannot bemake use of a static type checker, the error can bewell typed with a normal type system, or any ex-

detected and caught before the call to getSum. The

isting ones even its argument and return are finely

following shows that the parameter and return ofannotated. A static checker, such as Mypy [5], willfunction getSum is annotated using type annota-

complain that “Rect” has no attribute “color”. The

tions.

confliction stems from the fact that the reflection

1
2
3
4

from typing import Listat line 5 does not render any type information to

def getSum(argList: List[int]) −> int:...

the checker statically.

The parameter of the function is well annotated

3 Core Calculus

with a generic list type so that a static checker

Observations and presumptions bring us to thecan understand what type of elements a list should

following idea: a simple but well designed type sys-hold.

By documenting and enforcing type con-tem can type most of the Python programs. We

strains on the definition of getSum, a static checker

choose a simple, gradual union type system which

can prevent the usage of the function if the given

seems powerful enough for typing Python code andargument conflicts as declared before indeed run-by applying the type system, we shall carry out anempirical study to investigate to what extent real-

the primary expressions in Python. C() refers to in-world Python programs are typeable. To show the

stance initialization, which will create an instancecore calculus of our designed type system, we de-of a class C. e.f refers to field access. e(e) suggests

fine a simple pseudo language MiniPy and give its

an invocation. Since there is no function definition

formal calculus. The static semantics of MiniPy isin MiniPy, e(e) can only be method invocation.

almost a subset of the Gradual Typed Object Calculus defined in [8]. For simplicity, MiniPy does not

3. 2 Subtyping

have statements and only contains part of the ex-

Now let us define the types, denoted as follows:pressions in Python. Meanwhile, the typing rules
and type checking of MiniPy are the core part ofthat of our developed type system.
The type system of MiniPy is a gradual, union
type system. The purpose of choosing the gradual typing, which allows the mixture of static anddynamic typing, is to distinguish the typeable anduntypeable with the power of the unknown type. We
use the unknown type to mark the parts of the program that cannot be typed as dynamically typed,
and use the other types in the type system to typethose typeable parts.

| C | T → T | T ∨ T

T, S range over types; ? refers to the unknown
type in a gradual type system.
As the types suggest, our type system is gradual, which mixs static and dynamic type checking
by introducing the unknown type ?. Gradual typing integrates the unknown type ? and type consistency into an existing static type system in orderto support fully dynamic type checking, static typechecking, and any point on the continuum. [3]Besides basic types and function type, the typesystem allows union type. A union type, more pre-In the following subsections we first give the syntax and typing rules of MiniPy and then show how
the type system typechecks programs.

cisely, an untagged union, noted T1 ∨ T2 , denotes
the value of such a type can be either T1 or T2
at runtime. In the set-theoretic interpretation forunion type by Frisch [2], for example, Int ∨ Int is

3. 1 Syntax

the same type as Int; a value of Int can be a value

The syntax of MiniPy is given as follows:
CL ::= class C(C): {M} [class]
M ::= def m(p):T ::= ?

return e; [method]e ::= x | C() | e.f | e(e) [expressions]
The metavariables are listed as follows: C, D range
over class names; M ranges over method declarations; f ranges over fields; m ranges over methods;
x ranges over variables; e ranges over expressions;
In MiniPy, we can define a class with the classdefinition CL. A class definition class C(D): {M}introduces a class named C inheriting a superclass D.
The body of the class definition is a single method
declaration M. The body of the method is a single
return statement. Expressions e includes some ofof Int ∨ String. Union type can be used to type
methods whose argument shares some same properties. For instance, a method declaration def m(x):return x.f; can be well typed as type (T1 ∨ T2 )→ (S1 ∨ S2 ) if both T1 and T2 have the field f andtheir resulting types are S1 and S2 , respectively.
Before describing the subtyping rules, let us
briefly discuss the unknown type. ? is completely
unknown: we do not know what type it represents;
in other words, ? represents any type. For instance, a type Int → ? represents a function from
Int to some unknown type. In other words, thistype can be any type of function as long as it maps
from Int to some other type.

While the type consistency relation will be de-the following definition.

fined in the next subsection, here we present theC ∼ C(∼-ID)∼ T(∼-?1)

subtyping rules as the following:
?

<:

C <:
C1 <:

C

?

(<:-?)?

(<:-ID)C2C2 <:C1 <: C3

C3(<:-TRANS)

class C(D): {. . .}(<:-INHER)
C <: DS2 <: S1
T1 <: T2(<:-→)
S1 → T1 <: S2 → T2
S1 <: TS2 <: T(<:-∨LEFT)
S1 ∨ S2 <: T
S <: T1(<:-∨RIGHT1)
S <: T1 ∨ T2
S <: T2(<:-∨RIGHT2)
S <: T1 ∨ T2
The subtype relation is straightforward to define.
Most of the rules just follow a traditional subtyping for objects. A special construct is about theunknown type, which is given by ?

<:(∼-?2)T ∼ ?
S1 ∼ S2
T1 ∼ T2(∼-→)
S1 → T1 ∼ S2 → T2
S1 ∼ T1
S2 ∼ T2(∼-∨1)
S1 ∨ S2 ∼ T1 ∨ T2
S1 ∼ T2
S2 ∼ T1(∼-∨2)
S1 ∨ S2 ∼ T1 ∨ T2
The definition of type consistency is almost thesame as the one described in [8], while our typesystem involves the union type. (∼-∨1) describesthat two union types are consistent if their components are consistent with each other. (∼-∨2)tells the same property with a reverse consistent
relation of their components since two union types
are identical with the same components even theirorder are diﬀerent.

?. A classinheritance simply gives a subtype relation fromthe subclass to its superclass. <:-∨LEFT describesthat a union type is the subtype of another type if
both of its components are the subtype of that type.

3. 4 Consistent-Subtyping
Consistent-Subtyping is defined that takes bothtype consistency and subtyping into account.

of a union type if that type is the subtype of one

T’
T’ ∼ T(∼<:)
S ∼<: T
Although this rule still remains some non-of the components of the union type. <:-∨RIGHT2

determinacy because of the type T’ . Previous re-just explains the other case.

searches have conceived the consistent-subtyping<:-∨RIGHT1 describes that one type is the subtype

S <:relation in terms of a restriction operator T1 |T2
3. 3 Type Consistency

which masks oﬀ the parts of a type T1 that are

The intuition behind type consistency is to check

unknown in a type T2 . For space reason we will notwhether the two types are equal in the parts whereexplain its formular or a formal definition of theboth types are known. A gradual type system uses

consistent-subtyping relation: all details are given

type consistency, which replaces type equality thatby [8].

a simple type system typically uses.

A gradual

type check allows an implict conversion between

3. 5 Typing Rules

two types if they are consistent with each other.

The typing rules are outlined in this subsection.

We present the consistency relation ∼ on types with

An environment Γ is a finite mapping from variables
to types, written x:T.

Γ ::= ∅ | Γ, x:T

Before illustrating the typing rules, let us definesome operators on types and a lookup function thatare necessary to define and reason the typing rules

4 Can the Union Type System Typeand further the type inference. The two operators

Real-World Python Programs?

on types, especially on function types, are: (i) theIn this section we will describe the empiricaldom(.) operator that given a funciton type T re-study that examines whether our simple type sys-turns the domain of that type and (ii) the cod(.)

tem can type most expressions in real-world Python

operator that returns its codomain. While the for-programs. Detailed construction of the experimentmal definition of these two operators are omitted forwill be illustrated and a preliminary result, thoughspace reason, since the unknown type ? in our typestill under rough analysis currently, will be given

system can be any type (not only basic types), theto progressively show to what extent expressions inpatterns for ? proceed as dom(?)

real-world Python programs are typeable under our= ? and cod(?)

designed type system.

= ?.
The intuition of the lookup function is that we

To build our dataset, we collected 806 Python

need to be able to identify the type of a field or

repositories from Github. Our dataset contains 806

method upon a given type. Function field(T, f)

repositories, 101,442 Python files and 11,367,317

returns the field type of T if type T holds such alines of code in total. Since we didn’t apply any

field, and it is defined by:bias while searching repositories, which can indi-field(C, f) = T

cate that the applications of the collected reposito-

field(?, f) = ?

ries are of various fields. Algorithm 1 shows pseu-

field(T1 ∨T2 , f) = field(T1 , f)∨field(T2 , f)docode for the overview of our experiment setup

field( , ) = undefinedand how we typecheck programs and detect static

With these operators and the lookup function,
the typing rules are given as:
x: T ∈ Γ(T-VAR)Γ ⊢ x: T(T-INST)
Γ ⊢ C(): CΓ ⊢ e:

type errors from a given set of repositories.

Algorithm 1: overview
Data: Repositories ← set of Python
repositories
Result: report of type errors

T0field(T0 , f) = T1
(T-FIELD)Γ ⊢ e.f: T1

for repo ∈ Repositories do
run unit tests in repo;Γ ⊢ m: TΓ ⊢ e: S
S ∼<: dom(T)Γ ⊢ m(e): cod(T)(T-INVK)
The type judegement for expressions is almost acollect runtime type information;subset of the one provided by Siek and Taha [Grad-for .py file ∈ repo doual Typing for Objects]. Since our type system isdatabase ← collected runtime type
information;code ← content of .py file;gradual, T-INVK will judge not the subtype relation<: between the argument and the parameter, but
their consistent-subtyping relation ∼<:.

typechecker(code, database);
end
end

In a word, for a given set of repositories we firstrun their test code if there is. During the exe-

scripts which use the settrace function from the

cution, runtime type information is collected andbuiltin sys module to interpose on function calls

recorded into database. After that, we extract all

and method invocations. Furthermore, the argu-

valid Python files inside each repositories and thenments and returns of the traced callables are pro-use a type checker driven by the type system we

filed so that the data type of the objects are ob-presented in Section 3 to typecheck those Python

tained and they are treated as the runtime type

files. Finally, a report of static type errors detected

information of the corresponding functions/meth-by the checker is carried out.

ods.

Additionally, builtin container types such

In the following subsections, we explain how we

as list and tuple are recorded in generic types,

conduct each step of the experiment in detail, ana-i.e., the data type of [1, 2, 3] will be profiledlyze the results and then answer the research ques-as List[Int], while that of [42, 3.14, ‘tokyo’]tion we addressed.

will be profiled as List[?].
For example, consider the following test code:

4. 1 Collecting Runtime Type Information
As the first step of the whole experiment, foreach repository we try to retrive runtime type information to help type inference in the type checking step. Our system infers function and method
types with the type information obtained at runtime. While runtime can only tell properties ofobjects under limited conditions, if collected runtime types during the execution can give consistenttypes to all variables, expressions and functions in
our type system, then we claim that these variables,
expressions and functions can be typed.
Yet running the application is a far more complicated task, fortunately unit test releases us so that
we can easily run the application. Unit test is a
software testing to validate that each unit of thesoftware performs as designed, quite lightweighted
but able to provide rich runtime information. Regarded as an alternative of static typing, unit test is
widely accepted and used by Python programmers.
While not all of the repositories in our dataset
are equipped with well-written unit tests, for those
repositories which have unit tests, we invoke theirtests by pytest [6], which is one of the most used
Python testing tool to build tests.
During the execution of unit tests, we inject

1
2
3
4
5
6

from PhoneMod import Phone
def test phonecall():phone = Phone()
phone.call(123456)
phone.call("police")

Class Phone, from a module PhoneMod, has amethod call and its instance invokes this methodwith an integer and a string, respectively, and bothwill return None.

When this piece of test codeis executed, method invocations are traced andtheir arguments and returns are profiled. In otherwords, the runtime type information of these two
method invocation will be observed as Phone →Int → None and Phone → Str → None.

Since

the method is invoked by the arguments with two
diﬀerent types, these types will be merged into aunion type and therefore the type of method callwill be inferred as Phone → Int ∨ Str → None.
As we mentioned before, unit test can only test
functions/methods under limited conditions, thus
our type inference from runtime may fail to infer
function/method types if not enough runtime information. However, if the given type information in
the unit test can consistently type the tested functions, such type inference can be practically feasible. Hence, in the following type checking and further analysis, we keep an optimistic attitude thatthe collected runtime type information can giveis applied (also being applied to If statement andconsistent types to functions/methods and assume

other branch statements in Python) following thethat the inferred function/method types are typed

semantics of the If expression.

correctly.

union type system, variable x can be well typed

Thanks to ouras Str ∨ Int.
4. 2 Type Checker
After collecting the runtime type information,

4. 3 Expressions

a static type checker is invoked to typecheck

In the following subsection, we will investigate

Python programs under each repository. The tar-

how expressions in the source code are typed inget programs are all valid .py files (an unvalid

order to better understand how our designed type

example could be setup.py file which is a spe-

system can typecheck programs. Here an expres-cial named script file for Python package man-sion is defined as typed if the checker evaluates oragement). We implement the static type checker

infers it into a type that is neither type error nor

in Python, parsing a .py file and applying thethe unknown type ?. For instance, an expression

typing rules described in Section 3. 5 for type-of type Int is judged as typed ; type (?

checking. For example, following T-INVK defined∨ ? is typed ; ? is not typed.

→ Float)in Section 3. 5, function calls and method invo-

The expressions we will evaluate are all Python

cations are checked by consistent-subtyping rela-expressions recognized by a parser. As a tiny ex-tion between the parameters and the given argu-

ample to show how count the expressions, consider

ments. For example, List[?] and List[Car] are of

the following piece of code

consistent-subtyping relation, while List[Person]and List[Car] are not.
1
2
3
4
5
6
7
8
9
10

from typing import Any, List
from mod import Car, Person
def runCars(arg: List[Car]) −> None:
pass

1
2
3
4
5
6
7

def fib(n):if n == 0:
return 0
elif n == 1:
return 1
else:
return fib(n−1) + fib(n−2)

which shows the definition of a function computing

lst1: List[Any]lst2: List[Person]
runCars(lst1) # OK
runCars(lst2) # Error!

the Fibonacci number. The number of expressions
inside the body of fib is counted as 16. Part of theexpressions can be n, 1, n-1, fib(n-1) and so on

In the above example, the function call at line 9 will
be totally fine while the call at line 10 will cause atype error raised by the checker.
Since the calculus described in Section 3 shows
only the core part of the Python language, one of
the uncovered typing rules is the flow-sensitive typing in the control flow. An example can be:1

x = "string" if condition else 42

at line 5.
The results show that there are totally 14,966,689
expressions in all repositories. 12,333,335 (82.4%)of the expressions are typed. The remaining expressions are 409,524 detected errors (1.4%) and
2,223,830 the unknown type ? (14.9%). The results reveal that most of the expressions in thereal-world Python programs can be well typed withIn the above code, variable x can be a string or in-static types under a gradual type system. Since

teger at runtime according to variable condition

our system is still under development, the detectedwhich has the type Bool.

static errors are believed to be false positive ones,

Flow-sensitive typingwhich are errors convicted by the checker but being

which is the second most union type of all sizes, isinnocent at runtime.

14,005, which indicates that optional type is morethan other union types larger than 2. The discov-

4. 4 Categorizing Unions

ery reveals that optional type is rather practical in

Here we want to focus on how many expressions

real-world Python programs.

are evaluated as union type according to our type

4. 4. 2 Large Unions

system. As shown in Fig. 1, the majority, totally

We randomly sampled the larger unions to fig-

452,840, of the union types has the size of 2, which

ure out what kinds of code snippets result in suchis 95.7% over all the union types. Additionally,large unions. Surprisingly, all such unions point toonly 0.19% (896 over 473,312) of the union types

the same object unittest.TestCase.assertEqual,

have the size larger than 10 and the largest unioneven those we sampled are from diﬀerent repos-

size reaches 49. These results suggest that most of

itories.

the objects can be handled with simple data types

TestCase defined in the builtin library unittest,

such as union type with commputable sizes and thewhich is unit test framework for constructing andprograms can be reasonably typed by a union typerunning tests. The method is called to check forsystem.

an expected result and its “ground truth” signatureassertEqual is a method in the classcan be roughly written as T → T → Bool, where T
is type variable defined by T = TypeVar(‘T’). The
scenario is that users heavily apply this function
to test equality for diverse objects of many types
T1 , ..., Tn .

Since our type inferencer blindly

merges all types into one union for tested functions, multiple invocations of the same function
at the test phase will be traced and therefore
the type of unittest.TestCase.assertEqual will
be inferred into type (T1 ∨ ...
Fig.1

Distribution graph of the union types

over size. The horizontal axis shows the size ofthe union type; The vertical axis shows thenumber...

∨ Tn ) → (T1 ∨∨ Tn ) → Bool, whose argument types areunions with many components.
Such observation can lead us to two meaningful
discussions. First, union type can handle most of
Python objects. Larger unions only corresponds to

4. 4. 1 Optional Typea smalle part of the whole and the vast majority

According to our data, 5.06% (22,896 overof them are the same object from a builtin library.

452,840) of the union types of size 2 are optional

Namely, user defined objects tend to be of literaltypes. Optional type is a quite common polymor-

types or smaller unions like optional type, whichphic type that can represents encapsulation of an

indicates that such a union type system can type-

optional value avaiable in many programming lan-check most of the Python programs within bounds.

guages. In Python, a value of type Option[T] refers

Second, a slightly enhanced type inference algo-

to a value which may result in of type T or None.

rithm can fluently bring higher accuracy to type

As comparison, the number of union type of size 3,

checking. Since the large unions all point to thesame object, or large unions are caused by a particular scenario, we can apply additional ad-hoc typ-6 Conclusion

ing rules upon our type system. A special typing

In this paper we argued that a simple, well de-rule can be, for example, unions of size larger than,signed type system that can mostly type Python

i.e. 10, are replaced with type parameters so that

programs. An empirical study on the static typewe can well type highly generic functions.

checking in Python was given to show a preliminary evident to support our statement. Our analy-

5 Related Works

sis quantitatively revealed the potency of a simple,

There has been enough attempts of static typing

union type system typing real-world Python pro-for dynamic languages. In this section we will in-grams.

troduce some of them that are targeted at Python.

Though our research have made progressive ac-

Mypy [5] is probably the best known static typecomplishment, more investigation should be carried

checker for Python based on gradual typing. It canout to strengthen our statement. Designed as a test

lift Python programs to a statical level and type

bed, it is imperative to investigate how other typecheck your code by adding type annotations. By

systems are qualified for Python programs. Be-

distributing type annotations with the program-sides, the amount of the dataset is not large enoughmer’s will, Mypy can smoothly mix dynamic andso that our current assessmemt is not highly convin-static typing in the program.

Our approach iscible. It is also beneficial to explore what specificbased on type inference so it does not force typepieces of code the type sytem is not able to type.

annotation.

All of those studies are our central future work.

There exists other works at type checking Python
programs with pure inference instead of requiring

参 考 文 献type annotations.

[1] DeMillo, R., Lipton, R. J., and Sayward, F.:
Hints on Test Data Selection: Help for the Practicing Programmer, Computer, Vol. 11(1978), pp. 34–
41.
[2] Frisch, A., Castagna, G., and Benzaken, V.: Semantic Subtyping: Dealing Set-Theoretically with
Function, Union, Intersection, and Negation Types,
J. ACM, Vol. 55, No. 4(2008).
[3] Garcia, R., Clark, A. M., and Tanter, E.: Abstracting Gradual Typing, SIGPLAN Not., Vol. 51,
No. 1(2016), pp. 429–442.
[4] MonkeyType: https://github.com/Instagram/MonkeyType.
[5] mypy: http://mypy-lang.org.
[6] pytest: https://docs.pytest.org/en/stable/.
[7] pytype: https://github.com/google/pytype.
[8] Siek, J. and Taha, W.: Gradual Typing for Objects, 08 2007, pp. 2–27.
[9] Siek, J. G.: Gradual Typing for Functional Languages, 2006.

One of the celebrated is Py-

type [7], which uses type inference instead of gradual typing.

Pytype generates ‘false-positive’ er-rors such as a late attribute initialization in a classdefinition, which from the perspective of the typechecker are, but from a programmer’s view are not.
Alternatively, Pytype allows users to inject specific comments to slicent such warning. Our design employs gradual typing and emphasizes that alight-weight type inferencer can handle most of the
Python programs.