• R/O
  • HTTP
  • SSH


No Tags

Frequently used words (click to add to your profile)

javac++androidlinuxc#windowsobjective-ccocoa誰得qtpythonphprubygameguibathyscaphec計画中(planning stage)翻訳omegatframeworktwitterdomtestvb.netdirectxゲームエンジンbtronarduinopreviewer

A categorical programming language

Rev. 时间 作者
1edc88b master 2023-10-21 13:52:25 Corbin

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.

a7d1038 2023-09-29 07:58:20 Corbin

Enumerate jets for an expr?

I don't like this.

b79c5eb 2023-09-26 10:46:18 Corbin

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.

ec13b16 2023-09-19 12:57:12 Corbin

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.

59169e1 2023-09-19 04:03:15 Corbin

Build a new thing with libgit2 and CHICKEN.

54ea75c 2023-09-12 10:22:43 Corbin

Add a note.

34b5bd0 2023-06-05 03:05:20 Corbin

cammyo: Fix a typo.

c6a0447 2023-04-25 14:39:59 Corbin

Clean up Nix expressions.

6cdc008 2023-04-25 14:00:58 Corbin

Factor the JSON schemata to their own prefix.

Straightforward deduplication, I think.

f47e44b 2023-04-25 13:48:29 Corbin

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.

6a8366e 2023-04-03 15:18:56 Corbin

Print basic descriptions of arrows.

61ff218 2023-03-31 11:44:33 Corbin

Shuffle todo list.

b53ed5e 2023-03-30 12:02:58 Corbin

Basic template-saving abilities for the REPL.

9d52176 2023-03-28 05:46:40 Corbin

Add a few more rules for Booleans.

b11b782 2023-03-28 04:44:14 Corbin

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).

99a2f8a 2023-03-25 15:18:05 Corbin

Use SNOC bytecode in peephole optimizations.

c712d3d 2023-03-25 14:30:25 Corbin

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.

c341f0e 2023-03-24 19:23:20 Corbin

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

be70233 2023-03-24 19:03:47 Corbin

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.

3b77fb5 2023-03-24 16:24:46 Corbin

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.

11c65e3 2023-03-24 14:13:43 Corbin

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.

684744a 2023-03-19 11:50:58 Corbin

Start a tool for updating hives.

9e2cc69 2023-03-15 17:36:07 Corbin

Start working on a coherent theory of jets.

ea8fa4c 2023-03-13 14:59:34 Corbin

Allow basic entry/display of templates.

7f34a29 2023-03-09 22:26:21 Corbin

Jellify before presentation.

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

baafff0 2023-03-03 04:02:50 Corbin

Enable the JIT during animations. 60 FPS!

1e59f44 2023-03-03 02:44:33 Corbin

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

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

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.

31e3ce3 2023-03-02 14:30:15 Corbin

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.

f5ba4ac 2023-03-01 14:47:15 Corbin

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.

e69bb0c 2023-03-01 12:31:15 Corbin

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.