# The Categorical Language

Explaining Cation language in terms of Category Theory

Cation is a categorical language, meaning a strong equivalence between Category theory and language constructions. This article dives into the details of such equivalences, which are made into a core of the language design.

## Basics

In Cation language everything – data types, functions, expressions, values, literals – corresponds to categories,
functors and objects. Since categories can be seen as objects in a higher-order category, all of them need just
two main language constructions: **types** and **values**, introduced and explained in this section.

### Types and Values

The very fundamental concept of a Cation language is *type*. Each type is a *category* in itself.
Contravariantly, a *category* in Cation language is named *type*.

This is a full and sufficient definition of what *type* is; everything else about types in Cation and Cation
itself are just consequences of this definition. For instance, saying that Cation is a language of operations
with types defines Cation as a categorical language.

Important to note that all Cation types are small categories and can be represented as finite sets, inhabited by their
*values*. Hence, a value in Cation is an object in one of the *type* categories.

As all small categories can be seen as objects in the category of all small categories *types* as categories may also be seen as objects in a category of all types of Cation language –

### Expressions, functions, programs

A Cation expression maps a type

Evaluation of an expression selects a *value* *argument type* *value* *return type* *functor* *expression* to an object

$$\mathsf{eval}\ F\ a \doteqdot a \xrightarrow{F} r$$

The signature of an expression $F: A \rightarrow R$ is a type by itself: this is a function type. It can also be defined via the evaluation, as shown above, applied to all objects of the argument category:

$$F\ a = r \in R\ |\ \forall a \in A$$

In Cation, each function is a named expression – and each expression is a function (which maybe anonymous). All expressions and functions are

- functors,
- morphisms in
$\mathbf{Cation}$, - objects in $\mathrm{hom}(\mathbf{Cation})$

A Cation program is a composition of expressions, which is an expression itself (as a composition of functors is always a functor). Execution of program corresponds to an evaluation of the expression: an application of the composed functor to a program argument giving a result.

### Data types

Data types is another example of Cation *types*, such that data types are the first-class language citizen
alongside functions and expressions.

There are only two foundational data types, named *unit* and *uninhabited*. Unit type is an *initial object*
in the $\mathbf{Cation}$ category and is written as `(,)`

. Uninhabited type is a *terminal object* in the
$\mathbf{Cation}$ category and is written as `(|)`

. All other data types are derived from these two types via ... yes,
expressions!

Data type is defined as an expression composition of other types. As with any algebraic data type system there are two
forms of composition: *product* and *co-product*.

*Product data types* are bi-functors from categories representing types $L$ and $R$ to a new category $P$; where
$P$ is a cartesian product of sets of $L$ and $R$ objects: $P \doteqdot L \times R$. This also defines two
projections as functors from the type $P$ to the original types $L$ and $R$. Cation expresses product with a
comma operator (`,`

) and the new type may be defined in the following way:

```
data Prod: A, B
-- using the new Prod type
val new := (valueA, valueB)#Prod
val projA := new.a
val projB := new.b
-- testing that the result is the same as the original values:
projA =? valueA && projB =? valueB !! mustBeEqual
```

*Co-product data types* are bi-functors corresponding to the morphism in the $\mathbf{Cation^\mathrm{op}}$: they
map a union of sets representing all possible values in $L$ and $R$ to a new category $S$: $S \doteqdot L + R$. Cation
union with a pipe operator (`|`

) and the new type may be defined in the following way:

```
data Either: A | B
-- using the new Either type
let either := a#A -- `a` is the value from the type `A`
either >|
(a)#A |? print "I am A"
(b)#B |? print "I am B"
```

## Advanced topics

### Currying

Since each data type constructor is a functor, and each functor takes exactly one argument, the multi-argument function
type `type fn: A, B -> C`

can be seen as a functor of a single argument of an unnamed product type `(A, B)`

– or as a
composition of two unnamed functors `type fn: A -> (B -> C)`

– similar to the Haskell language.

### Lambda expressions

### Collections

### Generics

Now it is time to introduce Cation language constructs build using the last component of the Category theory:
*natural transformations*.

### Monads

## Expert topics

Here we show how all language constructs can be interpreted as natural transformations, such that their composability properties are used for terminal analysis and parallel computations without creation of racing conditions.