# Cammy

Designed by Corbin 2021 static, strong, inferred, implicit wikipedia:primitive recursive functional  Hagino CPL, OCaml `.cammy`

Cammy is a basic syntax for expressions of wikipedia:categorical logic. Cammy expressions can be interpreted in any category with the appropriate features. The current documented syntax addresses any wikipedia:Cartesian closed category which has wikipedia:categorical sums, a natural numbers object, and free monoids (lists).

The following Cammy expression has type N × N → N and implements addition of natural numbers:

```(uncurry (pr (curry snd) (curry (comp (uncurry id) succ))))
```

This is the desugared primitive form of the following Cammy expression from the reference hive:

```(uncurry
(pr
(fun/name id)
(curry (comp fun/app succ))))
```

Cammy is named for and partially inspired by the CAM, as implemented in OCaml. Cammy is additionally inspired by Hagino CPL, as described in Hagino 1986 and implemented in Sakai.

## Semantics

The internal language of a Cartesian closed category is always a lambda calculus.  We can therefore explore an example in terms of lambda expressions. Note that categorical arrows are not necessarily functions! The following Cammy expression has type N → Ω and tests whether a natural number is even:

```(pr t not)
^      λ() :unit. true
^^^  λb :bool. not b
^^        λx :(1 → X). λf (X → X). λn :N. case n of { O -> x (); S m -> f (pr x f m) }
^^^^^^^^  λn :N. case n of { O -> true; S m -> not (pr t not m) }
```

Several complicated ideas are tied together here. First, note that destructuring in categorical combinators is implicit. We had to introduce the idea of case/match syntax in order to implement primitive recursion, but primitive recursion is taken to be an axiomatic feature of natural numbers objects. When we work categorically, that entire case/match construction is encapsulated within the axioms. This also occurs with lists (free monoids); there is only one type of recursion, the katamorphic fold.

Next, note that fixpoint recursion is also implicit. There are no arbitrary fixpoint combinators in Cammy, just the predefined combinators for natural numbers and lists. The OCaml and Scheme implementations of Cammy must use their own recursion techniques to implement these combinators.

## Syntax

Each Cammy expression is a diagram which selects arrows in the target category. When the diagram is parameterized over a choice of source object, then we assign it a single polymorphic arrow instead of a family of arrows. To demystify this utterance and introduce some syntax, here is the simplest such diagram, the identity arrow:

```id
```

This expression has type X → X, where X is any source object whatsoever. For contrast, here's a diagram which doesn't have any choice of source objects:

```zero
```

This expression has type 1 → N, where 1 is the terminal object and N is the natural numbers object. Traditionally, there would not be a single identity arrow, but a family of arrows with one member for each different possible object; but Cammy treats both expressions similarly, and allows them to be freely intermixed.

We also have functors which take static parameters. For example, we may take any two arrows with types X → Y and X → Z, and produce a new arrow with type X → Y × Z, where once again X, Y, and Z range over objects. This diagram therefore has type X → X × X for any object X:

```(pair id id)
```

These are the only two syntactic rules; there are nullary functors and non-nullary functors. Note that Cammy expressions are valid wikipedia:S-expressions according to several programming ecosystems, including OCaml and Scheme.

### Primitive functors

A complete listing of the primitive functors follows, grouped by functionality. X, Y, and W are metavariables for types as before, but 1 is the terminal object, 2 is the Boolean object, and N is the natural numbers object. Equalities denote algebraic laws.

An appendix at Cammy/Bikeshed explains the nomenclature.

#### Categories

• id : X → X
• Given f : X → Y and g : Y → W, (comp f g) : X → W

#### Binary products

• ignore : X → 1
• fst : X × Y → X
• snd : X × Y → Y
• Given f : X → Y and g : X → W, (pair f g) : X → Y × W

#### Binary sums

• left : X → X + Y
• right : Y → X + Y
• Given f : X → W and g : Y → W, (case f g): X + Y → W

#### Cartesian closed categories

• Given f : X × Y → W, (curry f) : X → [Y, W]
• Given f : X → [Y, W], (uncurry f) : X × Y → W

#### Boolean algebra

• t : 1 → 2
• f : 1 → 2
• not : 2 → 2
• conj : 2 × 2 → 2
• disj : 2 × 2 → 2
• either : 2 → 1 + 1

#### Natural numbers object

• zero : 1 → N
• succ : N → N
• Given x : 1 → X and f : X → X, (pr x f) : N → X

#### Free monoids

• nil : 1 → [X]
• cons : X × [X] → [X]
• Given x : 1 → Y and f : X × Y → Y, (fold x f) : [X] → Y

#### Floating-point numbers object

The floating-point numbers object behaves like wikipedia:IEEE 754, except that NaNs are not elements, since they are not numbers. The NaN cases of f-add and f-mul return 0.0 or -0.0 as appropriate. The NaN case of f-sqrt is sent to the right-hand side of the binary sum. The reciprocal of ±0.0 is ±Infinity and vice versa.

