Safer Python

Intro
Asserts
Doctests
- Simple doctest
- More tricky doctests
Property tests
Enums
Dataclasses
Pydantic
Static types
Type-stub libraries
- More about types
- Interesting typing experiments in Python
Runtime types
- Comparison of libraries
- Examples
Combining compile and runtime types
AI and types
- Personal experience
- Pydantic AI
CrossHair
Dafny, Coq, etc extracting of Python code
Stronger "Python" is…
How to try it by self

Intro

The reason for most bugs is ignorance of how your language, your libraries, your OS, and your compiler work.
This happens because everything becomes too complicated.
To avoid it - use simple solutions and tools. Like… Python!
But how to make it… safer?

Asserts

Useful like in C, C++, etc:

import sys, traceback
def area(x, y):
    assert x and y, 'No any area!'   # TIP: or raise ValueError (exposed/API functions)
    return x * y
try:
    area(2, 0)
except Exception as x:
    print(*traceback.format_exception_only(x, file=sys.stdout))

AssertionError: No any area!

Doctests

Simple doctest

Regression tests
Tutorial and more illustrative documentation
AI friendly

It leads to unexpected exception:

def longest_word(s):
    '''Finds the longest word:

    >>> longest_word('w wow word word123')
    'word123'

    And for empty input string:
    
    >>> longest_word('')
    None
    '''
    words = s.split()
    return max(words, key=len)

import doctest; doctest.testmod(verbose=True)

Trying:
    longest_word('w wow word word123')
Expecting:
    'word123'
ok
Trying:
    longest_word('')
Expecting:
    None
**********************************************************************
File "<stdin>", line 9, in __main__.longest_word
Failed example:
    longest_word('')
Exception raised:
    Traceback (most recent call last):
      File "/usr/lib/python3.13/doctest.py", line 1395, in __run
        exec(compile(example.source, filename, "single",
        ~~~~^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
                     compileflags, True), test.globs)
                     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
      File "<doctest __main__.longest_word[1]>", line 1, in <module>
        longest_word('')
        ~~~~~~~~~~~~^^^^
      File "<stdin>", line 13, in longest_word
    ValueError: max() iterable argument is empty
1 item had no tests:
    __main__
**********************************************************************
1 item had failures:
   1 of   2 in __main__.longest_word
2 tests in 2 items.
1 passed and 1 failed.
***Test Failed*** 1 failure.

More tricky doctests

Expected exception, ellipsis:

def longest_word(s):
    '''Finds the longest word. It raises on empty string s:

    >>> longest_word('w wow word word123')  # doctest: +ELLIPSIS
    'word...'

    And for empty input string an exception is expected:
    
    >>> longest_word('')
    Traceback (most recent call last):
    ...
    ValueError: max() iterable argument is empty
    '''
    words = s.split()
    return max(words, key=len)

import doctest; doctest.testmod(verbose=True)

Trying:
    longest_word('w wow word word123')  # doctest: +ELLIPSIS
Expecting:
    'word...'
ok
Trying:
    longest_word('')
Expecting:
    Traceback (most recent call last):
    ...
    ValueError: max() iterable argument is empty
ok
1 item had no tests:
    __main__
1 item passed all tests:
   2 tests in __main__.longest_word
2 tests in 2 items.
2 passed.
Test passed.

You can write very complex tests even, integration tests if they use "fat" functions, so it looks compact enough

Property tests

Hypothesis comparing to QuickCheck

The best one Hypothesis - based on Haskell's QuickCheck but evolved substantially beyond it:

Tracks examples that trigger new behavior
Remembers previously interesting examples
Biases generation toward boundary cases
Replays known failures automatically
Can partially generate property tests for existing code

Shrinking:

Consistent behavior (search based)
Works automatically for composed structures
Usually finds dramatically smaller counterexamples

A Hypothesis test run is closer to:

