Type system concepts

Static, dynamic, and gradual typing

Astatically typed programming language runs a type checker before runninga program. The program is required to be well typed according to the language’stype system. The type system assigns a type to all expressions in the languageand verifies that their uses obey the typing rules. Normally, a program that isnot well typed (i.e., one that contains a type error) will not run. Java andC++ are examples of statically typed object-oriented languages.

Adynamically typed programming language does not run a type checker beforerunning a program. Instead, it checks the types of values before performingoperations on them at runtime. This is not to say that the language is“untyped”. Values at runtime have a type and their uses obey typing rules. Notevery operation will be checked, but certain primitive operations in thelanguage such as attribute access or arithmetic are. Python is adynamically typed language.

Gradual typing is a way to combine static and dynamic typing.Type-annotated Python allows opting in to static type checking at a fine levelof granularity, so that some type errors can be caught statically, withoutrunning the program. Variables, parameters, and returns can optionally be givenstatic type annotations. Even within the type of a single data structure,static type checking is optional and granular. For example, a dictionary can beannotated to enable static checking of the key type but only have dynamicruntime checking of the value type.

Agradual type system is one in which a special “unknown” or “dynamic” typeis used to describe names or expressions whose types are not known statically.In Python, this type is spelledAny. BecauseAny indicates astatically unknown type, the static type checker can’t check type correctnessof operations on expressions typed asAny. These operations are stilldynamically checked, via the Python runtime’s usual dynamic checking.

The Python type system also uses... withinCallable types andwithintuple[Any,...] (seeTuples) to indicate a statically unknowncomponent of a type. The detailed rules for these usages are discussed in theirrespective sections of the specification. Collectively, along withAny,these aregradual forms.

This specification describes a gradual type system for Python.

Fully static and gradual types

We will refer to types that do not contain agradual form as a sub-partasfully static types.

Agradual type can be a fully static type,Any itself, or a typethat contains a gradual form as a sub-part. All Python types are gradual types;fully static types are a subset.

Fully static types

A fully static type denotes a set of potential runtime values. For instance,the fully static typeobject is the set of all Python objects. The fullystatic typebool is the set of values{True,False}. The fully statictypestr is the set of all Python strings; more precisely, the set of allPython objects whose runtime type (__class__ attribute) is eitherstror a class that inherits directly or indirectly fromstr. AProtocol denotes the set of all objects which share a certain set ofattributes and/or methods.

If an objectv is a member of the set of objects denoted by a fully statictypeT, we can say thatv is a “member of” the typeT, orv“inhabits”T.

Gradual types

Any represents an unknown static type. It denotes some unknown set ofruntime values.

This may appear similar to the fully static typeobject, which representsthe set of all Python objects, but it is quite different.

If an expression has the typeobject, a static type checker should ensurethat operations on the expression are valid for all Python objects, or elseemit a static type error. This allows very few operations! For example, ifx is typed asobject,x.foo should be a static type error becausenot all Python objects have an attributefoo.

An expression typed asAny, on the other hand, should be assumed to have_some_ specific static type, but _which_ static type is not known. A statictype checker should not emit static type errors on an expression or statementifAny might represent a static type which would avoid the error. (Thisis defined more precisely below, in terms of materialization andassignability.)

Similarly, a type such astuple[int,Any] (seeTuples) orint|Any (seeUnion types) does not represent a single set of Pythonobjects; rather, it represents a (bounded) range of possible sets of values.

In the same way thatAny does not represent “the set of all Pythonobjects” but rather “an unknown set of objects”,tuple[int,Any] does notrepresent “the set of all length-two tuples whose first element is an integer”.That is a fully static type, spelledtuple[int,object]. By contrast,tuple[int,Any] represents some unknown set of tuple values; it might bethe set of all tuples of two integers, or the set of all tuples of an integerand a string, or some other set of tuple values.

In practice, this difference is seen (for example) in the fact that we canassign an expression of typetuple[int,Any] to a target typed astuple[int,int], whereas assigningtuple[int,object] totuple[int,int] is a static type error. (Again, we formalize this distinction in thebelow definitions of materialization and assignability.)

In the same way that the fully static typeobject is the upper bound forthe possible sets of values represented byAny, the fully static typetuple[int,object] is the upper bound for the possible sets of valuesrepresented bytuple[int,Any].

The gradual guarantee

Any allows gradually adding static types to a dynamically typed program.In a fully dynamically typed program, a static checker assigns the typeAny to all expressions, and should emit no errors. Inferring statictypes or adding type annotations to the program (making the program morestatically typed) may result in static type errors, if the program is notcorrect or if the static types aren’t able to fully represent the runtimetypes. Removing type annotations (making the program more dynamic) should notresult in additional static type errors. This is often referred to as thegradual guarantee.

In Python’s type system, we don’t take the gradual guarantee as a strictrequirement, but it’s a useful guideline.

Subtype, supertype, and type equivalence

A fully static typeB is asubtype of another fully static typeAif and only if the set of values represented byB is a subset of the set ofvalues represented byA. Because the subset relation on sets is transitiveand reflexive, the subtype relation is also transitive (ifC is a subtypeofB andB is a subtype ofA, thenC is a subtype ofA) andreflexive (A is always a subtype ofA).

