JUNK: a programming notation

JUNK is an algebraic programming notation which uses quantales as a primary organising principle, both for data and for code. Quantale modules also play a role, as well as monads; dictionaries are treated in such a way that they behave both very much like other values and very much like other functions.

We start with brief overview of the mathematical preliminaries, and proceed through a tour of the data values, both eager and lazy; the functions, and their application to values; and finish with a sampling of some advanced features made possible by the core theory, followed by some algebraic highlights of the theory.

0. Mathematical Preliminaries

A unital quantale is a monoid in the category Sup of complete join-semilattices. On this page we use ASCII: we spell multiplication as comma `,` with identity `Nil`; spell the join as pipe `|` with bottom `Null`, top `Nuts`; and natural order as `~` (`x ~ y` equivales `x|y == y`). Multiplications distribute over joins, and here they are noncommutative. We will refer to multiplication-prime elements (the alphabet of the monoid) as "items", and refer to join-prime elements as "atoms".

For a quantale Q, a left Q-module is a sup-lattice M together with an action `(Q,M)→M`, satisfying the usual axioms; a right Q-module has action `(M,Q)→M`.

1. Data

There are three sorts of data values:

• simple data - eg ints or strings (with their common orderings, but we won't need that here).
• compound data - other elements of the noncommutative unital quantale over the simple data. In particular, a simple datum is both atom (indivisible under `|`) and item (indivisible under `,`).
• complex data - data containing the packaging wrappers: `[` and `]` around any element denotes a distinct item packaging that element; `{` and `}` around any element of the quantale denotes a distinct atom packaging that element. (neither `[]` nor `{}` are idempotent on data: they may be nested) The quantale join is associative, but `{}` around a `|`-sum forms commutative but non-associative sets; the quantale monoid is associative, but `[]` around a `,`-multiple forms non-commutative and non-associative lists.

User-defined algebraic datatypes also count as complex, and we can view `[]` and `{}` as being similar to other constructors, except with special mixfix syntactic representation.

The join of two items is an item, and `|` distributes across `[]`, so `[0|1]` = `[0]|[1]` which is an item but not an atom. Note that `|` does not distribute across `{}`; `{0|1}` is distinct from `{0}|{1}`.

2. Strictness

There is another simple datum: `NotYet` which is part of an ordering `:~` in which it lies below all other values, all of which are indiscretely related by `:~`. As the name implies, `NotYet` serves as a lazy placeholder for a datum which will be better approximated, later, by a stricter value.

JUNK’s order is lexicographic (:~,~), ie strictness first, joins second, but in implementation it collapses to a flat-lattice.

3. Functions

Similarly to data, there are three types of function:

• simple fns - primitives, lambdas
• compound fns - other elements of the quantale over the simple fns with lattice join `|` having top `FNuts` and bottom `FNull`; and monoid operation `,` having identity `FNil`.

        (f|g)(x) == f(x)|g(x)
        (f,g)(x) == g(f(x))

• complex fns - [f](x) is strict f: application evaluates x until it is proper (recursively does not contain NotYet) and evaluates f(x) until its result it also proper. {f}(x) is lazy f: NotYet propagates. (NB unlike the case for data, [] and {} are idempotent when packaging functions.)

4. Principles of Application

Application is join-preserving: `f(x|y) == f(x)|f(y)`. Furthermore, application of a function to a value outside its domain results in `Nuts`. Application is monotonic in `:~`, the ordering containing `NotYet`. Functions are naturally ordered, `f~g` is equivalent to `(f|g) == g`.

5. Advanced Features

• Two primitive higher-order functions: `Opt(f)(x)` = `f(x)` if x in the domain of f, `x` otherwise; `Rep(f)(x)` = the fixpoint of f applied to x (...f(f(...f(x)...))...) when it exists, otherwise `NotYet`.
• Another syntactic constructor allows us to form `key: value` pairs. Joins of these pairs inside {} form dictionaries, which behave similarly to functions: {1:2,3:4}(1) == 2. Dictionaries can be joined with `|` and composed with `,` like functions. In order to get a compatible ordering with functions, although pairs have the usual lattice ordering within the curly brackets, from outside the curly brackets the keys sort in the opposite fashion: dictionaries are compared by (-size, revlex of key, lex of vals). This also means composition of dictionaries is monotonic.
• Local definitions use the `$$` operator. Instead of `let y=f(x) in let z=g(y,x) in h(z,x)`, JUNK writes `h(z,x) $$ z:=g(y,x) // y:=f(x)`; this local definition mechanism will be extended to provide modules in the program-organizing sense.
• Lambdas, instead of being expressed as `(\formals. expression)`, are expressed via `expression @ pattern` and application does a pattern match on the actuals to bind the formals. If the pattern does not match, the entire operation evaluates to `Nuts`. Dual to `$$` there is a substitution mechanism for patterns `$?` which goes in the opposite direction: `(decl1 // decl0 $? pat)` equals `decl1 $? (decl0 $? pat)`.
• Local definitions containing declarations of the form `z<-g(y,x)` act as quantale-monoid-comprehensions, producing an item of output for each item of `g(y,x)` (unless `z` is a pattern which fails to match, in which case it filters) and they can be freely mixed with scalar declarations.

Note that because `$$` and `$?` are useful for analysing complex expressions and patterns into simpler subexpressions and subpatterns, they induce a straightforward translation into ANF.

6. Algebraic Highlights

• Data forms a module over functions with application as scalar multiplication.
• The quantale homs (albeit not functions in general) form a module over data with application as scalar multiplication.
• Because `h(z,x) $$ z:=g(y,x) // y:=f(x)` is equivalent to `(h(z,x) $$ z:=g(y,x)) $$ y:=f(x)` and is bilinear in the join, expressions form a module over declarations with substitution as the scalar multiplication.
• Because `(decl1 // decl0 $? pat)` is equivalent to `decl1 $? (decl0 $? pat)` and is bilinear in the join, patterns form a module of the opposite-handedness to expressions. `$$` and `$?` do not commute; `@` is the tensor mediating them.
• Declarations acting on both pattern and expression modules respect the evaluation strategies of complex functions.
• `[]` is adjoint to `{}` and hence `[f]~g == f~{g}`, as well as giving rise to a lazy monad `T(f) = {[f|}` (isomorphic to Haskell's Maybe) and a strict comonad `S(f) = [{f}]`

Influences

Shout outs to Backus, Burstall, Conway, Dijkstra, Hehner, Iverson, Kleene, McCarthy, Scott, and Wadler.