Pierre Glaser, Gatsby Computational Neuroscience Unit
Python is a dynamically typed language, allowing for rapid prototyping at the cost of delegating error checking at runtime.
A similar structure can be observed in mathematical objects:
Given a commutative group $(E, +_E)$ over a field $(\mathbb F, +_F, \cdot_F) $, and an external law $\cdot: \mathbb F
\times E \longmapsto E$, E is called a $\mathbb F$-vector space if:
but when?
class TwoDVec:
def __init__(self, x, y):
self.x = x
self.y = y
def add(self, other):
return TwoDVec(self.x + other.x, self.y + other.y)
## the TwoDVec class complies with the following type system:
class TwoDVec:
x: float # important!
y: float # important!
def add(self: TwoDVec, other: TwoDVec) -> TwoDVec:
...
Type Safety can be enforced
# file 2Dvector.py
class TwoDVec:
def __init__(self, x, y):
self.x = x
self.y = y
def add(self, other):
return TwoDVec(self.x + other.x, self.y + other.y)
# file TwoDVec.pyi
# the folowing is a type rule: is ensures that all objects of the TwoDVec class verify the following rules:
class TwoDVec
x: float # important!
y: float # important!
def __init__(self, x: float, y: float) -> None: ...
def add(self: TwoDVec, other: TwoDVec) -> TwoDVec: ...
# file 2Dvector.py
class TwoDVec:
x: float
y: float
def add(self: TwoDVec, other: TwoDVec) -> TwoDVec:
return TwoDVec(self.x + other.x, self.y + other.y)
This code will behave the same as its untyped counterpart.
Let us now dig deeper into the structure of types and type systems.
class TwoDVec:
x: float
y: float
def add(self: "TwoDVec", other: "TwoDVec") -> "TwoDVec":
return TwoDVec(self.x + other.x, self.y + other.y)
TwoDVec: nullary type constructor.
TwoDVec elements called RateOfChange
class RateOfChange(TwoDVec):
x: float
y: float
def add(self: "RateOfChange", other: "RateOfChange") -> "RateOfChange":
return RateOfChange(self.x + other.x, self.y + other.y)
def total_change(self, T: float) -> "TwoDVec":
return TwoDVec(self.x * T, self.y * T)
Key Concept: Subtype Polymorphism: coercion subtype instances to their parent type should be possible.
from typing import Self
class ThreeDVec:
x: float
y: float
z: float
def add(self: Self, other: Self) -> Self:
return ThreeDVec(self.x + other.x, self.y + other.y, self.z + other.z)
from typing import Union
TwoOrThreeDVec = Union[TwoDVec, ThreeDVec]
def get_dimension(v: TwoOrThreeDVec) -> int:
return 2 isinstance(v, TwoDVec) else 3
Union: binary type constructor.
TwoOrThreeDVec a subtype of TwoDVec, or the other way around?
from typing import Tuple
TupleOfTwoDVec = Tuple[TwoDVec, TwoDVec]
def add(t: TupleOfTwoDVec) -> TwoDVec:
return t[0].add(t[1]) # valid
# return t[2].add(t[3]) # invalid
from typing import List
from typing_extensions import Self
from functools import reduce
ListOfTwoDVec = List[TwoDVec]
def add_all(l: ListOfTwoDVec) -> TwoDVec:
return reduce(lambda x, y: x.add(y), l)
TupleOfTwoDVec = Tuple[TwoDVec, TwoDVec]
TupleOfTwoOrThreeDVec = Tuple[TwoOrThreeDVec, TwoOrThreeDVec]
ListOfTwoDVec = List[TwoDVec]
ListOfTwoOrThreeDVec = List[TwoOrThreeDVec]
TupleOfTwoOrThreeDVec a subtype of TupleOfTwoDVec?ListOfTwoOrThreeDVec a subtype of ListOfTwoDVec?
To answer these questions, let us expose the type rules of
one by one.
class TupleOfTwoDVec:
def __getitem__(self, index: int) -> TwoDVec: ...
class TupleOfTwoOrThreeDVec:
def __getitem__(self, index: int) -> TwoOrThreeDVec: ...
tuple_of_two_d_vector: TupleOfTwoDVec = ...
tuple_of_two_or_three_d_vector: TupleOfTwoOrThreeDVec = ...
tuple_of_two_d_vector[0] returns a TwoDVec, which is a subtype of
TwoOrThreeDVec, and can thus be used in lieu of instances of such types.
TupleOfTwoDVec in place of TupleOfTwoOrThreeDVec.
⇒ There is a subtyping hierarchy for immutable product types.
class ListOfTwoDVec:
def __getitem__(self, index: int) -> TwoDVec: ...
def __setitem__(self, index: int, value: TwoDVec) -> ListOfTwoDVec: ...
class ListOfTwoOrThreeDVec:
def __getitem__(self, index: int) -> TwoOrThreeDVec: ...
def __setitem__(self, index: int, value: TwoDVec) -> ListOfTwoOrThreeDVec: ...
two_d_vector: TwoDVec = ...
two_or_three_d_vector: TwoOrThreeDVec = ...
l_2dvec: ListOfTwoDVec = ...
l_23dvec: ListOfTwoOrThreeDVec = ...
l_2dvec.set(l_23dvec) is not a syntax defined by the typing rules above. Thus,
ListOfTwoDVec is not a subtype of ListOfTwoOrThreeDVec.
ListOfTwoOrThreeDVec is not a subtype of ListOfTwoDVec because calling
l_23dvec[0] in lieu of l_2dvec[0] will return a supertype of
TwoDVec, and this thus not type safe.
⇒ No subtying hierarchy can be defined for mutable product types!
T a type variable, e.g. a variable whose array of possible concrete values is (for now) any type ( float, int, ...)
List[T] is a type whose array of possible concrete values is any type T for which List[T] is a valid type.
Careful! T is not a type, it is a type variable. Thus, List[T] is not a type, either.
let T be a Type Variable, and C be a unary type constructor (e.g. List).
For two type variables T1 and T2 we note T1≤ T2 if T1
is a subtype of T2 (a partial order on types). Then
C is covariant (w.r.t its argument) if T1≤ T2⇒C[T1]≤ C[T2] C is contravariant (w.r.t its argument) if T1≤ T2⇒C[T2]≤ C[T1] C is invariant if is is neither covariant nor contravariant.
In our case, Tuple is covariant (w.r.t its argument), while List is invariant. What type
constructor be contravariant?
from typing import TypeVar, Generic
T = TypeVar("T")
RealOrComplex = TypeVar("RealOrComplex", float, complex)
class TwoDVector(Generic[RealOrComplex]): # defines a type constructor/abstract type
x: RealOrComplex
y: RealOrComplex
def __init__(self, x: RealOrComplex, y: RealOrComplex):
self.x = x
self.y = y
def add(self, other: "TwoDVector[RealOrComplex]") -> "TwoDVector[RealOrComplex]":
return TwoDVector(self.x + other.x, self.y + other.y)
class RealTwoDVector(TwoDVector[float]): # concrete type
pass
class ComplexTwoDVector(TwoDVector[complex]): # ditto
pass
real_vec = RealTwoDVector(1.0, 2.0)
complex_vec = ComplexTwoDVector(1.0j, 2.0j)
real_vec.add(real_vec) # OK
real_vec.add(complex_vec) # type error
from typing import Callable
def inc(x: int) -> int:
return x + 1
def higher_order(f: Callable[[int], int], x: int) -> int:
return f(x)
ret = higher_order(inc, 1) # type safe
f is a function of type int -> int, or, in Python syntax, Callable[[int], int].
List and Tuple.