# Cation Language Overview

Cation as a pure categorical programming language for practical tasks.

We designed Cation to be:

- non-verbose;
- as close to mathematics notation as possible;
- extensible and usable for creation of domain-specific languages.

## Unique features

### Boundness

Cation is the first and the only language where *all types are bounded in their size and computational resources at the
compile time*. This enables two main core language properties: *formal verifiability* and *termination analysis*. It
also makes Cation a language which can be used for writing ubiquitous deterministic programs suitable for mathematical
modelling and immutable smart contracts.

By types being *bound* we mean that any type is a finite set of a known size, with all possible values known to the
compiler.

- Only two foundational types: unit (initial object) and uninhabitable type (empty set or a terminal object);
- All integers are enumerations made with unit type (Peano arithmetics);
- All rational numbers, including rational numbers (like results of division of integers),
arithmetic reals (like square root of 2) and irrational numbers (like
*pi*or*e*) are explicit decimal approximates expressed as functions running for a number of steps known at compile-time; - All other types are composed as a product or co-product categories from unit and uninhabitable type;
- Dynamic collections and iterators always have bounds on the minimum and maximal number of elements enforced at compile-time;
- There is no bottom type (non-terminating computations).

### Parallelism by default

Cation compiller converts a program as a set of expressions into a composition of natural transformations. This allows static analysis at compile-time of which branches of computations depends on which values from other branches; the compiler uses this information to parallize all computing wherever is possible with no programmer or syntax overhead.

When needed, a developer can use an explicit parallelism using asynchronous channels, avoiding racing conditions. These channels can be used to send values, lambda-functions and even other channels between execution threads using rho-calculus: an extension of lambda-calculus for parallel computations.

### No RAM, no mutability

- Absence of mutable variables;
- Abstracted memory management: language is suitable for architectures with no RAM access, like memristors and cellular automation;

## Notable features

- Generic system
- Collections
- Iterators
- Collection comprehensions
- Extensible set of literals
- Domain-specific languages
- No runtime
- Tiny set of compiler built-ins
- Moands
- Side-effect control
- Termination analysis
- Extensible infix operators
- Close-to-mathematics

## Syntax

### Declarations

Cation has only two keywords: `type`

, for defining a type, and `val`

, for instantiating a value.