generate (search vs QuickCheck's random)
observe behavior
adapt future generation
store interesting examples (in local "db" - to re-check them)
reuse them later

This is fundamentally different from classic QuickCheck.

Ideas behind Hypothesis

Imagine a parser bug only appears when:

length > 100
contains unicode
contains null byte

Pure random generation may take a long time to discover it. Hypothesis actively steers toward unusual and high-information examples.

Conjecture engine of Hypothesis

Hypothesis is built around an internal engine called Conjecture.

Instead of saying:

Generate an integer
Generate a string
Generate a list

Hypothesis effectively manipulates a stream of bytes and interprets it as structured data.

Conceptually:

bytes
↓
strategy
↓
object

This allows:

Uniform shrinking
Better exploration
More systematic search

QuickCheck generators generally operate directly at the value level.

Hypothesis examples

Simple example

from hypothesis import given, strategies as st

def my_sort(xs):
    return sorted(xs)

@given(st.lists(st.integers()))
def test_sort(xs):
    # `xs` will have values like:
    #   []
    #   [3]
    #   [1, 2, 3]
    #   [7, 7, 1]  etc.
    result = my_sort(xs)
    assert sorted(xs) == result
    assert all(result[i] <= result[i+1] for i in range(len(result)-1))

test_sort()

Bug-finding example with minimal counter-example

from hypothesis import given, strategies as st
import sys, traceback

def buggy_sort(xs):
    return list(set(xs))  # BUG: removes duplicates

@given(st.lists(st.integers()))
def test_sort(xs):
    assert sorted(xs) == buggy_sort(xs)

try:
    test_sort()
except Exception as x:
    print(*traceback.format_exception_only(x, file=sys.stdout))

AssertionError
 Falsifying example: test_sort(
     xs=[0, 0],
 )

Input size control

from hypothesis import given, strategies as st

@given(st.lists(st.integers(), max_size=10))
def test_small_lists(xs):
    assert len(xs) <= 10

test_small_lists()

Composed structures

from hypothesis import given, strategies as st

@given(st.lists(st.tuples(st.text(), st.integers())))
def test_pairs(data):
    assert isinstance(data, list) and all(isinstance(d, tuple) for d in data)

test_pairs()

Writes tests for you

Keywords: ghostwriter, fuzz (fuzzer).

Generates a test for functions that are inverses of each other (e.g., serializer/deserializer or encoder/decoder):

echo '#+begin_src python :results none'
hypothesis write --roundtrip json.dumps json.loads
echo '#+end_src'

# This test code was written by the `hypothesis.extra.ghostwriter` module
# and is provided under the Creative Commons Zero public domain dedication.

import json
import unittest
from hypothesis import given, strategies as st

# TODO: replace st.nothing() with an appropriate strategy


class TestRoundtripDumpsLoads(unittest.TestCase):

    @given(
        allow_nan=st.booleans(),
        check_circular=st.booleans(),
        cls=st.none(),
        default=st.none(),
        ensure_ascii=st.booleans(),
        indent=st.none(),
        obj=st.nothing(),
        object_hook=st.none(),
        object_pairs_hook=st.none(),
        parse_constant=st.none(),
        parse_float=st.none(),
        parse_int=st.none(),
        separators=st.none(),
        skipkeys=st.booleans(),
        sort_keys=st.booleans(),
    )
    def test_roundtrip_dumps_loads(
        self,
        allow_nan,
        check_circular,
        cls,
        default,
        ensure_ascii,
        indent,
        obj,
        object_hook,
        object_pairs_hook,
        parse_constant,
        parse_float,
        parse_int,
        separators,
        skipkeys,
        sort_keys,
    ):
        value0 = json.dumps(
            obj=obj,
            skipkeys=skipkeys,
            ensure_ascii=ensure_ascii,
            check_circular=check_circular,
            allow_nan=allow_nan,
            cls=cls,
            indent=indent,
            separators=separators,
            default=default,
            sort_keys=sort_keys,
        )
        value1 = json.loads(
            s=value0,
            cls=cls,
            object_hook=object_hook,
            parse_float=parse_float,
            parse_int=parse_int,
            parse_constant=parse_constant,
            object_pairs_hook=object_pairs_hook,
        )
        self.assertEqual(obj, value1)

Property test for associative, commutative, identity properties:

echo '#+begin_src python :results none'
hypothesis write --binary-op operator.add
echo '#+end_src'

# This test code was written by the `hypothesis.extra.ghostwriter` module
# and is provided under the Creative Commons Zero public domain dedication.

import operator
import unittest
from hypothesis import given, strategies as st

# TODO: replace st.nothing() with an appropriate strategy


class TestBinaryOperationadd(unittest.TestCase):
    add_operands = st.nothing()

    @given(a=add_operands, b=add_operands, c=add_operands)
    def test_associative_binary_operation_add(self, a, b, c):
        left = operator.add(a, operator.add(b, c))
        right = operator.add(operator.add(a, b), c)
        self.assertEqual(left, right)

    @given(a=add_operands, b=add_operands)
    def test_commutative_binary_operation_add(self, a, b):
        left = operator.add(a, b)
        right = operator.add(b, a)
        self.assertEqual(left, right)

    @given(a=add_operands)
    def test_identity_binary_operation_add(self, a):
        identity = "identity element here"
        self.assertEqual(a, operator.add(a, identity))
        self.assertEqual(a, operator.add(identity, a))

Uses predefined/template logic: checks idempotent, associativity, commutativity, identity element, code equivalency, duality (roundtrip), etc.

Enums

Enums restrict values to closed set of predefined values.

But a set is too wide term: we can treat them as a bit-fields/flags containers, strings containers, integers containers…

They exist: IntEnum, StrEnum, IntFlag, FlagBoundary, EnumDict, etc…

Alternative "old-school" approaches:

No grouping (just loose variables)
No type safety
Hard to discover valid values
Easy to mix unrelated constants
Boilerplate code

Example:

import enum

class Format(enum.Enum):       # simplest enum
    XML = 1                    # or use enum.auto() to avoid clashing
    JSON = 2
    TOML = 3
f = Format.JSON

class Distro(enum.StrEnum):    # Distro also is str
    DEBIAN = 'debian'
    MX = 'mx'
    GUIXOS = 'guixos'
    UNKNOWN = enum.auto()
print('Is Distro.DEBIAN a str?', isinstance(Distro.DEBIAN, str))
print(Distro.MX.capitalize() + ' linux!')

class Lang(enum.IntFlag):      # set of flags
    PYTHON = enum.auto()
    JAVA = enum.auto()
    GO = enum.auto()    

object_oriented = Lang.PYTHON  | Lang.JAVA
procedural = Lang.PYTHON | Lang.GO
print('Is Python object oriented?', Lang.PYTHON in object_oriented)
print('Is Go object oriented?', Lang.GO in object_oriented)

Is Distro.DEBIAN a str? True
Mx linux!
Is Python object oriented? True
Is Go object oriented? False

Dataclasses

They are close to the concept of Java, C# records, Scala case classes, Kotlin data classes. Think about them as about records.

Automatically generates are __init__, __repr__, __eq__, ordering methods (optional), __hash__ (depending on options), Haskell records (with deriving instances).

Better than any tuples:
1. fields have names
2. can be mutable (default) and immutable (frozen=True)
3. they can have methods
4. they can extend other classes
Better than named tuples: fields have types (NOTE: but since 3.5 NamedTuple supports types)
Better than plain classes: auto-generated magic methods

                         INCREASED SAFETY:

     tuples        ->       named tuples       ->      dataclasses
     ------                 ------------               -----------

('John', 31)           Person=namedtuple(              @dataclass
                         'Person',                     class Person(Human):
                         'name age')                     name:str
                       p = Person('Joe', 31)             age:int
                                                         def __str__(self):
                                                           return f'{self.name}, {self.age}'

                               BUT:

t:tuple[str,int] = \   Person=NamedTuple(
  ('John', 31)           'Person',
                         [('name', str),
                          ('age', int)])

Example:

import dataclasses

@dataclasses.dataclass(kw_only=True)
class Person:
    name:str
    age:int
    greeting:str=''
    def __post_init__(self):
        if self.age < 20: self.greeting = f'Hi, {self.name} !!'
        else:             self.greeting = f'How do you do, {self.name}.'
p1 = Person(name='John', age=15)
p2 = Person(name='Joe', age=35)
p3 = Person(name='John', age=15)
print(p1.greeting)
print(p2.greeting)
print(p1 == p2, p1 == p3)

Hi, John !!
How do you do, Joe.
False True

They are used for:

"value" objects
DTO (data transfer objects)
configuration objects
domain models
…

Pydantic

Features

Data validation library for Python
As FromJSON/ToJSON in Haskell and many-many more
Speed (core in written in Rust)
JSON schema emitting
ORM support (SQLAlchemy, Django ORM, Tortoise ORM)
Serialization/deserialization: JSON, Python (XML via extension)
8,000 packages in PyPI use it, 20 of 25 NASDAQ companies use it

Simple examples

From JSON

import pydantic
class FileLicenseTextSource(pydantic.BaseModel):
    'Locally obtained license text'
    file_url:str                # some URL
    location:None|int|str=None  # either line number of something other
try:
    flts = FileLicenseTextSource.model_validate_json(
        '{"file_url": "https://a.com/MIT.txt", "location": 123.12}')
except Exception as x:
    print(x)

2 validation errors for FileLicenseTextSource
location.int
  Input should be a valid integer, got a number with a fractional part [type=int_from_float, input_value=123.12, input_type=float]
    For further information visit https://errors.pydantic.dev/2.13/v/int_from_float
location.str
  Input should be a valid string [type=string_type, input_value=123.12, input_type=float]
    For further information visit https://errors.pydantic.dev/2.13/v/string_type

To JSON

import pydantic
class FileLicenseTextSource(pydantic.BaseModel):
    'Locally obtained license text'
    file_url:str                # some URL
    location:None|int|str=None  # either line number of something other
flts = FileLicenseTextSource(file_url='https://a.com/MIT.txt', location=123)
print(flts.model_dump_json())

{"file_url":"https://a.com/MIT.txt","location":123}

Nested models

import pydantic
class Address(pydantic.BaseModel):
    city: str
    zip: int
class User(pydantic.BaseModel):
    name: str
    age: int
    address: Address
data = {
    'name': 'Alice',
    'age': 30,
    'address': {
        'city': 'Sofia',
        'zip': 1000
    }
}
user = User(**data)
print(user)

name='Alice' age=30 address=Address(city='Sofia', zip=1000)

Discriminating unions

import pydantic, typing

class Circle(pydantic.BaseModel):
    type: typing.Literal['circle'] = 'circle'
    radius: float

class Rectangle(pydantic.BaseModel):
    type: typing.Literal['rectangle'] = 'rectangle'
    width: float
    height: float

Shape = Circle | Rectangle

# With `type` field:
s1 = pydantic.TypeAdapter(Shape).validate_python({'type': 'circle', 'radius': 5})
print(s1)
# !!! Without `type` field even:
s2 = pydantic.TypeAdapter(Shape).validate_python({'height': 14.8, 'width': 10.3})
print(s2)

type='circle' radius=5.0
type='rectangle' width=10.3 height=14.8

JSON schema

import pydantic, json
class FileLicenseTextSource(pydantic.BaseModel):
    'Locally obtained license text'
    file_url:str                # some URL
    location:None|int|str=None  # either line number of something other
sch = FileLicenseTextSource.model_json_schema()
print(json.dumps(sch, indent=2))

{
  "description": "Locally obtained license text",
  "properties": {
    "file_url": {
      "title": "File Url",
      "type": "string"
    },
    "location": {
      "anyOf": [
        {
          "type": "integer"
        },
        {
          "type": "string"
        },
        {
          "type": "null"
        }
      ],
      "default": null,
      "title": "Location"
    }
  },
  "required": [
    "file_url"
  ],
  "title": "FileLicenseTextSource",
  "type": "object"
}

Alternatives

msgspec (JSON, YAML, TOML, MessagePack)
marshmallow
dataclasses-json (old)

Static types

Basic idea of types

Programming: "static" contract
Logic: Curry-Howard correspondence:
- type is a proposition
- value is a proof of that proposition
- programs are proofs-as-constructions
Math: set together with the ways its elements can be constructed and used.
Category theory: types are objects, functions are morphisms

oranges:list[Orange] = apples  # BUG !

How types are checked

Compile time (C/C++, Java, Haskell, etc)
Type-checking mode/time (Python, Ruby, etc):

import typing
if typing.TYPE_CHECKING:
    # This block runs ONLY during static type checking (by pyright, mypy, etc)
    # and it does not run during Python execution (run time):
    from mymodule import HeavyDependency

which is useful to avoid errors like Failed importing ...: partially initialized module '...' related to circular import issues.

Type-check time assertions (proofs or "unit test for types"):

if typing.TYPE_CHECKING:
    r0:PackageToFilesRelationNode = RelationNode()                                # 1
    typing_extensions.assert_type(r0, RelationNode[L['PACKAGE'],list[L['FILE']]]) # 2
    r1:Node[L['RELATIONSHIP']] = r0                                               # 3

Assume r0 is a RelationNode[L['PACKAGE'], list[L['FILE']]] check that calling RelationNode() produces something compatible with that alias.
It forces the type checker to verify that r0 really is the expected specialized generic type.
RelationNode[...] is a subtype of Node[L['RELATIONSHIP']]

How to run it from a shell:

pyright source_dir

Where types help

cleaner design and architecture
fewer errors when writing code
SAFE REFACTORING!
better documentation, the code is easier to understand
VERY USEFUL FOR AI!
Include type-checking to your CI, together with doctests, unittests, property-tests…
Amazing IDE autocompletion and navigation (go to class/method/function/type of…)

Comparison of type checkers

Main features:

Type checker	Implementation	Speed	Type inference	Typing features
mypy	Python	Medium	Excellent	Excellent (PEP 484)
basedpyright	TypeScript	Very fast	Excellent	Excellent + stricter defaults
pyright	TypeScript	Very fast	Excellent	Excellent
ty	Rust	Extremely fast	Good (rapidly improving)	Good (still incomplete)
pytype	C++ + Python	Fast	Excellent	Good
pyre	OCaml	Very fast	Very good	Very good
pyanalyze	Python	Medium	Very good	Good
pytype2 (experimental)	Various	Experimental	Experimental	Experimental

Integration features:

Type checker	Plugins	Python support	IDE integration	Typical use
mypy	Excellent	Excellent	Excellent	General-purpose, library authors
basedpyright	No	Excellent	Excellent (VS Code, LSP)	Strict application development
pyright	No	Excellent	Excellent (VS Code, LSP)	Fast feedback during development
ty	No	Latest Python	LSP in progress	Future Ruff ecosystem
pytype	No	Good	Limited	Google codebases
pyre	Limited	Good	Good	Large Meta codebases
pyanalyze	Limited	Good	Limited	Bug finding, advanced analysis
pytype2 (experimental)	No	Experimental	Experimental	Research

Typing details:

Feature	mypy	pyright	basedpyright	ty	pytype	pyre	pyanalyze
Incremental checking	Yes	Yes	Yes	Planned	Limited	Yes	No
Daemon mode	Yes (dmypy)	LSP	LSP	Planned	No	Yes	No
Generic inference	Excellent	Excellent	Excellent	Good	Very good	Very good	Good
Literal types	Yes	Yes	Yes	Partial	Yes	Yes	Yes
Type narrowing	Good	Excellent	Excellent	Good	Good	Very good	Excellent
TypedDict	Yes	Yes	Yes	Partial	Yes	Yes	Yes
Protocols	Yes	Yes	Yes	Partial	Partial	Yes	Partial
Variadic generics	Yes	Yes	Yes	Partial	Partial	Partial	Partial
Plugins	Yes	No	No	No	No	Limited	Limited

Recommendations:

If you…	Recommended
Want the reference implementation	mypy
Want the fastest mature checker	basedpyright
Use VS Code	pyright or basedpyright
Write libraries for others	mypy
Want the strictest diagnostics	basedpyright
Work at Google	pytype
Work at Meta	pyre
Like Ruff and Rust tools	ty
Want additional bug-finding beyond typing	pyanalyze

Stability:

Checker	Stable Python API	Stable CLI	LSP
mypy	Yes	Yes	No
pyright	No	Yes	Yes
basedpyright	No	Yes	Yes
ty	Not yet	Yes	In progress

mypy remains the de facto reference implementation for Python's typing ecosystem. New PEPs are often implemented there first, and it has the richest plugin ecosystem.
Pyright is widely regarded as the fastest mature checker and has excellent type inference.
basedpyright is a fork of Pyright with stricter defaults, additional diagnostics, and a focus on catching more potential issues without requiring as much manual configuration.
ty is a relatively new Rust-based checker developed as part of the Ruff ecosystem. It's exceptionally fast, but as of mid-2026 it is still catching up to mypy and Pyright in terms of feature completeness.
pytype uses abstract interpretation and can infer types in code with few or no annotations, but it's primarily developed for Google's internal use cases.
Pyre emphasizes performance and scalability for very large repositories.
pyanalyze combines type checking with broader static analysis and can detect some classes of bugs that traditional type checkers do not.

Remember:

Type-checkers can be configured, their errors, warnings, the can be very strict or weak
Type-checkers can be extended with custom plugins allowing more complex type systems (think about dependent types, affined types…)
Different type-checkers can report different errors, warnings, either use only one or use multiple and try to satisfy them all

Examples of type based safety

Primitive examples

Assignment:

1: x:int = 'hello world'   # BUG: it is not int

mypy /tmp/tmp1.py || :

/tmp/tmp1.py:1: error: Incompatible types in assignment (expression has type "str", variable has type "int")  [assignment]
Found 1 error in 1 file (checked 1 source file)

Incorrect usage of a function possibly returning None:

1: import math
2: def safe_sqrt(n:int) -> None|float:
3:     return math.sqrt(n) if n >= 0 else None   # no more exception, just None
4: 2.5 + safe_sqrt(9)                            # BUG: 2.5 + None|float

mypy /tmp/tmp2.py || :

/tmp/tmp2.py:4: error: Unsupported operand types for + ("float" and "None")  [operator]
/tmp/tmp2.py:4: note: Right operand is of type "float | None"
Found 1 error in 1 file (checked 1 source file)

Wrong argument's type:

1: def size(x:tuple|list|str) -> int:
2:     if x is not None:           # IMPROVEMENT: you don't need this check anymore
3:         return len(x)
4: size(12)                        # BUG: int is not expected
5: size({1: 'a', 2:'b'}.get(100))  # BUG: {}.get() can return None, must be checked

mypy /tmp/tmp3.py || :

/tmp/tmp3.py:4: error: Argument 1 to "size" has incompatible type "int"; expected "tuple[Any, ...] | list[Any] | str"  [arg-type]
/tmp/tmp3.py:5: error: Argument 1 to "size" has incompatible type "str | None"; expected "tuple[Any, ...] | list[Any] | str"  [arg-type]
Found 2 errors in 1 file (checked 1 source file)

More precise standard containers:

 1: import typing, enum
 2: class Planet(enum.StrEnum):
 3:     Mars = 'Mars'
 4:     Earth = 'Earth'
 5:     Jupiter = 'Jupiter'
 6: planet_masses:dict[Planet,float] = {}
 7: planet_masses[Planet.Mars] = 6.42e23
 8: planet_masses[Planet.Earth] = 5.97e24
 9: planet_masses[Planet.Jupiter] = '1.90e24 tonnes'  # BUG: expected float, not str
10: planet_masses['Saturn'] = 68e26                   # BUG: expected enumerated Planet, not str

mypy /tmp/tmp4.py || :

/tmp/tmp4.py:9: error: Incompatible types in assignment (expression has type "str", target has type "float")  [assignment]
/tmp/tmp4.py:10: error: Invalid index type "str" for "dict[Planet, float]"; expected type "Planet"  [index]
Found 2 errors in 1 file (checked 1 source file)

Final values:

1: import typing
2: pi:typing.Final = 3.14
3: pi = 3                  # BUG: cannot re-assign final value

mypy /tmp/tmp4_0.py || :

/tmp/tmp4_0.py:3: error: Cannot assign to final name "pi"  [misc]
Found 1 error in 1 file (checked 1 source file)

Advanced types usage

Wrapper-types for correct algorithms chaining:

 1: import typing
 2: 
 3: class SortedList(list):
 4:     def __init__(self, items):
 5:         super().__init__(sorted(items))
 6: 
 7: def unique(data: SortedList) -> SortedList:
 8:     res: SortedList = SortedList([])
 9:     for x in data:
10:         if res and x == res[-1]: continue
11:         else: res.append(x)
12:     return res
13: items = [11, 20, 11, 20, 1, 20, 11, 5, 1]
14: sorted_items = SortedList(items)
15: print(unique(items))             # BUG: expected SortedList so unique() works correctly
16: print(unique(sorted_items))

[11, 20, 11, 20, 1, 20, 11, 5, 1]
[1, 5, 11, 20]

mypy /tmp/tmp5.py || :

/tmp/tmp5.py:15: error: Argument 1 to "unique" has incompatible type "list[int]"; expected "SortedList"  [arg-type]
Found 1 error in 1 file (checked 1 source file)

Distinct, refined types avoiding multiple checks (or "ensure"-functions) - refinement happens only once on the edge of the domain where external raw data is transformed to internal typed form:

 1: import typing
 2: ReadableName = typing.NewType('ReadableName', str)  # DISTINCT TYPE: or a class
 3: def readable_name(raw_str:str) -> ReadableName:     # IDEAS: capitalized, stripped, ...
 4:     res = ' '.join(s.strip().capitalize() for s in raw_str.split() if s)
 5:     return ReadableName(res)
 6: def greating(n:ReadableName):
 7:     # n = readable_name(n)                          # REDUNDANT: we don't need it more
 8:     print(f'Hello {n}, how are you?')
 9: def closing(n:ReadableName):
10:     # n = readable_name(n)                          # REDUNDANT: we don't need it more
11:     print(f'-- Best regards,\n--  {n}')
12: r = '   michael   dudikoff  '
13: n = readable_name(r)                                # ONCE: on the edge, raw -> internal/trusted
14: greating(n)                                         # OK
15: closing(n)                                          # OK
16: greating(r)                                         # BUG: expected ReadableName

Hello Michael Dudikoff, how are you?
-- Best regards,
--  Michael Dudikoff
Hello    michael   dudikoff  , how are you?

mypy /tmp/tmp6.py || :

/tmp/tmp6.py:16: error: Argument 1 to "greating" has incompatible type "str"; expected "ReadableName"  [arg-type]
Found 1 error in 1 file (checked 1 source file)

Refined, strongly typed math:

1: import typing, math
2: Positive = typing.NewType('Positive', float)
3: def make_positive(x:int|float) -> Positive | None:  # SMART CONSTRUCTOR
4:     return Positive(x) if x >= 0 else None
5: def safe_sqrt(n:Positive) -> Positive:
6:     return Positive(math.sqrt(n))
7: safe_sqrt(4)                                        # BUG: expected strongly typed Positive
8: p = make_positive(4)                                # ONCE: on the edge
9: if p: safe_sqrt(p)                                  # USE: only trusted, refined value

mypy /tmp/tmp7.py || :

/tmp/tmp7.py:7: error: Argument 1 to "safe_sqrt" has incompatible type "int"; expected "Positive"  [arg-type]
Found 1 error in 1 file (checked 1 source file)

Another classic example with non-empty containers:

 1: import typing
 2: 
 3: class Comparable(typing.Protocol):
 4:     def __lt__(self, other: typing.Any, /) -> bool: ...
 5: 
 6: class NonEmptyList[A](list[A]): pass
 7: 
 8: def make_non_empty[A](x:list[A]) -> NonEmptyList[A] | None:
 9:     return NonEmptyList(x) if x else None
10: 
11: def safe_max[A:Comparable](n:NonEmptyList[A]) -> A:
12:     return max(n)
13: 
14: print(safe_max([1,2]))                              # BUG: expected strongly typed NonEmptyList
15: n = make_non_empty([1,2])                           # ONCE: on the edge
16: if n: print(safe_max(n))                            # USE: only trusted, refined value

But here we will use PyRight, because MyPy does not fully support it and it has a regression:

pyright /tmp/tmp8.py || :

/tmp/tmp8.py
  /tmp/tmp8.py:14:16 - error: Argument of type "list[int]" cannot be assigned to parameter "n" of type "NonEmptyList[A@safe_max]" in function "safe_max"
    "list[int]" is not assignable to "NonEmptyList[A@safe_max]" (reportArgumentType)
1 error, 0 warnings, 0 informations

Units of measurement:

def area(w: Meter, h: Meter) -> SquareMeter: ...

Still mostly experimental, the mature production level implementation is in F#.

See libraries about refined and phantom types:

Typing KungFu

       S I M P L E   U S A G E   O F   T Y P E S
     [v e r y   s h o r t   c o d e    r o u t e]

                 pass     expect
                value    some type
                  o--------->o

     A D V A N C E D   U S A G E   O F   T Y P E S
  ⎡ l o n g   c o m p l e x   c o d e   r o u t e s ⎤
  ⎣ o r   b i g   c o n s i s t e n c e   f o r m s ⎦
     
  state    state1            state3      never
  zero             state2      or        state5
    o------->o------->o      state4   from state3,4
                      `-------->o . . . . . o
                      `-------->o

States control in compile time:

let's imagine the next domain - we have an empty scene that can be cluttered with objects, objects can be "dressed" (by a texture), if they are textured then they can be illuminated by a light, and only after illuminating the scene can be rendered.

Transitions between scene's states are:

Empty-Scene       Cluttered            Textured    Illuminated    Rendered
     ║                ║                    ║            ║             ║
     ║----object----->║----object----.     ║            ║             ║
     ║                ║<-------------'     ║            ║             ║
     ║                ║                    ║            ║             ║
     ║                ║<------object-------║            ║             ║
     ║                ║                    ║            ║             ║
     ║                ║-------texture----->║---light--->║---render--->║

 1: import typing, dataclasses
 2: 
 3: Empty = typing.Literal['Empty']
 4: Cluttered = typing.Literal['Cluttered']
 5: Textured = typing.Literal['Textured']
 6: Illuminated = typing.Literal['Illuminated']
 7: Rendered = typing.Literal['Rendered']
 8: 
 9: SceneState = Empty | Cluttered | Textured | Illuminated | Rendered
10: 
11: @dataclasses.dataclass
12: class Scene[T:SceneState=Empty]:  # default constructor produces Empty scene
13:     objects:list[str]
14: 
15: def put_object(s:Scene[Empty|Cluttered|Textured]) -> Scene[Cluttered]:
16:     return Scene(objects=s.objects + [f'obj{len(s.objects)}'])
17: 
18: def texture_objects(s:Scene[Cluttered], texture:str) -> Scene[Textured]:
19:     return Scene(objects=[f'{o.split("-")[0]}-{texture}' for o in s.objects])
20: 
21: def light(s:Scene[Textured]) -> Scene[Illuminated]:
22:     return Scene(objects=[o.upper() for o in s.objects])  # "lighting" make them upper case!
23:     
24: def render(s:Scene[Illuminated]) -> Scene[Rendered]:
25:     print(s.objects)
26:     return Scene(objects=s.objects)  # imitate change of the state
27: 
28: # This is fully fine rendered scene with 2 textured objects, we
29: # expect to see:
30: #   ['OBJ0-BRICK', 'OBJ1-BRICK']:
31: s0:Scene[Rendered] = \
32:     render(light(texture_objects(
33:         put_object(put_object(
34:             Scene(objects=[]))), 'brick')))
35: 
36: # BUG: not fine - we cannot light after put of non-textured object in
37: # textured scene - it returns us back to Cluttered (non-textured) scene,
38: # without type-check it produces OBJ2 illuminated but without a texture:
39: #   ['OBJ0-BRICK', 'OBJ1-BRICK', 'OBJ2']
40: render(light(
41:     put_object(texture_objects(
42:         put_object(put_object(
43:             Scene(objects=[]))), 'brick'))))
44: 
45: # BUG: no way to light scene before to texture it,
46: # without type-check it produces illuminated objects but without textures:
47: #   ['OBJ0', 'OBJ1']
48: render(light(
49:     put_object(put_object(
50:         Scene(objects=[])))))
51: 
52: # BUG: no way to render scene before to illuminate it,
53: # without type-check it produces textured objects but in full darkness:
54: #   ['obj0-brick', 'obj1-brick']
55: render(texture_objects(
56:     put_object(put_object(
57:         Scene(objects=[]))), 'brick'))

['OBJ0-BRICK', 'OBJ1-BRICK']
['OBJ0-BRICK', 'OBJ1-BRICK', 'OBJ2']
['OBJ0', 'OBJ1']
['obj0-brick', 'obj1-brick']

pyright /tmp/tmp9.py || :

/tmp/tmp9.py
  /tmp/tmp9.py:41:5 - error: Argument of type "Scene[Cluttered]" cannot be assigned to parameter "s" of type "Scene[Textured]" in function "light"
    "Scene[Cluttered]" is not assignable to "Scene[Textured]"
      Type parameter "T@Scene" is covariant, but "Cluttered" is not a subtype of "Textured"
        "Cluttered" is not assignable to type "Textured" (reportArgumentType)
  /tmp/tmp9.py:49:5 - error: Argument of type "Scene[Cluttered]" cannot be assigned to parameter "s" of type "Scene[Textured]" in function "light"
    "Scene[Cluttered]" is not assignable to "Scene[Textured]"
      Type parameter "T@Scene" is covariant, but "Cluttered" is not a subtype of "Textured"
        "Cluttered" is not assignable to type "Textured" (reportArgumentType)
  /tmp/tmp9.py:55:8 - error: Argument of type "Scene[Textured]" cannot be assigned to parameter "s" of type "Scene[Illuminated]" in function "render"
    "Scene[Textured]" is not assignable to "Scene[Illuminated]"
      Type parameter "T@Scene" is covariant, but "Textured" is not a subtype of "Illuminated"
        "Textured" is not assignable to type "Illuminated" (reportArgumentType)
3 errors, 0 warnings, 0 informations

Example modeling animal breeding. We have species: a lion, a tiger, a donkey, a horse, and some of them can have offsprings, some - cannot. The table of breeding:

male	female	offspring
Lion	Tiger	Liger
Tiger	Lion	Tigon
Donkey	Horse	Mule
Horse	Donkey	Hinny
N	N	N

and animals will have nicknames. Let's model it:

 1: import typing, dataclasses
 2: 
 3: class Species: ...
 4: class Lion(Species): ...
 5: class Tiger(Species): ...
 6: class Liger(Species): ...
 7: class Tigon(Species): ...
 8: class Donkey(Species): ...
 9: class Horse(Species): ...
10: class Mule(Species): ...
11: class Hinny(Species): ...
12: 
13: S = typing.TypeVar('S', bound=Species) # TIP: Species is kind of S
14: 
15: @dataclasses.dataclass
16: class Animal(typing.Generic[S]):
17:     nick: str
18: 
19: # Play role of type-level functions encoding the table of breeding
20: # statically in type-check time (not runtime!):
21: 
22: @typing.overload
23: def offspring(male: Animal[Lion], female: Animal[Tiger], nick: str) -> Animal[Liger]: ...
24: 
25: @typing.overload
26: def offspring(male: Animal[Tiger], female: Animal[Lion], nick: str) -> Animal[Tigon]: ...
27: 
28: @typing.overload
29: def offspring(male: Animal[Donkey], female: Animal[Horse], nick: str) -> Animal[Mule]: ...
30: 
31: @typing.overload
32: def offspring(male: Animal[Horse], female: Animal[Donkey], nick: str) -> Animal[Hinny]: ...
33: 
34: @typing.overload
35: def offspring(male: Animal[S], female: Animal[S], nick: str) -> Animal[S]: ...
36: 
37: def offspring(male: Animal, female: Animal, nick: str) -> Animal:
38:     return Animal(nick)
39: 
40: a1 = Animal[Tiger]('Shere Khan')
41: a2 = Animal[int]('Inty')                # BUG: Species cannot be int, only Lion, Tiger, ...
42: o1 = offspring(Animal[Donkey]('Snag'),
43:                Animal[Horse]('Jinnah'),
44:                'Bud')
45: typing.reveal_type(o1)                  # Mule!
46: o2 = offspring(Animal[Horse]('Night'),
47:                Animal[Donkey]('Lisa'),
48:                'Cat')
49: typing.reveal_type(o2)                  # Hinny!
50: o3 = offspring(Animal[Horse]('Night'),
51:                Animal[Horse]('Donna'),
52:                'Cadger')
53: typing.reveal_type(o3)                  # Horse!
54: o4 = offspring(Animal[Horse]('Night'),  # BUG: Horse and Tiger have not offsprings
55:                Animal[Tiger]('Leonna'),
56:                'Cadger')

pyright /tmp/tmp10_0.py || :

/tmp/tmp10_0.py
  /tmp/tmp10_0.py:41:13 - error: Type "int" cannot be assigned to type variable "S@Animal"
    Type "int" is not assignable to upper bound "Species" for type variable "S@Animal"
      "int" is not assignable to "Species" (reportInvalidTypeArguments)
  /tmp/tmp10_0.py:45:20 - information: Type of "o1" is "Animal[Mule]"
  /tmp/tmp10_0.py:49:20 - information: Type of "o2" is "Animal[Hinny]"
  /tmp/tmp10_0.py:53:20 - information: Type of "o3" is "Animal[Horse]"
  /tmp/tmp10_0.py:54:6 - error: No overloads for "offspring" match the provided arguments (reportCallIssue)
  /tmp/tmp10_0.py:55:16 - error: Argument of type "Animal[Tiger]" cannot be assigned to parameter "female" of type "Animal[S@offspring]" in function "offspring"
    "Animal[Tiger]" is not assignable to "Animal[Horse]"
      Type parameter "S@Animal" is invariant, but "Tiger" is not the same as "Horse" (reportArgumentType)
3 errors, 0 warnings, 3 informations

Another similar example:

 1: import typing
 2: 
 3: @typing.overload
 4: def fetch_from_net(url:str, encoding:None=None) -> bytes: ...
 5: 
 6: @typing.overload
 7: def fetch_from_net(url:str, encoding:str) -> str: ...
 8: 
 9: def fetch_from_net(url:str, encoding:str|None=None) -> str|bytes:
10:     if encoding is None: return b'Imagine we fetched this'
11:     else: return 'Imagine we fetched this'
12: 
13: s1:str = '\n'.join(['Result:', fetch_from_net('https://no.such', encoding='utf-8')])
14: s2:str = '\n'.join(['Result:', fetch_from_net('https://no.such')])  # BUG: join of str and bytes

pyright /tmp/tmp10.py || :

/tmp/tmp10.py
  /tmp/tmp10.py:14:10 - error: No overloads for "join" match the provided arguments (reportCallIssue)
  /tmp/tmp10.py:14:32 - error: Argument of type "list[str | bytes]" cannot be assigned to parameter "iterable" of type "Iterable[str]" in function "join"
    "bytes" is not assignable to "str" (reportArgumentType)
2 errors, 0 warnings, 0 informations

Structural equivalence is very useful when you use objects from some libraries that you cannot modify, for example - every object having these attributes (or properties) will be treated as a class (successor) of these (WebSource, FileSource) classes.

You qualify (by a type) existing (library) classes for type-check time:

 1: import typing, socket
 2: 
 3: @typing.runtime_checkable  # can be used in run-time with isinstance()
 4: class TcpSource(typing.Protocol):
 5:     @property
 6:     def port(self) -> int: ...
 7:     @property
 8:     def ip(self) -> str: ...
 9: 
10: @typing.runtime_checkable
11: class SocketSource(typing.Protocol):
12:     @property
13:     def socket(self) -> socket.socket: ...
14: 
15: def read_from_net(src:TcpSource|SocketSource) -> str:
16:     if isinstance(src, TcpSource):
17:         return f'Read from TcpSource {src.ip}:{src.port}'
18:     elif isinstance(src, SocketSource):
19:         return f'Read from SocketSource'
20:     else:
21:         return '<nothing>'
22: 
23: class LibTcpSrc:
24:     port = 8080
25:     ip = '127.0.0.1'
26: 
27: class UnsuitableTcpSrc:                   # TIP: does not support TcpSource protocol:
28:     port_number = 8080                    # there are no expected properties of it !
29:     def get_ip(self): return '127.0.0.1'
30:     
31: print(read_from_net(LibTcpSrc()))         # OK: can be treated as TcpSource
32: print(read_from_net(UnsuitableTcpSrc()))  # BUG: neither SocketSource nor TcpSource

Read from TcpSource 127.0.0.1:8080
<nothing>

pyright /tmp/tmp11.py || :

/tmp/tmp11.py
  /tmp/tmp11.py:32:21 - error: Argument of type "UnsuitableTcpSrc" cannot be assigned to parameter "src" of type "TcpSource | SocketSource" in function "read_from_net"
    Type "UnsuitableTcpSrc" is not assignable to type "TcpSource | SocketSource"
      "UnsuitableTcpSrc" is incompatible with protocol "TcpSource"
        "port" is not present
        "ip" is not present
      "UnsuitableTcpSrc" is incompatible with protocol "SocketSource"
        "socket" is not present (reportArgumentType)
1 error, 0 warnings, 0 informations

Typed dictionaries are another way to typify something traditionally raw and error prone - dictionaries. It is useful within business applications full of large JSON files, huge XML data… TypedDict allows to define typed and flexible dictionaries with required and optional keys:

 1: import typing
 2: class Person(typing.TypedDict, total=False):
 3:     name: typing.Required[str]
 4:     email: typing.Required[str]
 5:     age: int
 6: def print_person(p:Person):
 7:     try:
 8:         age = f', {p["age"]}' if 'age' in p else ''
 9:         print(f'NAME: {p["name"]}{age}')
10:         print(f'EMAIL: {p["email"]}')
11:         print('----------')
12:     except Exception as x:
13:         print(f'Cannot print to the end {p}: {x}')
14: p0:Person = {'name': 'Axel', 'email': 'axel@fake.com'}
15: print_person(p0)
16: p1:Person = {'name': 'John', 'email': 'john@fake.com', 'age': 40, 'gender': 'male'} # BUG: gender is superfluous
17: print_person(p1)
18: p2:Person = {'name': 'John', 'age': 40}                                             # BUG: no email
19: print_person(p2)

NAME: Axel
EMAIL: axel@fake.com
----------
NAME: John, 40
EMAIL: john@fake.com
----------
NAME: John, 40
Cannot print to the end {'name': 'John', 'age': 40}: 'email'

pyright /tmp/tmp12.py || :

/tmp/tmp12.py
  /tmp/tmp12.py:16:67 - error: Type "dict[str, str | int]" is not assignable to declared type "Person"
    "gender" is an undefined item in type "Person" (reportAssignmentType)
  /tmp/tmp12.py:18:13 - error: Type "dict[str, str | int]" is not assignable to declared type "Person"
    "email" is required in "Person" (reportAssignmentType)
2 errors, 0 warnings, 0 informations

Final cases (reminds Common Lisp's ecase and etypecase but for type-check time, more relevant is exhaustive switch of Java) - very helpful when refactoring happens:

 1: import typing
 2: 
 3: # Initial implementation:
 4: class Name(str): pass
 5: class Nick(str): pass
 6: 
 7: # Then, during refactoring, I added FullName:
 8: class FullName(str): pass
 9: type Moniker = Name | Nick | FullName
10: 
11: # BUGGY CODE AFTER REFACTORING: in another module I had this case-analysis:
12: def print_moniker(m:Moniker):
13:     match m:
14:         case Name(): print(f'Name is {m}')
15:         case Nick(): print(f'Nick is {m}')
16:         case _:      typing.assert_never(m)  # BUG: FullName cannot be Never
17: print_moniker(Nick('maverick'))
18: print_moniker(FullName('Alex Johnson'))      # BUG: nothing printed + assert_never raises

Nick is maverick

mypy /tmp/tmp13.py || :

/tmp/tmp13.py:16: error: Argument 1 to "assert_never" has incompatible type "FullName"; expected "Never"  [arg-type]
Found 1 error in 1 file (checked 1 source file)

Type-guards refine types for an underlying branch:

 1: import typing, json, collections.abc as C
 2: 
 3: def check_indexes(size:int, nums:C.Iterable[int]) -> bool:
 4:     return min(nums) >= 0 and max(nums) < size if nums else True
 5: 
 6: def are_indexes(something) -> typing.TypeGuard[C.Iterable[int]]:
 7:     return (isinstance(something, C.Iterable) and
 8:             all(isinstance(el, int) for el in something))
 9: # IMPORTANT: without object typing x1,x2 are Any, which prevents their type-check:
10: x1:object = json.loads('[1,2,3,4,5]')       # Simulate external source
11: x2:object = json.loads('["a", "b", "c"]')   # Simulate external source
12: try:
13:     if are_indexes(x1):                     # x1 is object
14:         print('1:', check_indexes(10, x1))  # ...but if I enter "if", x1 is Iterable[int]
15:     if are_indexes(x2):                     # x2 is object
16:         print('2:', check_indexes(10, x2))  # ...but if I enter "if", x2 is Iterable[int]
17:     print('3:', check_indexes(10, x1))      # BUG: unsure Iterable[int]
18:     print('4:', check_indexes(10, x2))      # BUG: unsure Iterable[int] + raises
19: except Exception as x:
20:     print(f'ERROR: {x}')

1: True
3: True
ERROR: '>=' not supported between instances of 'str' and 'int'

mypy /tmp/tmp14.py || :

/tmp/tmp14.py:17: error: Argument 2 to "check_indexes" has incompatible type "object"; expected "Iterable[int]"  [arg-type]
/tmp/tmp14.py:18: error: Argument 2 to "check_indexes" has incompatible type "object"; expected "Iterable[int]"  [arg-type]
Found 2 errors in 1 file (checked 1 source file)

Another example clarifying external dictionaries:

 1: import typing, json
 2: 
 3: class Person(typing.TypedDict):
 4:     name: str
 5:     surname: typing.NotRequired[str]
 6: 
 7: def is_person(d:object) -> typing.TypeGuard[Person]:
 8:     return isinstance(d, dict) and isinstance(d.get('name'), str)
 9: 
10: # IMPORTANT: force type-checking with object instead of default Any:
11: xs:list[object] = [json.loads('{"name": "John", "surname": "Doe"}'),
12:                    json.loads('{"email": "steve@apple.com"}')]
13: for x in xs:                            # x is object
14:     if is_person(x):                    # skips x that are not Person
15:         print('Name:', x['name'])       # here x is the typed dict Person
16:         if surname := x.get('surname'): # ...with optional surname key
17:             print('Surname:', surname)
18: try:
19:     for x in xs:                        # x is any object
20:         print('Name:', x['name'])       # BUG: x being object forces report "x is not indexable"
21:         if surname := x.get('surname'): # BUG: and x can miss .get()
22:             print('Surname:', surname)
23: except Exception as x:
24:     print(f'ERROR: {x}!')               # BUG: I hit it bcs some x is not dict like Person

Name: John
Surname: Doe
Name: John
Surname: Doe
ERROR: 'name'!

mypy /tmp/tmp15.py || :

/tmp/tmp15.py:20: error: Value of type "object" is not indexable  [index]
/tmp/tmp15.py:21: error: "object" has no attribute "get"  [attr-defined]
Found 2 errors in 1 file (checked 1 source file)

Terminal branches leading to unreachable code:

 1: import typing
 2: 
 3: @typing.overload
 4: def report_error(error:str, exception:type[Exception]) -> typing.NoReturn: ...
 5: @typing.overload
 6: def report_error(error:str, exception:None=None) -> None: ...
 7: def report_error(error:str, exception:None|type[Exception]=None) -> None:
 8:     if exception is None:
 9:         print(f'ERROR HAPPENS, GUYS: {error}')
10:         return None                       # TIP: to satisfy MyPy
11:     else:
12:         raise exception(error)
13: 
14: report_error('No data')
15: report_error('No data again', ValueError) # here an exception will be thrown, so -
16: report_error('No data')                   # WARN: statement is unreachable!

ERROR HAPPENS, GUYS: No data

Pay attention that I add the option --warn-unreachable:

mypy --warn-unreachable /tmp/tmp16.py || :

/tmp/tmp16.py:16: error: Statement is unreachable  [unreachable]
Found 1 error in 1 file (checked 1 source file)

Types can be used for introspections and different tricks with help of annotations. Use-cases:

ORM
Dependency injections
Routing
Serialization/deserialization/validation
IDE integration/documentation
Hooks/callbacks/chaining
Optimization hints
Code generation
DSL
Custom type systems (dependent types, etc)
…

from typing import Annotated

class PrimaryKey: pass
class Indexed: pass

class User:
    id: Annotated[int, PrimaryKey()]  # int, but with extra-metadata marked it as a primary key
    email: Annotated[str, Indexed()]  # str, but with extra-metadata marked it as an index

@validate
def set_age(age: Annotated[int, Between(0, 120)]): # args also can be Annotated
    return age

3rd party DSL for Annotated: annotated-types (standardized DSL for complex refined types):

from typing import Annotated
from annotated_types import Gt, Len, Predicate

class MyClass:
    age: Annotated[int, Gt(18)]                         # Valid: 19, 20, ...
                                                        # Invalid: 17, 18, "19", 19.0, ...
    factors: list[Annotated[int, Predicate(is_prime)]]  # Valid: 2, 3, 5, 7, 11, ...
                                                        # Invalid: 4, 8, -2, 5.0, "prime", ...

    my_list: Annotated[list[int], Len(0, 10)]           # Valid: [], [10, 20, 30, 40, 50]
                                                        # Invalid: (1, 2), ["abc"], [0] * 20

Type-stub libraries

Used for static analysis, runtime metaprogramming, and developer tooling.
.pyi modules.
Used by type-checkers, not by Python.
Usually MyPy and Pyright automatically pick up .pyi files.

'''Module shapes.pyi'''
from typing import Protocol

class Shape(Protocol):
    def area(self) -> float: ...
    def perimeter(self) -> float: ...

class Circle:
    radius: float
    def area(self) -> float: ...
    def perimeter(self) -> float: ...

PI: float

Location:

project/
    shapes.py
    shapes.pyi <- type stub for shapes.py

If sub-files are located in a separate directory - one of options is:

    Directories:           mypy.ini:              pyrightconfig.json:
~~~~~~~~~~~~~~~~~~~~~      ~~~~~~~~~~~~~~~~~      ~~~~~~~~~~~~~~~~~~~~~~~
project/                   [mypy]                 { "stubPath": "stubs" }
    src/                   mypy_path = stubs
        mypkg/
            ...
    stubs/
        mypkg/
            utils.pyi

Types can be imported and used as usually:

from mypkg.types.geometry import Shape

They can be found, for ex., as: https://pypi.org/project/typing/
Example: https://pypi.org/project/argparse-typing/ (enhanced types for argparse)

More about types

Interesting typing experiments in Python

Runtime types

Wait, but Python is graduate typing language! It means that if you did not include type-check into your CI, then some member of the team can inject buggy code that could be caught on the type-check phase!

To be 100% sure, you can/have use runtime types too.

Comparison of libraries

Typing PEP following:

Library	Strict Runtime Checking	Coercion	Follows Typing PEPs	Notes
Beartype	✔	✘	✔	Fastest strict checker
Typeguard	✔	✘	✔	Most widely used strict checker
Pytypes	✔	✘	✔	Very complete typing support
Enforce	✔	✘	✔	Simple, lightweight checker
Typeenforcer	✔	✘	✔	Declarative runtime type enforcement
attrs	✘ (optional validators)	✔	✔	Declarative classes; flexible typing

Features:

Library	Union	Literal	Annotated	TypedDict
Beartype	✔	✔	✔	✔
Typeguard	✔	✔	✔	✔
Pytypes	✔	✔	✔	✔
Enforce	✔	✘	✘	✘
Typeenforcer	✔	✘	✘	✘
attrs	✔	✔	✔	✔

Generics support:

Library	Supports Generic Types	Parametric Checking	Nested Generics
Beartype	✔	✔	✔
Typeguard	✔	✔	✔
Pytypes	✔	✔	✔
Enforce	✘	✘	✘
Typeenforcer	✘	✘	✘
attrs	✔ (via validators)	✘ (manual)	✘ (manual)

Performance:

Library	Runtime Speed	Import Overhead	Notes
Beartype	✔ Fast	✔ Low	JIT-compiled checks; fastest overall
Typeguard	✘ Medium	✔ Low	Pure Python; slower than Beartype
Pytypes	✘ Slow	✘ High	Very complete but heavy
Enforce	✔ Fast	✔ Low	Lightweight; simple checks
Typeenforcer	✔ Fast	✔ Low	Declarative; efficient
attrs	✔ Fast	✔ Low	Validation optional; minimal overhead

Integration:

Library	Error Messages	IDE Friendliness	Config Complexity	Notes
Beartype	✔ Excellent	✔ Good	✘ Medium	Very descriptive errors
Typeguard	✔ Good	✔ Good	✔ Low	Simple decorator-based usage
Pytypes	✔ Good	✘ Poor	✘ High	Powerful but complex
Enforce	✘ Basic	✔ Good	✔ Low	Minimalistic
Typeenforcer	✔ Good	✔ Good	✔ Low	Declarative and readable
attrs	✔ Good	✔ Excellent	✔ Low	Great DX; optional validation

Examples

Pay attention - all checks happen in run-time and run-time exceptions are not weird and cryptic more: they report type violation before to operate with the object!

Simple example:

import typeguard, traceback, sys

@typeguard.typechecked
def add(x: int, y: int) -> int:
    return x + y
try:
    add(1, 5)
    add('a', 5)         # BUG: unexpected str for x
except Exception as x:
    print(*traceback.format_exception_only(x, file=sys.stdout))

python /tmp/tmp17.py

typeguard.TypeCheckError: argument "x" (str) is not an instance of int

Example with generics:

import typeguard, traceback, sys

@typeguard.typechecked
def add(x:list[tuple[int,bool]], f:bool):
    x.append((len(x), f))
try:
    x = []
    y:list[tuple[bool,str]] = [(False,'hi!')] # TIP: empty mutable containers are not checked!
    add(x, True)
    add(y, True)                              # BUG: y contains unexpected item type
except Exception as x:
    print(*traceback.format_exception_only(x, file=sys.stdout))

python /tmp/tmp18.py

typeguard.TypeCheckError: item 1 of item 0 of argument "x" (list) is not an instance of bool

Example with classes:

import typeguard, traceback, sys

@typeguard.typechecked
class Counter:
    def __init__(self, start:int=0, *, name:None|str=None):
        self.name:str = name or '<unnamed>'
        self.value:int = start
        self._root_name:str = '<unnamed>'

    def increment(self, step:int=1) -> int:
        self.value += step
        return self.value

    @property
    def root_name(self) -> str: return self._root_name

    @root_name.setter
    @typeguard.typechecked
    def root_name(self, n:str): self._root_name = n

cnt = Counter(10)
cnt.increment(2)
try:
    cnt.increment('a')        # BUG: must be int
except Exception as x:
    print(*traceback.format_exception_only(x, file=sys.stdout))    
try:
    cnt.name = True           # WARN: no check here
except Exception as x:
    print(*traceback.format_exception_only(x, file=sys.stdout))    
try:
    cnt.root_name = True      # BUG: thrown, bcs it happens via typechecked setter!
except Exception as x:
    print(*traceback.format_exception_only(x, file=sys.stdout))

python /tmp/tmp19.py

typeguard.TypeCheckError: argument "step" (str) is not an instance of int

typeguard.TypeCheckError: argument "n" (bool) is not an instance of str

Combining compile and runtime types

Just run your type-checkers as before.

AI and types

Personal experience

Type annotations help a lot to AI (the same as to IDE/LSP) - AI "understands" the code better, refactoring done by AI is many times better, it is able to infer types by self, and it is able to check them, find an error, to explain them, also to fix them and to run type-checkers in a shell and to fix type problems.

⚠ I have hit a case when AI wrote wrong code, I asked him to run type-checker and to check errors if there are any - AI found that the just written code contains errors - the type-checking helped AI - and it fixed problems!

Pydantic AI

It is where stronger typing meets AI!

Pydantic AI is a framework for building “AI assistants/agents” where inputs and outputs are strongly typed, validated, and predictable instead of being free-form text chaos.

AI agents (chatbots with tools + memory)
LLM workflows (multi-step reasoning systems)
Structured data extraction from text
Tool-using AI systems (function calling)
Reliable API wrappers around LLMs

             TRADITIONAL LLM CODE:
                                           +----------+
 Extract name     +-----+                  | parse to |
 and age from --> | LLM | --> raw text --> | extract  | --> ('John', 21)
  this text       +-----+                  |  data    |
                                           +----------+

                 PYDANTIC AI:

class Person(BaseModel):
    name: str            ----.
    age: int                  \     +-----+
                               >--> | LLM | --> Person(name='John', age=21)
                              /     +-----+ 
Give me Person           ----'  
from this text

✔ validated
✔ typed (input, output, intermediate steps)
✔ structured (DIE support, static hints)
✔ safe
✔ agents, instead of prompts
✘ not mature yet

Usage:

AI chatbots with memory
Data extraction pipelines
Tool-using agents
Backend AI services
Enterprise AI workflows

from pydantic import BaseModel
from pydantic_ai import Agent

class Weather(BaseModel):
    city: str
    temperature: int

agent = Agent("openai:gpt-4o")

result = agent.run(
    "What's the weather in Paris?",
    result_type=Weather
)

print(result.data)   # OUT: Weather(city='Paris', temperature=22)

CrossHair

Formal verification/symbolic execution tool for Python, it supports IDEs, also Web-broswer playground, can be included in CI, to "watch" source directory, to be integrated to LSP, to find difference between behavior of 2 version, etc:

automatically generates inputs for your functions
uses symbolic execution + SMT solving (not runs as pytest do it)
searches for:
- crashes
- assertion violations
- unexpected edge cases
can sometimes prove properties always hold

Static contracts exist also in Ada SPARK, Dafny, LiquidHaskell, F*, etc.

Simple example - pre-conditions, post-conditions ("static contracts"):

 1: def div1(a: int, b: int) -> int:
 2:     '''
 3:     post: True
 4:     '''                            # TIP: "post: True" - will be checked!
 5:     return a // b                  # BUG: can lead to zero division (non-totality/partial function)!
 6: 
 7: def div2(a: int, b: int) -> int:
 8:     '''
 9:     pre: b != 0
10:     post: True
11:     '''
12:     return a // b                  # OK: precondition requires safe value for b
13: 
14: def div3(a: int, b: int) -> int:
15:     '''
16:     post: True
17:     '''
18:     return div2(a, b)              # BUG: precondition on div2's b can be violated

crosshair check /tmp/tmp20.py 2>&1 || :

/tmp/tmp20.py:5: error: ZeroDivisionError:  when calling div1(0, 0)
/tmp/tmp20.py:18: error: PreconditionFailed: Precondition "b != 0" was not satisfied before calling "div2" when calling div3(0, 0)

Very similar to previous:

 1: def average(xs: list[int]) -> float:
 2:     '''post: True'''
 3:     # BUG: Crosshair finds when ZeroDivisionError will be thrown: xs==[]:
 4:     return sum(xs) / len(xs)
 5: 
 6: def index(xs: list[int], i: int) -> int:
 7:     '''post: True'''
 8:     # BUG: Crosshair finds that xs==[0], i==1 will step over the assert and throw IndexError
 9:     assert 0 <= i <= len(xs)
10:     return xs[i]
11: 
12: def is_power_of_two(n: int) -> bool:
13:     '''post: __return__ if n > 0 else False'''
14:     # BUG: property is wrong for n==0: 0 is not 2**X, Crosshair finds it
15:     return (n & (n - 1)) == 0
16: 
17: def buggy_sort(xs:list[int]) -> list[int]:
18:     '''post: all(a <= b for a,b in zip(__return__, __return__[1:]))
19:     '''
20:     # BUG: no sorting/wrong sorting
21:     return xs
22: 
23: def remove_negatives(xs: list[int]) -> list[int]:
24:     '''post: len(__return__) == sum(x >= 0 for x in __old__.xs)
25:     '''
26:     for x in xs:
27:         if x < 0:
28:             xs.remove(x)
29:     return xs
30: 
31: def append_one(a: list[int], b: list[int]) -> None:
32:     '''post[]: True
33:     '''             # TIP: empty [] - nothing is mutated
34:     a.append(1)     # BUG: a is mutated, counter-example:  [0] -> [0, 1]
35: 
36: def remove_spaces(s: str) -> str:
37:     '''
38:     post: ' ' not in __return__
39:     '''
40:     return s.strip()  # BUG: spaces in the middle are not removed: remove_spaces('\x00 ¡')
41: 
42: State0, State1 = 0, 1
43: class Parser:
44:     '''inv: self.state in (State0, State1)
45:     '''
46:     state:int = State0
47:     def parse(self, s:str):
48:         if s: self.state = State0
49:         elif s == 'a': self.state = State1
50:         else: self.state = 10  # BUG: invariant is violated with parse(Parser(), '') !

crosshair check --analysis_kind=asserts,PEP316,deal /tmp/tmp21.py 2>&1 || :

/tmp/tmp21.py:4: error: ZeroDivisionError:  when calling average([])
/tmp/tmp21.py:10: error: IndexError:  when calling index([0], 1)
/tmp/tmp21.py:13: error: false when calling is_power_of_two(0) (which returns True)
/tmp/tmp21.py:18: error: false when calling buggy_sort([17869, -400]) (which returns [17869, -400])
/tmp/tmp21.py:31: error: Error while evaluating post condition: "<unknown>" yields Argument "a" is not marked as mutable, but changed from [0] to [0, 1]
/tmp/tmp21.py:38: error: false when calling remove_spaces('\x00 ¡') (which returns '\x00 ¡')
/tmp/tmp21.py:47: error: "'''inv: self.state in (State0, State1)" yields false when calling parse(Parser(), '')

Syntax is standard for Python, though:

Conclusions:

Good: Crosshair finds errors faster then property tests - it's symbolic "execution"

(with stubs) using Satisfiability Modulo Theories (SMT) solver (Z3 in the case)

Bad:
- Crosshair is still limited and not mature enough (0.0.107)
- it seems it cannot detect possible aliasing (see append_one())
- it works not so good with impure functions (which is expected, btw!)
but it works well with:
- arithmetic
- indexing
- bounds
- assertions
- dictionary lookups
- integer properties
- string operations

Dafny, Coq, etc extracting of Python code

Dafny - verification-aware programming language with native support for recording specifications and is equipped with a static program verifier.

How can Dafny (or LEAN, coq…) help Python programmers increasing safety? It can produce Python (and Go, and Javascript, and …) code which is verified by static contracts:

                compilation
     +-------+               +---------+
     | Dafny |  __________\  |  Python |  
     |  code |            /  | program |
     +-------+               +---------+

     
               Dafny source
                    ↓
          verification conditions
                    ↓
              Z3 proves them
                    ↓
             verified program
                    ↓
 compiles to Python/Go/Javascript/C#/Java

Similar: Coq, LEAN, etc… but they call "compilation" phase - "extraction".

Stronger "Python" is…

This is very "Pythonish" code:

class Layer(i: Int):
  val sqside = 10 + 4 * i
  val (width, height) = SIZE
  val cols = (1 + i * LAYERDIST) until (width / sqside - 1 - i * LAYERDIST)
  val rows = (1 + i * LAYERDIST) until (height / sqside - 1 - i * LAYERDIST)

  private val _pencolor_hsl = (50 * i, 10 + 10 * (3 - i), 4 + 6 * i)
  private val _brushcolor_hsl = (24 + i * 10, 10 * (3 - i), 25 + 10 * i)

  def pencolor: (Int, Int, Int) =
    val (h, s, l) = _pencolor_hsl
    (h, rnd(s, 10), rnd(l, 30))

  def brushcolor: (Int, Int, Int) =
    val (h, s, l) = _brushcolor_hsl
    (h, rnd(s, 70), rnd(l, 10))

but it is… Scala.

How to try it by self

$ python -m venv .venv

$ pip install -r requirements.txt

$ cat requirements.txt
pyright[nodejs]
pydantic
hypothesis
hypothesis[cli]
crosshair-tool
typeguard
mypy

$ source .venv/bin/activate

# HAPPY TYPING :)