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.

Types in Cation are declared using a type keyword followed by a type name:

type TypeName

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.

Values are defined using val keyword followed by an optional type annotation and a literal or an expression which evaluation results in the value from the type:

val valName: TypeName := expression

As all small categories can be seen as objects in the category of all small categories $\mathbf{Cat}$, all Cation types as categories may also be seen as objects in a category of all types of Cation language – $\mathbf{Cation}$. As a category, $\mathbf{Cation}$ is small category with infinite number of members.

Expressions, functions, programs

A Cation expression maps a type ($A$) (named argument type) to a type ($R$) (named return type: it can be the same as the argument type, or a different type). Thus, an expression in Cation is always a functor $F: A \rightarrow R$.

Evaluation of an expression selects a value ($a$) from the argument type ($A$) and maps it to another value ($r$) in the return type ($R$). Thus, it is an application of the functor ($F$) of the expression to an object ($a$):

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

Cation uses syntax close to math notation: a function type and expression evaluation are written as

type F: A -> R
val r := F a

You can even use Cation compiler to prove that `r` has the type `R`:

val r := (F a)#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})$

Named functions are defined from expressions

type name: A -> R := expr

or, with a multi-line syntax,

type name: A -> R
   expression(s)

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

In fact, this is a syntactic sugar: data is a macro coming with the standard library, which expends into this code, defining type, constructor function and two projections:

type Prod
type `#Prod`: a A, b B @op -> Prod
  (a, b)
type `.a`: self Prod -> A
  val ($, _) := self
type `.b`: self Prod -> B
  val (_, $) := self

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"

Again, this is a syntactic sugar for

type Either
-- two constructurs:
type `#Either`: a A -> Either := a
type `#Either`: b B -> Either := 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.