taliesinb

What are your half dozen active projects? And did AI use make you more ambitious about what those projects could be?

Interesting. It all seems very brittle, though. And that something has gone very wrong with our ecosystem of tools, languages, and processes when it becomes advisable to massage source until specific passes in a specific version LLVM don't mess things up for other passes.

Not picking on the OA in the slightest; just thinking in terms of holistic system design. If you know what you want to happen, and you are smart enough to introspect the behavior of the tool and decide that it didnt happen, you are more than smart enough to just write it correctly in the first place.

Perhaps that is unrealistic, perhaps there is a hidden iceberg of necessary but convolutive optimizations no human could realistically or legibly write. But ok, where do you really need to engage in this kind of optimization golf? Inlined functions?

Ok, what about this targeted language feature for a future-day Zig:

1. Write an ordinary zig function 2. Write inline assembly version of that function 3. Write a "comptime assert" that first compiles to second, which only "runs" for the relevant arch. 4. What should that assert mean? That the compiler just uses your assembly version instead, but _also_ uses existing compiler machinery or an external theorem prover to verify they "behave the same up to X", for customizable values of X

That has the right feel, maybe. You are "pinning" specific, vetted, optimizations without compromising the intent, readability, or correctness of your code. And easy iteration is possible, because a failing comptime assert will just dump the assembly; you can even start with an empty manual impl.

Amusingly, you need only have circuits of prime depth, though you should probably adjust their widths using something principled, perhaps Euler's totient function.

And i bet these would be useful in initial and final parts of transformer too. Because syntactic parsing and unparsing of brackets, programming language ASTs, etc is highly recursive; no doubt current models are painfully learning "unrolled" versions of the relevant recursive circuits, unrolled to some fixed depth that must compete for layers with other circuits, since your total budget is 60 or whatever. Incredibly duplicative and by definition unable to generalize to arbitrary depth!

There is an obvious implication: since the initial models were trained without loops, it is exceedingly unlikely that a single stack of consecutive N layers represents only a single, repeatable circuit that can be safely looped. It is much more likely that the loopable circuits are superposed across multiple layers and have different effective depths.

That you can profitably loop some say 3-layer stack is likely a happy accident, where the performance loss from looping 3/4 of mystery circuit X that partially overlaps that stack is more than outweighed by the performance gain from looping 3/3 of mystery circuit Y that exactly aligns with that stack.

So, if you are willing to train from scratch, just build the looping in during training and let each circuit find its place, in disentangled stacks of various depths. Middle of transformer is:

(X₁)ᴹ ⊕ (Y₁∘Y₂)ᴺ ⊕ (Z₁∘Z₂∘Z₃)ᴾ ⊕ …

Notation: Xᵢ is a layer (of very small width) in a circuit of depth 1..i..D, ⊕ is parallel composition (which sums the width up to rest of transformer), ∘ is serial composition (stacking), and ᴹ is looping. The values of ᴹ shouldnt matter as long as they are > 1, the point is to crank them up after training.

Ablating these individual circuits will tell you whether you needed them at all, but also roughly what they were for in the first place, which would be very interesting.

If you could link to where this is implemented I'd be very grateful!

Hello! Yes I am curious, how does one deal with cycles in the code hash graph? Mutually recursive functions for example?

Given that whole name binding thing is ultimately a story of how to describe a graph using a tree, I was primed to look for monoidal category-ish things, and sure enough the S and K combinators look very much like copy and delete operators; counit and comultiplication for a comonoid. That’s very vibe-based, anyone know of a formal version of this observation?

Yes, this is a very cool story.

But, fascinatingly, integration does in fact have a meaning. First, recall from the OP that d/dX List(X) = List(X) * List(X). You punched a hole in a list and you got two lists: the list to the left of the hole and the list to the right of the hole.

Ok, so now define CrazyList(X) to be the anti-derivative of one list: d/dX CrazyList(X) = List(X). Then notice that punching a hole in a cyclic list does not cause it to fall apart into two lists, since the list to the left and to the right are the same list. CrazyList = CyclicList! Aka a ring buffer.

There's a paper on this, apologies I can't find it right now. Maybe Alternkirch or a student of his.

The true extent of this goes far beyond anything I imagined, this is really only the tip of a vast iceberg.

The end-game is just dissolving any distinction between compile-time and run-time. Other examples of dichotomies that could be partially dissolved by similar kinds of universal acid:

* dynamic typing vs static typing, a continuum that JIT-ing and compiling attack from either end -- in some sense dynamically typed programs are ALSO statically typed -- with all function types are being dependent function types and all value types being sum types. After all, a term of a dependent sum, a dependent pair, is just a boxed value.

* monomorphisation vs polymorphism-via-vtables/interfaces/protocols, which trade roughly speaking instruction cache density for data cache density

* RC vs GC vs heap allocation via compiler-assisted proof of memory ownership relationships of how this is supposed to happen

* privileging the stack and instruction pointer rather than making this kind of transient program state a first-class data structure like any other, to enable implementing your own co-routines and whatever else. an analogous situation: Zig deciding that memory allocation should NOT be so privileged as to be an "invisible facility" one assumes is global.

* privileging pointers themselves as a global type constructor rather than as typeclasses. we could have pointer-using functions that transparently monomorphize in more efficient ways when you happen to know how many items you need and how they can be accessed, owned, allocated, and de-allocated. global heap pointers waste so much space.

Instead, one would have code for which it makes more or less sense to spend time optimizing in ways that privilege memory usage, execution efficiency, instruction density, clarity of denotational semantics, etc, etc, etc.

Currently, we have these weird siloed ways of doing certain kinds of privileging in certain languages with rather arbitrary boundaries for how far you can go. I hope one day we have languages that just dissolve all of this decision making and engineering into universal facilities in which the language can be anything you need it to be -- it's just a neutral substrate for expressing computation and how you want to produce machine artifacts that can be run in various ways.

Presumably a future language like this, if it ever exists, would descend from one of today's proof assistants.

An earnest question: can you elaborate on what Zig got wrong in that respect?

In another life!