The Type Category

Although deep knowledge of category theory is not required to use fp library, understanding its basic vocabulary and concepts should be very valuable. We also hope that this Python library will encourage unfamiliar users to learn how functional languages represent polymorphic types and programs, stateful or asynchronous computations, I/O and error-handling… without the hustles of moving to a foreign language and losing the rich Python ecosystem.

Introduction

This manual will sequentially introduce all the relevant concepts that are embodied by some (meta)class in the fp library. Let us also mention that the Wikipedia is also a very valuable resource on both the mathematical and programming aspects of category theory.

Let us start with our very first mathematical definition,

Category:

A category C is defined by

  • a class of objects denoted \({\rm Obj}({\bf C})\) (e.g. the class of sets, vector spaces, types…)

  • a set of arrows or morphisms \({\rm Hom}_{\bf C}(A, B)\) (e.g. functions, linear maps, typed programs…) whose elements are denoted by \(f : A \to B\), for every objects \(A, B\),

  • a composed morphism \(g \circ f : A \to C\) for every pair of composable morphisms \(f : A \to B\) and \(g : B \to C\)

  • an identity morphism \(1_A : A \to A\) for every object \(A\), which fixes any composable morphism by left and right compositions respectively.

The composition is furthermore demanded to satisfy \(h \circ (g \circ f) = (h \circ g) \circ f\) for every triplet of composable morphisms, composition is said to be associative.

Categories and functors were introduced in the 1950s by mathematicians Eilenberg and Steenrod to classify topological spaces by their homology groups. Somehow surprisingly, category theory has also found profound applications in computer science and logic since (see for instance the Curry-Howard correspondence).

Example

Types

The Type category is described by:

  • the class of objects \({\rm Obj}({\tt Type})\) described by isinstance(..., Type),

  • type of programs (functions) Hom(A, B) for any pair of input/output types A and B,

  • a composed program g @ f for every composable pair f : Hom(A, B) and g : Hom(B, C),

  • an identity function Hom.id(A) : Hom(A, A) for every type A.

Note that within the library, fp.Hom is an alias to fp.Type.Hom.

Type Objects

All types within fp are instances of the metaclass fp.meta.type.Type, which for instance takes care of pretty-printing type annotations of typed values.

>>> from fp import *
>>> isinstance(Int, Type)
True
>>> Int(8)
Int : 8

The Int class is a subclass of the python builtin int. Its behaviour is only decorated by the metaclass type(Int) == Ring, a subclass of Type.

>>> n = Int("fp", base=32)
Int : 505
>>> isinstance(n, int)
True
>>> [isinstance(T, Type), for T in (Int, int)]
[True, False]

Instances of Type are referred to as type objects, as Type forms a cartesian closed category.

Type Morphisms

A type morphism f: A -> B refers to a pure, typed function with input in A and output in B.

Because morphisms is a shorthand for homomorphism in mathematical terminology, the type of pure functions from A to B is generically denoted by Hom(A, B). This type accepts any plain python callable, which means it may be used as a function decorator:

>>> @Hom(Int, Str)
... def bar(n):
...     return n * "|"
>>> bar
Int -> Str : bar

The axioms of a category demand that morphisms are equipped with the following structure:

  • For every type A, there is an identity morphism: Hom.id(A) of type A -> A.

  • For any morphisms f: A -> B and g : B -> C, there is a composed morphism g @ f : A -> C.

It is also required that (i) left/right composition with the identity is the identity and (ii) composition is associative, i.e. h @ (g @ f) == h @ (g @ f) for every composable triple f, g, h.

Note: The fact that Hom(A, B) is itself an instance of Type is an additional axiom of cartesian categories. The categories of sets and vector spaces are also cartesian (i.e. they have sets of functions and vector spaces of linear maps as objects). In many other interesting examples, the set of morphisms Hom(A, B) is only required to be a set, but not an object of the category (e.g. in a partial order such as Keys, the set of arrows A -> B is a point when A is contained in B and empty otherwise).

>>> foo = Hom(Str, Int)(len)
>>> foo
Str -> Int : len
>>> foo @ bar
Int -> Int : len . bar
>>> bar @ foo
Str -> Str : bar . len
>>> isinstance(type(bar), Type) and type(bar) is Hom(Int, Str)
True

Typed functions of Hom(A, B) store their computation sequence in a tuple: an empty tuple is an identity, and concatenated tuples describe compositions. This yields a truely associative representation of function pipes, avoids the stack growth of nested function closures, and enables composing an arbitrary number of functions at the small cost of tuple instance creation.

>>> baz = Hom(Str, Int)(lambda s: s.count("*"))
...
# Typed compositions compare their internal tuple
>>> foo @ (bar @ baz) == (foo @ bar) @ baz
True
>>> foo @ bar @ baz == Hom.compose(baz, bar, foo)
True
>>> foo @ bar @ baz
Str -> Int : len . bar . λ
...
# Input redirection `<<` will execute last
>>> foo @ bar @ baz << "M*ule * G*uffres!"
(Int: 3)

Type checks and type casts only happen at the entrance and exit of the pipe. Future versions of the library might include switches to customize this behaviour, e.g. warn on implicit type casts as the python isinstance builtin might incur a little overhead.

Type Sums and Products

A fascinating aspect of category theory is its ability to succinctly describe almost all mathematical concepts with simple arrow diagrams. In particular, sums ans products are characterized by their so-called universal properties. This means that defining sums or products is not at all arbitrary, but enforced by the categorical structure (objects, arrows and identities), whenever sums and/or products exist. The Type category (just like sets and vector spaces) has both sums and products, obtained by the Either and Prod type constructors.

In fp, the universal property of sums is called gather:

Either.gather: ((A -> Y), (B -> Y),  ...) -> Either(A, B, ...) -> Y

and the dual universal property of products is called branch:

Prod.branch: ((X -> A), (X -> B), ...) -> X -> Prod(A, B, ...)