Cammy
| Designed by | Corbin |
|---|---|
| Appeared in | 2021 |
| Type system | static, strong, inferred, implicit |
| Computational class | wikipedia:primitive recursive functional |
| Reference implementation | [1] |
| Influenced by | Hagino CPL, OCaml |
| File extension(s) | .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).
Many folks find that first paragraph confusing or overly generic. Let's assume that we are working with the category of sets and functions. Then, Cammy looks like a point-free programming language; each expression is an S-expression denoting a total function.
The following Cammy expression has type N × N → N and implements addition of natural numbers:
(uncurry (pr (curry snd) (curry (comp app succ))))
This is the desugared primitive form of the following Cammy expression from the reference hive:
(uncurry
(pr
(fun/name id)
(curry (comp 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. [2] 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 → 2 (that is, it denotes a function from natural numbers to Booleans) and tests whether a natural number is even:
(pr t not)
^ λ() :unit. true
^^^ λb :bool. case b of { true -> false; false -> true }
^^ λ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 templates 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)
We could also write this diagram as the primitive arrow:
dup
Crucially, there is no observable difference between `(pair id id)` and `dup`; they are the same arrow.
These are the only two syntactic rules; there are primitive arrows and applications of templates. Note that Cammy expressions are valid wikipedia:S-expressions according to several programming ecosystems, including OCaml and Scheme.
Primitive diagrams
A complete listing of the primitive arrows and templates 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-pi : 1 → F
Predicates
- f-sign : F → 2
- f-lt : F × F → 2
Operators
- f-negate : F → F
- f-recip : F → F
- f-add : F × F → F
- f-mul : F x F → F
- f-floor : F → F + 1
- f-sqrt : F → F + 1
- f-sin : F → F
- f-cos : F → F
- f-atan2 : F × F → F
- f-exp : F → F
- f-log1p : F → F + 1
Jets
A jet is a primitive arrow which is introduced to represent a composite arrow. For example, `app` is introduced to represent `(uncurry id)`. Jets are copied from the runtime into each hive. For any hive, the collection of jets must form a wikipedia:partial order where a jet J is earlier/lesser than another jet K when K's definition requires J. Whenever a runtime sees a jet in user-provided code, it may either compile the jet directly to an efficient low-level operation, or replace the jet with its definition; because jets form a partial order, this process always has well-founded recursion.
The following jets are considered standard, in the sense that the reference implementation will add them into any hive that it saves.
Binary products
- dup = (pair id id) : X → X × X
Cartesian closed categories
- app = (uncurry id) : [X, Y] × X → Y
Natural numbers object
- n-add = (uncurry (pr (curry snd) (curry (comp app succ))) : N × N → N
- n-pred-maybe = (pr right (comp (case succ zero) left)) : N → N + 1
- n-mul = (uncurry (pr (curry (comp ignore zero)) (curry (comp (pair app snd) n-add)))) : N × N → N
- n-double = (pr zero (comp succ succ)) : N → N
Paradigms & classifications
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 [3], 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. [4]
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. [5] 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.