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

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?

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".

StackExchange Computer Science Q#90415, answer score: 6