Cammy

Fork

Move 2to3 to subcommand of bk.

This was straightforward and an overall (if slight) reduction in code.
The next commit will clean up the nested lambdas and establish a bit
more structure to be shared between commands.

bk: Extract trees from v3 hives.

I'm a tad worried about the _0, _1, etc. encoding, as it doesn't easily
sort without first parsing once we have more than nine parameters. But
that's a problem for the future, because we haven't had even close to
that number of params.

bk: Switch from CHICKEN to Python 3.

The main motivation is Dulwich; it's so much nicer than libgit2. Click
is also nice too. An important secondary motivation is reducing our
CHICKEN dependencies, because (sadly) we are no longer able to update
our eggs.nix in a seamless fashion. I can't spend my time hacking Nix
expressions that should have been autogenerated.

Clean up envrc.

It's still kind of specific to my setup, but less so.

Add rpypkgs; bump zaha.

Didn't mean to bump zaha, really, but it turned out that I was pointing
at my internal git repository, which isn't going to work for anybody
else. Whoops!

Make a plan.

I wanted to add rpypkgs, but I effectively can't use it yet.

2to3: Fixups.

The output trees are now somewhat respectable. git is still very unhappy
with us, but I don't think I really care.

Get 2to3.py to build a v3 hive.

I haven't verified that the contents of the hive are correct, and
git-fsck is (unsurprisingly) very unhappy with me. I used a monkey patch
on dulwich to allow creation of refs with question marks in their names,
because I know it's legal on Linux and I don't care about other kernels.

Start hacking up a proper migration for old hives.

The script 2to3.py will read in a v2 hive (JSON) and add it to a v3 hive
(git). In theory it could be a really nice and fancy script, but I think
I'm the only person who needs it.

I do need it, though. I have hundreds of expressions in a v2 hive and
I'm not willing to start from scratch.

Maybe solve the (comp dup nil) problem?

Include zaha.

jelly: Parallelize recursion and folds.

This should be cheaper when compiled, although it's not cheaper when
interpreted. It's a matter of cache locality vs number of opcodes.

I'm not yet doing this for tree folds. No real reason.

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.