How Type Variance fits into Category Theory

Category theory

(f◦g)◦h = f◦(g◦h)

Definition (group)

A couple (G, °), where G is a set, and ° : G x G -> G a binary operator, is said to be a “Group” if all these conditions hold:

— there exists an element e in G such that for every g in G, e ° g = g = g ° e (e is called the neutral of the group)

— for every a, b and c in G, we have (a ° b) ° c = a ° (b ° c) (associativity of °)

— for every element g in G, there exists an element h in G such that g ° h = e = h ° g (the inverse)

Definition (morphism of groups)

A function f : G -> H between two groups G and H is said to be a morphism if the two following conditions hold:

— if a is the neutral element of G, and b the neutral element of H, then f(a) = b

— for all x, y in G, we have f(x ° y) = f(x) ° f(y)

Definition (category)

A category C is composed of

— A class O(C) of objects

— A class A(C) of arrows f: A -> B where A and B are objects

such that the two conditions hold:

— if there is an arrow f: A -> B and an arrow g: B -> C, then there exists an arrow g.f: A -> C

— for each object A, there exists an identity arrow id: A -> A such that, for all arrows f: A -> B, we have f.id = f and for all arrows g: C -> A, we have id.g = g.

Furthermore, arrow composition is associative, i.e., f.(g.h) = (f.g).h.

Definition (functor)

A functor F from a category C to a category D is such that

— each object O in C is mapped to an object F(O) in D

— each arrow f in C is mapped to an arrow F(f) in D, in such a way that either of these conditions hold:

— — if f: A -> B, then F(f): F(A) -> F(B) and for all arrows f: A -> B and g: B -> C, we have F(g.f) = F(g).F(f) (in this case, we say that the functor is “covariant” — it preserves the direction of the arrows)

— — if f: A -> B, then F(f): F(B) -> F(A) and for all arrows f: A -> B and g: B -> C, we have F(g.f) = F(f).F(g) (in this case, we say that the functor is “contravariant” — it reverses the direction of the arrows)

Moreover, in each of these cases, for all A, the identity of A is mapped to the identity of F(A)

Type Variance

How type variance fits into category theory

Function[Function[T, Boolean], T]

Conclusion

--

--

Get the Medium app

A button that says 'Download on the App Store', and if clicked it will lead you to the iOS App store
A button that says 'Get it on, Google Play', and if clicked it will lead you to the Google Play store