Can we define a program by means of a walk of a graph induced by the category of types?

Question

After reading about Category Theory at https://bartoszmilewski.com/2014/10/28/category-theory-for-programmers-the-preface/ I was wondering whether we can represent any program by means of a walk of a graph induced by the category of types.

EDIT: rephrasing the question a little bit.

So, given the category of types where the objects belong to a set of types $V$ and the morphisms are a set of functions $F$ with $f : a \rightarrow b$, if we define a walk on this category as a sequence $v_0, e_{0,1}, v_1, ..., v_n$, with $v_i \in V$ and $e_{i,j} \in E \subset F$, with $E$ as the default set of functions of any given programming language (add, mul, <, etc.), the pure part of a program could be defined as a walk on this set $E$.

So, for example, a program to return the greatest of two integers could be represented as:

v0 -> e1 -> v1 -> e2 -> v2
(Int, Int) -> e1 -> (Bool, Int, Int) -> e2 -> Int

with:

e1 : (Int, Int) -> (Bool, Int, Int)
e1 x y = (x>y, x, y)

e2 : (Bool, Int, Int) -> (Int, Int)
e2 b x y = if b then x else y

given that e1 and e2 are part of the subset of morphisms.

So, is the definition of a walk and this set $E$ sufficient to represent the pure part of any program?

Answer 1

Consider the simply-typed $\lambda$ calculus: this is one of the simplest functional languages you can define.

It is very common to interpret it in a Cartesian closed category (CCC). Indeed, CCCs are the "ideal" categorical setting where to interpret simple types.

CCCs, being categories, admit morphisms composition and identity. Taking your definition of "walk" loosely, as a rough idea rather than a rigorous concept, I think you covered this aspect of CCCs.

However, they also allow products, which are not considered by "walking". Given $f:A\to B$ and $g:A\to C$ there is a unique morphism $\langle f,g \rangle: A\to B\times C$ satisfying a certain universal property. This is a way to craft new morphisms from old ones that "walking" does not consider.

There's even more. The main, fundamental property of CCCs is the "currying" adjunction. That is, there's a natural bijection between the set of morphisms $A\times B\to C$ and $A\to C^B$ (where $C^B$ corresponds to the functional type $B\to C$). So, given a morphism in one of this set, we can take the corresponding one in the other set. Doing this is important to interpret $\lambda x. \ldots$, and without that, we do not have a "lambda" calculus.

So, even in the simplest setting, interpreting a functional program is much more than "composing morphisms", or the proposed definition of "walking".

Answer 2

Your question sounds redundant to me. By definition of category whenever two morphisms with common object $f\colon A \rightarrow B$ and $g\colon B \rightarrow C$ exist, then their composition $g\circ f \colon A \rightarrow C$ must exists as another arrow in that same category. (otherwise, that situation is just not a category.)

So the redundant part in your question is: there is no need to convert a category of types to its underlying graph then find all the possible walks then decide what morphism (function) that walk correspond to. The morphism obtained this way was already in the category to begin with.

---

On the other hand, if I were to interpret your question less literally. Maybe you were wondering if composing morphism is the only way to build new programs from existing ones. This couldn't be more wrong. You'll see many more ways to construct new morphisms from existing ones. Some examples that you'll see soon after learning category theory are functors, limits, and adjunctions. Once you know how they translate in category of types, you'll see that they provide many essential construction in programming that isn't covered by just composition of function.