3
$\begingroup$

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?

$\endgroup$
  • $\begingroup$ What sort of 'programs' do you allow? This appears to be true for pure functions, but this might be trickier to do for programs involving state or I/O. $\endgroup$ – Discrete lizard Apr 8 '18 at 18:42
  • $\begingroup$ @Discretelizard no particular set of programs in mind. That was just a random thought that crossed my mind :) But we can constrain it to just pure functions $\endgroup$ – Olivetti Apr 8 '18 at 19:37
  • 1
    $\begingroup$ I suspect the answer might depend on the specific set $E$ you have in mind. So can you specify $E$? (without using "etc") Does it have any conditionals, loops, control flow constructs, etc.? Also what types do you allow? Only integers? Also arrays/lists/etc.? $\endgroup$ – D.W. Apr 9 '18 at 16:54
  • $\begingroup$ @D.W. I have purposely left the set $E$ open, but you can imagine that it comprehends any function that is default of a language, in C it can be +,-,*,...if-else, while,...The types can also be the primitives of the language of choice. $\endgroup$ – Olivetti Apr 9 '18 at 20:10
  • $\begingroup$ I don't think the question is answerable without specifying that; I suspect the answer will depend too heavily on the choice of $E$. I'm confused by you calling it a "function". In what sense is if-else or while a function (especially in C)? Or are you assuming a language that has lambdas and higher-order functions? It seems like you're going to need to do a better job of setting up the question before it will have a definite answer. $\endgroup$ – D.W. Apr 9 '18 at 20:15
6
$\begingroup$

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

$\endgroup$
  • $\begingroup$ Thanks for the answer. That clarified many of my misconceptions! I'll move forward on my readings! $\endgroup$ – Olivetti Apr 11 '18 at 10:42
5
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ Thanks for the answer. About the redundancy, I'm aware that any walk would be part of the morphisms, my point is: given the subset of morphisms defined by the default functions of a programming language and the definition of a walk, is this sufficient to build the pure part of any program? I have edited the question to clarify these! (btw, gonna start reading about limits and adjunctions, thx) $\endgroup$ – Olivetti Apr 9 '18 at 11:07

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.