Thesupertype relation is the inverse of subtype:A is a supertype ofB if and only ifB is a subtype ofA; or equivalently, if and onlyif the set of values represented byA is a superset of the valuesrepresented byB. The supertype relation is also transitive and reflexive.

We also define anequivalence relation on fully static types: the typesA andB are equivalent (or “the same type”) if and only ifA is asubtype ofB andB is a subtype ofA. This means that the set ofvalues represented byA is both a superset and a subset of the valuesrepresented byB, meaningA andB must represent the same set ofvalues.

We may describe a typeB as “narrower” than a typeA (or as a “propersubtype” ofA) ifB is a subtype ofA andB is not equivalenttoA. In the same scenario we can describe the typeA as “wider” thanB, or a “proper supertype” ofB.

Nominal and structural types

For a type such asstr (or any other class), which describes the set ofvalues whose__class__ isstr or a direct or indirect subclass of it,subtyping corresponds directly to subclassing. A subclassMyStr ofstris a subtype ofstr, becauseMyStr represents a subset of the valuesrepresented bystr. Such types can be called “nominal types” and this is“nominal subtyping.”

Other types (e.g.Protocols andTyped dictionaries) instead describe a setof values by the types of their attributes and methods, or the types of theirdictionary keys and values. These are called “structural types”. A structuraltype may be a subtype of another type without any inheritance or subclassingrelationship, simply because it meets all the requirements of the supertype,and perhaps adds more, thus representing a subset of the possible values of thesupertype. This is “structural subtyping”.

Although the means of specifying the set of values represented by the typesdiffers, the fundamental concepts are the same for both nominal and structuraltypes: a type represents a set of possible values and a subtype represents asubset of those values.

Materialization

SinceAny represents an unknown static type, it does not represent anyknown single set of values (it represents an unknown set of values). Thus it isnot in the domain of the subtype, supertype, or equivalence relations on statictypes described above.

To relate gradual types more generally, we define amaterializationrelation. Materialization transforms a “more dynamic” type to a “more static”type. Given a gradual typeA, if we replace zero or more occurrences ofAny inA with some type (which can be different for each occurrence ofAny), the resulting gradual typeB is a materialization ofA. (Wecan also materialize aCallable type by replacing... with any typesignature, and materializetuple[Any,...] by replacing it with adeterminate-length tuple type.)

For instance,tuple[int,str] (a fully static type) andtuple[Any,str](a gradual type) are both materializations oftuple[Any,Any].tuple[int,str] is also a materialization oftuple[Any,str].

IfB is a materialization ofA, we can say thatB is a “morestatic” type thanA, andA is a “more dynamic” type thanB.

The materialization relation is both transitive and reflexive, so it defines apreorder on gradual types.

Consistency

We define aconsistency relation on gradual types, based onmaterialization.

A fully static typeA is consistent with another fully static typeB ifand only if they are the same type (A is equivalent toB).

A gradual typeA is consistent with a gradual typeB, andB isconsistent withA, if and only if there exists some fully static typeCwhich is a materialization of bothA andB.

Any is consistent with every type, and every type is consistent withAny. (This follows from the definitions of materialization andconsistency but is worth stating explicitly.)

The consistency relation is not transitive.tuple[int,int] is consistentwithtuple[Any,int], andtuple[Any,int] is consistent withtuple[str,int], buttuple[int,int] is not consistent withtuple[str,int].

The consistency relation is symmetric. IfA is consistent withB,Bis also consistent withA. It is also reflexive:A is always consistentwithA.

The assignable-to (or consistent subtyping) relation

Given the materialization relation and the subtyping relation, we can definetheconsistent subtype relation over all types. A typeB is aconsistent subtype of a typeA if there exists a materializationA' ofA and a materializationB' ofB, whereA' andB' are bothfully static types, andB' is a subtype ofA'.

Consistent subtyping defines “assignability” for Python. An expression can beassigned to a variable (including passed as an argument or returned from afunction) if its type is a consistent subtype of the variable’s type annotation(respectively, parameter’s type annotation or return type annotation).

We can say that a typeB is “assignable to” a typeA ifB is aconsistent subtype ofA. In this case we can also say thatA is“assignable from”B.

In the remainder of this specification, we will usually prefer the termassignable to over “consistent subtype of”. The two are synonymous, but“assignable to” is shorter, and may communicate a clearer intuition to manyreaders.

For example,Any isassignable toint, becauseint is amaterialization ofAny, andint is a subtype ofint. The samematerialization also shows thatint is assignable toAny.

The assignable-to relation is not generally symmetric, however. IfB is asubtype ofA, thentuple[Any,B] is assignable totuple[int,A],becausetuple[Any,B] can materialize totuple[int,B], which is asubtype oftuple[int,A]. Buttuple[int,A] is not assignable totuple[Any,B].

For a gradual structural type, consistency and assignability are alsostructural. For example, the structural type “all objects with an attributex of typeAny” is consistent with (and assignable to) the structuraltype “all objects with an attributex of typeint”.

