Skip to content

jorenham/hkt-survey

Repository files navigation

Higher-Kinded Types in Python: a survey of real-world use cases

Use cases for higher-kinded typing (HKT) in Python, distilled from real code, one per file, as requested in python/typing#548 (comment). Each file includes the expected type-checker behavior at call sites, since inference of type constructors is the hard part.

Notation

Examples use the notation from python/typing#548 (comment): a PEP 695 type parameter bound to a generic class/protocol is a higher-kinded variable -- a type constructor that is applied by subscription.

A bare class can't be that bound: under PEP 696, T: dict already means T: dict[Any, Any] (a fully applied type), so it can't denote the constructor. We write the bound as Origin[dict] instead -- the unapplied constructor, matching typing.get_origin (get_origin(dict[int, str]) is dict); cf. returns' Kind. Origin[X] "unsubscripts" X to its constructor; the variable is then applied with T[...]. A variable with no family bound (e.g. def f[F](x: F[int]) -> F[str]) is still higher-kinded, recognized by its subscripted use.

Ordinary types have kind $\ast$; a unary type constructor is a type operator of kind $\ast \to \ast$, binary ones $\ast \to \ast \to \ast$, etc. At a call site the checker solves a higher-order unification of the parameter against the argument type,

$$\dfrac {\begin{array}{c} F, G \;:\; \ast \to \ast \qquad X, Y \;:\; \ast \\ F \;\sim\; G \qquad X \;\sim\; Y \end{array}} {F[X] \;\sim\; G[Y]}$$

No new surface syntax is implied; the point is the semantics.

Index

Example Library Refs
bidict_inverse.md bidict typing#548, src
numpy_ndarray_view.md NumPy src
scipy_sparse_astype.md scipy-stubs src
scipy_transformed_distribution.md scipy-stubs src
gevent_group_greenlet.md gevent (typeshed) src
tensorflow_gradient_tape.md tensorflow (typeshed) src
django_admin_register.md django-stubs #9, src
dict_fromkeys.md stdlib (dict/OrderedDict) python/typeshed#6485, python/typeshed#3800
returns_monad_bind.md returns docs

About

Higher-Kinded Types in Python: a survey of real-world use cases

Topics

Resources

License

Stars

Watchers

Forks

Contributors