Cammy

Fork

Try prototyping type inference for algebras.

I'm really *really* thinking about how to avoid having to write out the
types of the carriers, but I'm not quite seeing how to do it. I'm also
trying to avoid writing out the names of elements of signatures, but I
might have to give up.

Enumerate jets for an expr?

I don't like this.

Successfully insert and fetch a nested AST.

What is left before making a blog post? Probably trails and names, at
least. Modules can wait. Laws can wait. Jets are important, but can be
added later.

Flesh out a basic tree-insertion tool.

This is sufficient to implement a basic set of expressions, but it's
neither enumerable nor tagged, and doesn't have trails.

Build a new thing with libgit2 and CHICKEN.

Add a note.

cammyo: Fix a typo.

Clean up Nix expressions.

Factor the JSON schemata to their own prefix.

Straightforward deduplication, I think.

Become a Nix flake.

I had to use nixos-22.11 because it seems like egg2nix is broken on
nixos-unstable. I'll probably have to care about that in the future.

Print basic descriptions of arrows.

Shuffle todo list.

Basic template-saving abilities for the REPL.

Add a few more rules for Booleans.

Tell jelly about symmetry instead of commutativity.

This is perhaps a subtle change, so I should explain it at least once.

Suppose we have a symmetric binary operator o : X × X → Y. It is
equivalent to (comp swap o), by definition. So, we used to take the
classical Church-Rosser-ish approach, rewriting (comp swap o) => o.
However, there's a phase issue. This rule consumes swaps, but it doesn't
generate them, so it is dependent upon the rest of the rules to squeeze
swaps to the right of compositions, making them available:

(comp (comp (comp f swap) swap) o) =>
(comp (comp f swap) (comp swap o)) =>
(comp (comp f swap) o)

This is only one possible ordering; another is:

(comp (comp (comp f swap) swap) o) =>
(comp (comp f (comp swap swap)) o) =>
(comp (comp f id) o) =>
(comp f o)

This non-determinism is even worse when we consider that dup is
symmetric in its outputs; a rule like (comp dup swap) => dup is
reasonable on its own, but can only consume swaps which are squeezed to
the left. By abstract nonsense, dup is the only arrow with this
property, but it is intrinsic to CCCs and thus we must handle it
gracefully and correctly.

So, let's put all of this on its head since we use e-graphs. Let's say
that o => (comp swap o) and dup => (comp dup swap). This means that the
e-graphs containing o and dup will always reify them with just a bit of
non-determinism. This is desirable because a symmetric arrow is
semantically the same before and after the swap, so the e-graph is
really just representing the symmetry faithfully. Let's also consider
arbitrary f and say that o is opaque and neither primitive nor jet, to
preserve generality. Now, the e-graph for our example expression adds
the following representatives to its e-class (rules in brackets,
unlabeled lines are bookkeeping):

$0 ← f
$1 ← o
$2 ← (comp $0 swap)
$3 ← (comp $2 swap)
$4 ← (comp $3 $1) [assumption]
$5 ← (comp swap $1)
$4 ← (comp $2 $5) [comp is associative]
$1 ← (comp swap $1) [new symmetry rule]
$5 = $1 [e-graph union-finding]
$4 ← (comp $2 $1) [$5 = $1]
$4 ← (comp $0 $1) [comp is associative]

And now e-class $4 can be extracted as (comp f o); when swap has
non-zero cost, then this will be the preferred representative. The
e-class $5 is introduced for bookkeeping when we reassociate e-class $4,
but is immediately identified with e-class $1, skipping the need to
introduce and eliminate a (comp swap swap) term! In a certain way, our
rule suggests that symmetric operations generate swap's involution
simply by being invariant under swap:

$0 ← swap
$1 ← o
$2 ← (comp $0 $0) [assumption]
$3 ← (comp $2 $1)
$1 ← (comp $0 $1) [new symmetry rule]
$3 ← (comp $0 $1) [comp is associative]
$3 = $1 [e-graph union-finding]
$4 ← id
$3 ← (comp $4 $1) [explosive! id is unit for comp]
$4 = $2? [e-graph union-finding? swap is involutive]

Similar logic applies to dup when dualized; it can be generalized to
apply to any (pair f g), since (pair f g) = (comp (pair g f) swap).

The point of all of this is to work towards partial evaluation of
arbitrary binary operators. When such operators are symmetric, then we
can both use the symmetry to cut the number of needed rules in half (as
I've done with disj and conj in this commit!) and to expose PE
opportunities on any dup or (pair f g).

Use SNOC bytecode in peephole optimizations.

Use general recursion to implement folds.

This required extending the queue of curried arrows to a more general
pending-arrow queue which can emit several types of subroutines. Along
the way, I fixed some disassembler bugs, factored some text handling,
and tightened up the data model a bit.

Add trees to jelly.

That second unfold rule is daunting! Hopefully that means that it will
not be preferred often. Still, sometimes it will be necessary just for
beta-reduction.

Implement trees in REPL and typechecker.

They seem to work! I might have either fold or tfold backwards in the
interpreter, but that's life.

Update jelly and prepare for future jets.

This was going to be a bigger change, but apparently I can't write Rust
late at night, so I'm calling it here.

Use a side stack for folding lists in CAM.

This Forth-inspired hack seems like a reasonable alternative to
recursion, and hopefully is more legible to the GC than stack frames.

Everything worked on the first try, modulo RPython translation errors.
This is not normal, and I poked around a bit to double-check the
correctness of output.

Start a tool for updating hives.

Start working on a coherent theory of jets.

Allow basic entry/display of templates.

Jellify before presentation.

This isn't quite full-heap jellification, but that might always be a
pipe dream. Not sure.

Enable the JIT during animations. 60 FPS!

Add single-channel greyscale rendering.

Easy enough. The stb writer supports 1-4 channels, with the
interpretation hardcoded for the number of channels:
1. K
2. KA
3. RGB
4. RGBA

libcaca is more flexible. Each pixel takes up some number of bits. If
it's 8 bpp or less, then a palette is used; by default, it appears to be
either greyscale or 232 RGB. Above 8 bpp, explicit channel masks are
required.

My API includes a number of channels as well as explicit masks. We could
compute libcaca masks in advance, if we wanted to make libcaca do
exactly the same mapping as stb.

Isolate the ability to examine output types when sampling.

Since both samplers are hardcoded to RGB outputs, this doesn't do
anything new. But in a commit or two, we'll support RGBA or grayscale
or something along those lines.

Pipe animate/draw calls through jelly.

One animate call seems to stall, but there are many possible causes and
it's hard to know where to start. It's also not important at the moment.

Show partially-dissolved expressions with dips.

This is something I've wanted for a while, and it required so much code
before... now, it seems almost free. Except for the code duplication, of
course! I think I can start hacking again now.