##### Constants
• f-zero : 1 → F
• f-one : 1 → F
• f-sign : F → 2
##### Operators
• f-negate : F → F
• f-recip : F → F
• f-lt : F × F → 2
• f-add : F × F → F
• f-mul : F x F → F
• f-sqrt : F → F + 1

### User-defined functors

Cammy can load functors from hives, which are directory trees where files are Cammy expressions. By default, functors are nullary, but special names can be used to address functor parameters. For example, the nullary functor "swap" is usually defined as:

```   (pair snd fst)
```

And the reference hive includes this as "fun/swap.cammy". As an example of parameterized functors, the unary functor "fun/name" is defined as:

```   (curry (comp snd @0))
```

The special name "@0" refers to the zeroth parameter. Arity is implicit and inferred during the frame step of the reference toolchain, so that (name id) will be allowed but (name id id) will be rejected.

In terms of the principal programming paradigms, Cammy is a "functional programming" language; it possesses the ability to encode arbitrary functions via topos theory. Later improvements may shift Cammy to the "monotonic dataflow programming", "multi-agent dataflow programming", or "event-loop programming" paradigms.

In terms of the common taxonomy of type systems, exhibited for tutorial at , Cammy's current toolchain implements a static, implicit, structural, sound type system. For a classic example, the program (comp dup apply), sometimes called the "Turing bird", will be rejected by the toolchain as ill-typed.

In terms of the taxonomy of desugaring systems, Cammy does not implement desugaring. Any nullary sugar can be implemented as plain Cammy programs. Every algebraic equality in Cammy's combinators corresponds to a desugaring rule in the toolchain, but those equalities are not taxonomically syntactic sugar.

## Computational complexity class

Cammy has wikipedia:primitive recursive functionals, placing it between PR and R. This complexity class has no standard name. 

## Implementation

The reference implementation consists of several components composed into several high-level pipelines.

### cammy-frame & cammy-jelly

The `cammy-frame` tool takes a hive and an expression relative to that hive, and returns an expression containing only primitive operations. No optimizations are performed.

The `cammy-jelly` tool reads an expression and simplifies it by applying algebraic optimizations. Jellification is ignorant of hives, but non-primitive operations are allowed; they will be opaque to optimizations.

#### Example usage

A demonstration hive is included with the reference distribution.  This hive includes basic arithmetic on natural numbers and some folds on lists.

```\$ cammy-frame hive/ <hive/list/gauss.cammy | cammy-jelly
(comp
(comp (pr (pair zero nil) (pair (comp fst succ) cons)) snd)
(fold zero (uncurry (pr (curry snd) (curry (comp (uncurry id) succ))))))
```

### cammy-djinn

The `cammy-djinn` tool takes a type and returns a primitive expression with that type. It operates via relational logic, inverting the relation between expressions and types.

#### Example usage

`cammy-djinn` takes three parameters. The first two parameters are an input and output type. The third parameter is a difficulty/creativity parameter which starts at 1 and has no upper limit. Higher difficulty/creativity will make the tool take longer and search for more complex expressions.

Types have a simple S-expression syntax. The concrete types 1, 2, N, and F appear as themselves. Polymorphic variables can be given any fresh identifier, like X, Y, Z, W, etc. The compound types are expressed as functors:

• `(pair X Y)` is the product type of X and Y
• `(sum X Y)` is the sum type of X and Y
• `(hom X Y)` is the type of functions from X to Y
• `(list X)` is the type of lists of X
```\$ cammy-djinn 'X' '(sum X Y)' 1
left
```
```\$ cammy-djinn '(pair (hom X Y) X)' 'Y' 1
(uncurry id)
```

### cammy-repl

The `cammy-repl` tool takes a hive and examines it interactively. Cammy expressions entered at the REPL are expanded, jellified, and typechecked. The `:!` command evaluates and pretty-prints any element.

#### Example usage

```\$ cammy-repl hive/
> nat/fact
Type: N -> N
> :! (comp nat/5 nat/fact)
120
```

### cammy-draw

The `cammy-draw` tool interprets a simplified Cammy expression as a function from the two-dimensional plane to red-green-blue color triples. While interpreted, it is much faster than compiled native code because it is built upon the RPython JIT toolkit.

#### Example usage

```\$ cammy-frame hive/ <hive/demo/burning-ship.cammy | cammy-jelly >ship.cammy
\$ time cammy-draw ship.cammy '-1.8 -0.08 -1.7 0.02' 1920 1080 ship.png
real	1m52.253s
user	1m51.983s
sys	0m0.233s
```

## Related work

This concept is perennial. Curien 1986 gives an isomorphic syntax for the fragment of topoi and a recipe for compiling syntax to the CAM. Elliott 2017 gives an isomorphic syntax for the fragment of Cartesian closed categories and a recipe for compiling a fragment of Haskell to syntax. See the appendix at Cammy/Bikeshed for a complete bibliography.