Cammy

From Esolang
Jump to navigation Jump to search
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).

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

(uncurry (pr (curry snd) (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 → Ω 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.

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
  • pick : 2 × (X × X) → X

NNO

  • 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

  • f-zero : 1 → F
  • f-one : 1 → F
  • f-negate : 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 "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.

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 in a simple pipeline.

Frame

The frame is a preprocessor written in OCaml which statically links together multiple Cammy expressions. The frame takes any nullary functor which is not standard, and treats it as a file path into a tree of Cammy expressions. Each path is replaced with the expression at that path.

Suitable trees are called hives. A demonstration hive is included with the reference distribution. [5] This hive includes basic arithmetic on natural numbers and some folds on lists.

Jelly

The jelly optimizer is a Cammy-to-Cammy optimizer which uses e-graphs to search for the smallest equivalent expression. The rule engine from Willsey et al 2021 is used for its ergonomic yet speedy design. The rules are written in a DSL embedded in Rust, along with comments explaining their provenance and correctness. [6]

Movelist

The movelist is a relational typechecker written in CHICKEN Scheme's dialect of miniKanren. It can typecheck a Cammy expression, or take a type representation and synthesize Cammy expressions with the given type.

Compiler

The compiler is a bash wrapper which assembles a Scheme program. The program mostly consists of a handwritten stub. The wrapper combines the stub with both the Cammy expression and its represented type and then invokes `csc` on the complete program. This lets us abuse CHICKEN Scheme's toolchain to compile a Cammy expression to native code.

Example

The reference implementation includes the program `list/gauss`, which is a function N → N computing the sum of the natural numbers up to a given bound. We can ask the toolchain to compile this program and run it:

$ ./compile.sh hive/list/gauss.cammy
$ ./gauss 101
5050

When the compiler is invoked, it first reads in the program from "hive/list/gauss.cammy":

(comp list/range nat/sum)

It then recursively looks up the files "hive/list/range.cammy":

(comp (pr (pair zero nil) (pair (comp fst succ) cons)) snd)

And "hive/nat/sum.cammy":

(fold zero (uncurry nat/add))

Which finally looks up "hive/nat/add.cammy", which has the same expression in the example at the top of this page. After linking, jelly finds no possible improvements, which is common for small handwritten expressions.

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.