Still writing the docs. Content addressing is the mechanism, that is: same content lands in the same slot, equality is a handle compare. The allocator is provably extensional so distinct content never aliases even though the hash itself can collide. The Leech part: the heap is sized to the lattice's 196,560 minimal vectors, the coordinate-to-slot map is a collision-free perfect hash built from the Conway group's mm_op tables, and that fixed universe is what makes sets into 196,560-bit bitmaps with O(1) membership and bitwise ops.
I understand that you can hash any object into a 196,560-slot space (that's how regular hash tables work), but I'm not sure why you'd want to do that. Regular hash tables can be resized when they get full (or less-full), yours cannot. How is this any different from a hash table with a fixed capacity of 196,560 entries?
"provably extensional" is not an established term in this context and communicates nothing about the design. I simply do not believe that this design doesn't have trivial collision issues, or that it makes efficient use of memory.
Are you saying that two distinct pieces of content can never collide? That seems obviously incorrect.
For example, take the integers 0 - 196,561, and put them into your lattice-based map. Something’s got to give. There are only 196,560 containers in the map (right?)
The only relation to the Leech group appears to be the number of slots.
When a table gets full they allocate a second one, and so on, up until 256 tables when allocations start silently failing (after exactly 50319104 allocations).
I hope OP is seriously considering what’s actually been built here, and how their interactions with whatever LLM they’ve been using really reflects that. I’m genuinely a bit concerned for them.
There's no wrong in vibe coding as long as you check what's the output. I can be wrong or missing the goal of course. But the work is in progress and I'm not writing a bash script for the theorem of pytagora. It's more complex and I'm studying as I go. You reviewed frontend/ast.ml, the small kernel, and concluded MLTT, but you missed frontend/cubical.ml. Thanks for the time you took to bring this critique, it will be helpful in the end.
Oooft, in cubical.ml why is your identity equivalence `CVar "__id"`? Surely this should be some fibration/reduction?
In fact, these weird string terms pop up pretty often, but surely you’d want to be using de Brujin indices lest you accidentally string match two different things (can’t believe I’m saying that for an implementation of a dependently typed language).
I started to wonder how your types were glued, as I would have thought Sigma types glued along identity equivalences would give me some insight on the odd behaviour.
`reduce_comp` seemed like the place it should be. There I realised your `CTGlue` case is wrong: it seems like `partial_pairs` is in the head but dropped from the body, so they’re never glued by any equivalence.
Hi everyone, and thanks for taking the time to read about Yon.
I had an idea and I threw it down, and I'm refining it day by day. It's hard because I have little time, but I'm trying. Most of the concepts seem to be working, and that makes me proud of the intuition, even if it's eccentric enough to look psychotic. Better docs, cleaner and more coherent code, new benchmarks and use cases will come. But it's version 1.0: what did you expect? I'm alone in this exploration.
A few answers for you trough the comments...
