Programming Languages as Categories

Or, if we consider several different sorting algorithms implementations, do we want to consider them equal as functions?For a machine it is definitely easier to check whether the abstract syntax trees used to define two functions are equal, but it could turn out very hard to understand whether two functions are extensionally equal, because it would have to compute the functions for every possible value.

Therefore in programming the default form of equality between functions, called intensional, concerns the equality of internal definitions.

Coming back to our functor definition, we can now spot where the problem is.

Our definition of equality between functions uses intensional equality, while the VerifiedFunctor interface is using extensional equality.

Since intensional equality is more fine-grained that the extensional one, we can not hope to adapt the VerifiedFunctor interface to our definition.

We will need to slightly change our definitions to use extensional equality.

What we need to do is change our definition of morphisms, so that we can assert that extensional equality holdsrecord ExtensionalTypeMorphism (a : Type) (b : Type) where constructor MkExtensionalTypeMorphism func : a -> bpostulatefunExt : {f, g : ExtensionalTypeMorphism a b} -> ((x : a) -> func f x = func g x) -> f = gWe wrap functions in a new type ExtensionalTypeMorphism and we postulate that two elements of this type are equal whenever we have a proof of the extensional equality of the inner functions.

This corresponds to quotienting the TypeMorphism type with respect to the equivalence relation given by extensional equality.

Moreover, we can use this new type for defining morphisms of a new category which we will call typesAsCategoryExtensional.

Functors are functors (part 2)We can now come back to prove that VerifiedFunctors can be seen as CFunctors.

Let’s resume from where we left off, adjusting things with our newly introduced ExtensionalTypeMorphism and typesAsCategoryExtensional.

functorToCFunctor : VerifiedFunctor f -> CFunctor typesAsCategoryExtensional typesAsCategoryExtensionalfunctorToCFunctor {f} func = MkCFunctor f (functorOnMorphisms func) ?funcPreserveId ?funcPreserveCompWe can now use our postulate funExt to complete the missing piecesfunctorPreserveId : (func : VerifiedFunctor f) -> (a : Type) -> functorOnMorphisms func a a (extIdentity a) = extIdentity (f a)functorPreserveId _ a = funExt (x => functorIdentity {a} id (v => Refl) x)Here we use the functorIdentity field of the VerifiedFunctor interface, which gives us the extensional equality between id : f a -> f a and (map id) : f a -> f a.

Using funExt we can transform the extensional equality into a concrete equality and complete the proof.

Similarly, we can prove that an Idris functor respects function composition according to our definition.

functorPreserveCompose : (func : VerifiedFunctor f) -> (a, b, c : Type) -> (g : ExtensionalTypeMorphism a b) -> (h : ExtensionalTypeMorphism b c) -> functorOnMorphisms func a c (extCompose a b c g h) = extCompose (f a) (f b) (f c) (functorOnMorphisms func a b g) (functorOnMorphisms func b c h)functorPreserveCompose func _ _ _ (MkExtensionalTypeMorphism g’) (MkExtensionalTypeMorphism h’) = funExt (x => functorComposition x g’ h’)ConclusionToday we saw how types and functions of a programming language, Idris in our case, can be interpreted as a category.

Moreover, we proved that the concept of functor commonly used in functional programming correspond exactly to functors from a categorical point of view.

This implies that we can use concepts from category theory, reason with them in their very abstract setting, and then apply what we found out to our software.

Or, from another point of view, we can try to write our software thinking just in terms of categories, so that we know that our code can be used not only to talk about programming languages, but has a broader scope and application.

I promised a little surprise at the beginning, so here it is: we released open source our category theory library!.You can have a look at the parts of the code which I didn’t have the time and space to investigate in this series of blog posts.

It would be really awesome if you could provide us with some feedback on it and, if you will, maybe contribute with a new category or some other concept we haven’t defined yet.

.

. More details

Leave a Reply