Summary of type relations

The subtype, supertype, and equivalence relations establish a partial order onfully static types. The analogous relations on gradual types (viamaterialization) are “assignable-to” (or “consistent subtype”),“assignable-from” (or “consistent supertype”), and “consistent with”. We canvisualize this analogy in the following table:

Fully static types

Gradual types

B is asubtype ofA

B isassignable to (or a consistent subtype of)A

A is asupertype ofB

A is assignable from (or a consistent supertype of)B

B isequivalent toA

B isconsistent withA

We can also define anequivalence relation on gradual types: the gradualtypesA andB are equivalent (that is, the same gradual type, notmerely consistent with one another) if and only if all materializations ofA are also materializations ofB, and all materializations ofBare also materializations ofA.

Attributes and methods

In Python, we can do more with objects at runtime than just assign them tonames, pass them to functions, or return them from functions. We can alsoget/set attributes and call methods.

In the Python data model, the operations that can be performed on a value alldesugar to method calls. For example,a+b is (roughly, eliding somedetails) syntactic sugar for eithertype(a).__add__(a,b) ortype(b).__radd__(b,a).

For a static type checker, accessinga.foo is a type error unless allpossible objects in the set represented by the type ofa have thefooattribute. (We consider an implementation of__getattr__ to be a getter forall attribute names, and similarly for__setattr__ and__delattr__.There are morecomplexities;a full specification of attribute access belongs in its own chapter.)

If all objects in the set represented by the fully static typeA have afoo attribute, we can say that the typeA has thefoo attribute.

If the typeA ofa ina.foo is a gradual type, it may not representa single set of objects. In this case,a.foo is a type error if and only ifthere does not exist any materialization ofA which has thefooattribute.

Equivalently,a.foo is a type error unless the type ofa is assignableto a type that has thefoo attribute.

Union types

Since accepting a small, limited set of expected types for a singleargument is common, the type system supports union types, created with the| operator.Example:

defhandle_employees(e:Employee|Sequence[Employee])->None:ifisinstance(e,Employee):e=[e]...

A fully static union typeT1|T2, whereT1 andT2 are fully statictypes, represents the set of values formed by the union of the sets of valuesrepresented byT1 andT2, respectively. Thus, by the definition of thesupertype relation, the unionT1|T2 is a supertype of bothT1 andT2, andT1 andT2 are both subtypes ofT1|T2.

A gradual union typeS1|S2, whereS1 andS2 are gradual types,represents all possible sets of values that could be formed by union of thepossible sets of values represented by materializations ofS1 andS2,respectively.

For any materialization ofS1 toT1 andS2 toT2,S1|S2can likewise be materialized toT1|T2. Thus, the gradual typesS1 andS2 are both assignable to the gradual union typeS1|S2.

IfB is a subtype ofA,B|A is equivalent toA.

This rule applies only to subtypes, not assignable-to. The unionT|Any isnot reducible to a simpler form. It represents an unknown static type withlower boundT. That is, it represents an unknown set of objects which maybe as large asobject, or as small asT, but no smaller.

Equivalent gradual types can, however, be simplified from unions; e.g.list[Any]|list[Any] is equivalent tolist[Any]. Similarly, the unionAny|Any can be simplified toAny: the union of two unknown sets ofobjects is an unknown set of objects.

Union with None

One common case of union types areoptional types, which are unions withNone. Example:

defhandle_employee(e:Employee|None)->None:...

Either the typeEmployee or the type ofNone are assignable to theunionEmployee|None.

A past version of this specification allowed type checkers to assume an optionaltype when the default value isNone, as in this code:

defhandle_employee(e:Employee=None):...

This would have been treated as equivalent to:

defhandle_employee(e:Employee|None=None)->None:...

This is no longer the recommended behavior. Type checkers should movetowards requiring the optional type to be made explicit.

Support for singleton types in unions

A singleton instance is frequently used to mark some special condition,in particular in situations whereNone is also a valid valuefor a variable. Example:

_empty=object()deffunc(x=_empty):ifxis_empty:# default argument valuereturn0elifxisNone:# argument was provided and it's Nonereturn1else:returnx*2

To allow precise typing in such situations, the user should usea union type in conjunction with theenum.Enum class providedby the standard library, so that type errors can be caught statically:

fromenumimportEnumclassEmpty(Enum):token=0_empty=Empty.tokendeffunc(x:int|None|Empty=_empty)->int:boom=x*42# This fails type checkifxis_empty:return0elifxisNone:return1else:# At this point typechecker knows that x can only have type intreturnx*2

Since the subclasses ofEnum cannot be further subclassed,the type of variablex can be statically inferred in all branchesof the above example. The same approach is applicable if more than onesingleton object is needed: one can use an enumeration that has more thanone value:

classReason(Enum):timeout=1error=2defprocess(response:str|Reason='')->str:ifresponseisReason.timeout:return'TIMEOUT'elifresponseisReason.error:return'ERROR'else:# response can be only str, all other possible values exhaustedreturn'PROCESSED: '+response

References

The concepts presented here are derived from the research literature in gradualtyping. See e.g.: