# Towards GPU Type Inference: Data-Parallel Hindley-Milner (DPHM Part 1) _Date: 2026-09-23_ ___ Good type systems are awesome. Long compile times are not. Can we do better? How about _exponentially_ better? ## A Late Hello This post has been ~1000 days overdue. Oops! It was my Recurse Center project ~3 years ago, teased in my post on [GPU Bitonic Sorting](Faster%20sorting%20with%20SIMD%20CUDA%20intrinsics.md). I've been working on this post itself for a while now, and have learned many things beyond my initial explorations, mainly due to AI helping me find relevant literature and experimenting with some optimizations. (Near the bottom of this post, I'll have an [[#AI Aside]] for those who might want to know how I used AI for this.) Let's just get to it now! ### What Okay, maybe "Towards GPU Type Inference" was a bit too much hype. And we can't really do "exponentially" better. But I _do_ want to scam type inference from `O(N)` runtime down to "`O(log^2(N))`" (mind the scare-quotes). We're going to explore (propose) an algorithm for parallel type inference for the simply typed lambda calculus (STLC). In fact, a _data-parallel_ type inference algorithm, so that we might sneakily, handwavedly call it a sensible idea for GPU acceleration. "GPU inference" has never been such an overloaded term until now -- let's confuse everyone for fun and profit(?)! I'll call this overall idea `DPHM` (Data-Parallel Hindley-Milner) because it's a nice, short acronym. More specifically: we're going to go after something shaped like Algorithm W, and we'll keep the entire thing **monomorphic**. Let-polymorphism only somewhat affects the performance arguments, but it also needs a bit more time to cook[^1]. This post will be aimed at undergrad CS level with a bit of assumed type systems/PL theory. For those who may need an intro/refresher on STLC/type inference... well, besides the large amounts of guides already out there, you'll have to wait for my next post. Out-of-order execution is modern, get with the times! ## Why? So... I hate waiting. But I like having strong type systems (e.g. in Scala) prove things about my code that I'd otherwise have to test -- which takes significantly more code, and still doesn't _guarantee_ properties. As someone who is lazy and hates production incidents, the more I can prove about my code, the better. Except that some of the compute we save on tests becomes compute we spend waiting for the compiler. Scala compilation speed was also generally a constant complaint, being the top-requested language "feature" survey after survey. At Twitter, I worked on parallel compilation performance and massively parallel builds (e.g. Twitter's experimental Scala outliner, Rsc). CI could take over two hours, half of which was just building. There were long serial stretches where everything waited on a few core dependencies. With local compilation, my Intel MacBook's fans would spin ceaselessly with all CPU cores pegged, while its AMD GPU was just sitting there like a lazy bum. On paper, it had something like 10x the compute and efficiency, but it was doing nothing. How dare it! How (massively) parallel compilation works is usually: assume you know all public types, then parallelize (i.e. C/C++ headers). With Rsc, we used declared signatures to produce outlines (effectively the equivalent of headers), which unlocked parallelism in the subsequent Scala compilation. But I also want type inference. I don't want to annotate everything, and sufficiently interesting types may be painful/impossible to write out anyway. Now with AI coding and formal proofs in the picture, propositions-as-types has never been so relevant. A faster typechecker, please. And from that, maybe a faster prover? There's a whole parallel computer sitting right there, whether GPU or (SIMD) CPU. ## Isn't Type Inference Serial? Typically, yes. Algorithm W and its state-mutating cousin, Algorithm J, are basically depth-first-search (DFS). Which, since it uses a stack, is inherently serial, right?[^2] But, even [DFS is parallelizable](https://www.andrew.cmu.edu/user/mrainey/papers/pdfs_sc15.pdf). And even if DFS were serial, who's to say we can't turn it into a BFS? Regardless, I was already convinced for many years that type inference can be parallelized[^3]. But can full STLC inference be done, and can it be made data-parallel? And can we make it "provably better" (for some useful definition of "better") than a sequential typechecker? Yesn't. If I were a bit more arrogant, this is where I'd say "[On the **Allegedly** Sequential Nature of Unification](https://dspace.mit.edu/entities/publication/9614acb5-d1d4-4371-b772-012bfe9d92b9)"... but, not quite. STLC type inference (via first-order unification) is [PTIME-complete](https://cstheory.stackexchange.com/questions/47639/complexity-of-type-inference-in-the-simply-typed-lambda-calculus). And if I legitimately gave you `O(polylog(N))` time, I would have proven `P` = [`NC`](https://en.wikipedia.org/wiki/NC_%28complexity%29). That's... probably not happening, unfortunately. But we can do something "good enough" given real-world program shapes. We'll show that, "in practice", the sequential requirement (parallel depth/span) is manageable, somehow allowing us to scale with the number of processors, `P`, which we'll take to be approximately `N` (size of AST). The claim is we can get our runtime bound for the core solver to something like `O(D*log(N))`, where `D` is the maximum depth of any inferred type. While `D` is technically `O(N)`, in practice, it's roughly constant. Or, I can give theorists an aneurysm by saying `D ~ O(log(N))`. What gave the idea a concrete shape was reading [EigenCFA](https://matt.might.net/papers/prabhu2011eigencfa.pdf), a GPGPU version of 0CFA, a minimal [control-flow analysis problem](https://matt.might.net/articles/implementation-of-kcfa-and-0cfa/): local constraints, a work queue (frontier), propagation until saturation. Why couldn't we use that skeleton here?[^4] Every AST node contributes local typing constraints. We can collect them into an initial frontier of constraints and start propagating from every node at the same time. Unification lets us uncover more consequences which then update the frontier, looping until we're out of "neighboring equations". Philosophically, this is like turning sequential DFS sideways into a parallel BFS. The interesting question is how much sequential depth might remain, and what it depends on. ## The Idea The high-level machinery for parallel type inference looks fairly ordinary: - A frontier of constraints is an array of pairs/equations of types, i.e. `A=B`. - Hashmaps (if needed) for function interning[^5], i.e `{F: A->B}`. [GPU hashmaps](https://developer.nvidia.com/blog/maximizing-performance-with-massively-parallel-hash-maps-on-gpus/) are a thing. - Parallel connected components (CC), or [parallel union-find](https://jshun.csail.mit.edu/6506-f25/lectures/lecture15-2.pdf) Effectively, every piece is known to work. We just have to put them together. Here's a sketch of the algorithm -- pseudocode, like every code block in this post: ```python def infer(ast): frontier, union_find = initialize(ast) while frontier: union_find.bulk_merge(frontier) # parallel CC: O(log(N)) check_components(frontier) # O(1) + O(log(N)) for deduping return union_find ``` Assuming you buy the fact that we can `bulk_merge` quickly and correctly, and deal with the occurs check[^6], the major point collapses to "wtf is `check_components`"? ### Type inference is solving constraints Type inference for STLC writes down one constraint per AST node, then solves it after solving for its children. Take an application `f a`. We don't know the type of `f` or `a` yet. But `f` had better be a function that accepts whatever `a` is and returns whatever `f a` is. Name those three types `F`, `A`, `R`: ```python f : F a : A f a : R # Once we see `f a`, just make up "R" because we can # the constraint from seeing `f a` F = A->R # or Eq(F,A->R) ``` We can write that down without solving anything. So write it down for the *whole program* first: `N` nodes, `N` constraints, produced by an embarrassingly parallel map. That's our initial frontier. A classical typechecker instead walks the tree and solves each constraint as it meets it. ![[dphm-fig-dfs-vs-parallel.svg]] ### Two ways to get more equalities Given a bunch of constraints, there are only two ways to get more equalities[^7]: 1. **Transitivity** via `bulk_merge`: `A = B` and `B = C` give `A = C`. 2. **Down** via `check_components`: `(A -> B) = (X -> Y)` gives `A = X` and `B = Y`. There are also two ways to fail: a clash (`Int = Bool`, or `Int = A -> B`), or an infinite (cyclic) type (`X = X -> R`, from `\x. x x`[^8]). We'll assume finite types for the sake of clarity. Each way to progress is parallel-friendly on its own. Transitivity over all known constraints is just parallel CC/union-find. In type inference, every connected component (disjoint set) represents one distinct type. During `bulk_merge`, we publish a batch of `O(N)` equations as merge (union) "requests" in parallel, and parallel connected components is a solved problem -- asymptotically, at least. Down is a local `map`: look at a pair of function types we know are equal, _decompose them_, then emit two child constraints. The key is that this actually exposes more information. Just because we merged two function types, `A->B` and `X->Y`, doesn't mean we know whether `A=X` and `B=Y` -- but they *must* be, or our program doesn't typecheck. Naively, this means we'll need to decompose all pairs of known-equal functions. The trick: to get all the information we'll need, we only need to consider `O(N)` rather than `O(N^2)` pairs. ### The serial part What's *not* parallel is that the two feed each other to uncover more levels of consequences. Down produces constraints. And while we can sometimes know enough to produce more than one "level" of constraints at once, I don't believe that matters, not even asymptotically. We still need to publish and globally sync. Publishing the results of Down is what merges components. That allows us to compare new pairs of functions for new constraints in the next Down round, and we loop. A sketch of what this algorithm does per loop is that each processor (thread/worker) looks at a type and "deepens" it a single layer, e.g. something like: ```python round 0: A1 round 1: B1->B2 # A1 was secretly this all along round 2: (Bool->C1)->(C2->Int) # B1 was (Bool->C1), B2 was (C2->Int) round 3: (Bool->(D1->Int))->(Int->Int) # ... ... ``` ![[dphm-fig-rounds-tree.svg]] This per-level deepening is also not a new invention. Well, I thought it was new at the time, but recently, with the help of AI (and paying $41.50), I found a fairly old (and rather uncited) paper[^9] which supposedly gives a similar treatment. ### Why the number of rounds is the depth of the types Each round of the loop goes Down exactly one layer on every type, everywhere in the program, in parallel. If you write out any inferred type as a tree (binary tree in our case), then the depth of a function type is the height of its tree. Call the maximum depth of any such inferred type `D`. ```python A # depth = 1 Int # depth = 1 A -> B # depth = 1 + max(depth(A), depth(B)) # depth = 4 (Bool->(Int->Bool))->Int ``` If each round costs `O(log(N))` (connected components, sorting, etc), the whole thing is `O(D * log(N))`. **Claim**: for typical programs, `D` is small and roughly constant. We don't write deeply nested types in reality[^10]. This is what makes DPHM even remotely interesting. In the worst case, `D` is `O(N)` and we're at `O(N log N)` span, which is worse than just running sequentially (`O(N)`-ish). But that kind of input is almost certainly an adversarial program. That's the idea. The rest of this post will attempt to be a bit more precise. ## The Algorithm We're going to _describe_ the algorithm here, preferring to be illustrative rather than necessarily present code or going into too many ideas about "performance". The hope is, by the end of this, you'll either go "huh, that might work", or possibly even better, explain exactly to me why it shouldn't work. Still, part of "that might work" comes from "can we efficiently represent this on real hardware", so some "implementation detail"-like ideas will leak in (like representing IDs with `Int`s). Sequential (illustrative) Python code [here](https://gist.github.com/wiwa/c8e60f36e2a63045dd4a0427ff1767fe). Actual CUDA code, and (maybe) Lean proofs will be added later[^11]. Now, the stated problem: Given a closed STLC term (AST with no free variables) of size `N`, find its [principal type](https://en.wikipedia.org/wiki/Principal_type) -- or we fail if we have a type that recurses infinitely, e.g. `F: A->B` but `A: F->G` or a clash (type error) like `Int = Bool`. **We assume $P = \Theta(N)$ parallel processors on a [CREW](https://en.wikipedia.org/wiki/Parallel_RAM) machine**. (And now, I will revert to using `O(n)` instead of $\Theta(n)$ for the engineers out there.) ### The Setup For the most part, we don't want to fuss around with inputs/outputs, and instead focus on the solver. But it's a good idea to show that we're not hiding any serious work. The AST is given to us in an array of nodes via preorder traversal. The index of a node (`Expr`) is its `NodeId`. Therefore the root term is at index `0`. ```python NodeId = Int TypeId = Int ``` We will assume, wolog, that no two binders (parameters) share the same name (i.e. AST preprocessed via alpha-renaming), so we don't have to think about annoying shadowing nonsense. #### 1. Process the syntactic metadata First, we need to know where each variable comes from, i.e. map each variable occurrence to its binder (its function parameter declaration). Then, every AST node gets a type ID. This can simply be "make a new type variable per node, node ID == type ID", and let the later constraints do the legwork. That being said, we do need more than just an ID per type, we need actual type info. This means that we have three arrays of size `O(N)`: ```python nodes: Array[Expr] # NodeId -> Expr # For each variable occurrence, just remember its binder's TypeId. binders: Array[TypeId] # NodeId -> TypeId (or 0) types: Array[TInfo] # TypeId -> TInfo (including extra function records) @dataclass class TInfo: tid: TypeId arg: TypeId ret: TypeId Type = TVar | TAtom | TFn TVar # an unknown type / metavariable TAtom(name) # a fixed base type, such as Int or Bool TFn(arg, ret) # a function whose children are type IDs; arg -> ret ``` Variables (binders and occurrences) initially map to `TVar`. Literals map to `TAtom`. Allocate functions as needed for lambdas/applications[^12]. `O(N)` records, all allocated up front. Each type can be fully represented as a single `TInfo` (`TAtom` `tid` can be an index into a string array for later pretty-printing). While this preprocessing step can be parallelized, I'd rather just assume it as input for the solver. Importantly, every `TInfo` stores "1 level" of type data -- not the entire tree of `TFn`. Hardware-related note: if we use `u32` for types, we can represent every `TFn` as `u64: (arg, ret)`[^13]. #### 2. Initial Constraints Map each AST node to one constraint (equation) as the initial frontier, straight from the STLC typing rules: | Source node | Constraint | |---|---| | Variable `x` | `type(x) = binder_type(x)` | | Constant `c` | `type(c) = TAtom(base_type(c))` | | Lambda `\x. body` | `type(lambda) = TFn(binder_type(x), type(body))` | | Application `f a` | `type(f) = TFn(type(a), type(f a))` | Each equation is a constraint represented by a 64-bit struct (a pair of integer type IDs). The initial state is an array of type records (`TInfo`), an array of constraints, and an array-based union-find (`UF`) with every type initially its own root (i.e. in its own component). ```python types: Array[TInfo] initial_constraints: Array[Eq] # pending equations, not reflected in UF yet uf: UF = UF(parents: Array[TypeId]) # TypeId -> TypeId ``` ### 3. The Loop Here's a slightly more detailed sketch: ```python def infer(types, initial_constraints, uf, root): constraints: Array[Eq] = initial_constraints while constraints: uf = bulk_merge(uf, constraints) # publish constraints = check_components(uf) # Down, one level constraints = normalize(uf, constraints) # dedupe occurs_check(uf) return read_back(uf, types[root]) ``` Three operations, so let's start with the most boring one first. #### normalize Drop constraints which have the same roots (which implies they're already equal), order each pair so `A = B` and `B = A` look the same, then sort and dedupe the list into a _set_. An empty result means we're done. #### bulk_merge `bulk_merge` publishes a batch of constraints to the global UF. Any parallel CC algorithm will do, but we also ask for two extra properties in the result: 1. **Flatness**: Every element points directly at its root, so `uf.root(t)` is `O(1)` afterwards (i.e. it's a star shape). 2. **Rigid roots**: If a component contains a _rigid_ type (`TAtom` or `TFn`), its root should be a rigid type as well, not a `TVar`. Two different atoms in one component, or an atom and a function, is a clash (we should error out). Two different `TFn`s in one component is fine, that's exactly what drives `check_components`[^14] and subsequent constraints. Both rules can be run as cleanup steps after merging, or we can bake them into the merge itself. The rigid-root rule is what makes a clash visible even when it was produced by two different workers who never saw each other's constraints: `A = Int` and `A = Bool` are individually fine, but after (or during) merging, we can easily find the issue. Well, okay, we could just use a metadata array, but that's extra memory usage _and_ a pointer hop. #### check_components To me, the surprising _star_ of the show is `check_components`. It looks like it doesn't do enough work. `check_components` says: for each component, pair all its elements (types) against its root, then decompose into equations of their children. `(A->B)=(X->Y)` implies `A=X, B=Y`. Those more familiar with union-find terminology may prefer "representative" over "root". ```python def check_components(uf: UF) -> List[Eq]: # Every UF component is in a star shape, meaning uf.root() is O(1) # Since there are O(N) components and O(N) processors, this is entirely O(1) fn_pairs = [(F, uf.root(F)) for F in uf if is_fn(F)] # "Down" decomposition return [ eq for F, R in fn_pairs if F != R # F isn't the actual root itself # Because F=R, we have F.arg=R.arg and F.ret=R.ret for eq in [Eq(F.arg, R.arg), Eq(F.ret, R.ret)] ] ``` Why does this actually work to give us all the progress we need? What is this doing? Can this actually merge currently-disjoint types? Since it only compares already-equal types, how can their children be different in the first place? It's because the consequences of equating two types haven't necessarily reached their children yet. Let's say we have a (sub)term like this: `\f. (g (f x)) (f y)`, where `f` is applied twice to different outer terms, `x` and `y`. We could get two different constraints like so: ```python F=A->B # from f x F=X->Y # from f y ``` Because we asked `bulk_merge` to give us flat connected components, the component of `F` might currently look something like this: ```python # Every element here points directly to its root # uf.parents[i] == (X->Y).type_id (X->Y) <- {F, A->B, C->D, ...} # Reminder: each one of these types is represented by u32 type IDs ``` Naively, we should compare every pair of functions in the component and produce equalities from them. That would mean we'd need `O(N^2)` comparisons, requiring `O(N)` time on `O(N)` processors, even if we memoized to keep space `O(N)`. The trick: why do we need to compare every pair? We already know each function type must be equal to its root: ```python A->B generates [X=A,Y=B] # Down one level from (X->Y)=(A->B) C->D generates [X=C,Y=D] ... # X->Y generates nothing because X->Y *is* X->Y, wow! # F also generates nothing because F is a TVar rather than a TFn ``` ![[dphm-fig-star.svg]] With a component of size `k`, we get up to `2(k-1)` possible equations. Each element of a component (and, by disjointness, of the entire UF) can only contribute 2 (or 0) equations, keeping us in `O(N)` space and `O(1)` time. And so we have: 1. `bulk_merge`: publish constraints to the global UF structure. 2. `check_components`: inspect the UF for newly-found constraints and emit them. 3. Loop if there's any new constraints left after `normalize`. ## Why this works We have two things to worry about in our constraint discovery: inventing an equality that isn't required (or possibly wrong), and failing to discover one that _is_ required. If we can overcome those, then: does our algorithm stop, and is its answer the principal type? ### Our constraints are constrained Remember that our initial constraints came directly from STLC typing rules applied to our AST nodes. An application really does require the applied function to accept the argument's type and return its result's type, and a lambda function really does have a type of `type(param)->type(body)` (wow!). After that, we only get equalities two ways: transitivity (`bulk_merge`) and Down (`check_components`). Both are simple consequences of how types work. Any typing satisfying `A = B` and `B = C` satisfies `A = C`, and any typing satisfying `(A->B) = (X->Y)` satisfies `A = X` and `B = Y`. Every equality we ever end up holding is required by the program. ### We don't skip consequences What about constraints hiding in the comparisons we skipped? Comparing two function types directly would immediately equate their arguments and results. Comparing both with their root forces those same equalities through transitivity: ```python # Given a UF looking like this: (A1->A2) <- {(X1->X2),(Y1->Y2),...} # Other components, assuming X1/X2/Y1/Y2 are also function types # x.a, x.r are just short for x.arg, x.ret (X1.a->X1.r) <- {X1,...} (Y1.a->Y1.r) <- {Y1,...} (X2.a->X2.r) <- {X2,...} (Y2.a->Y2.r) <- {Y2,...} ... # check_components produces these comparison tuples: [(A1->A2, X1->X2), (A1->A2, Y1->Y2), ...] # Decompose into children: [A1=X1, A2=X2, A1=Y1, A2=Y2,...] # Publish via bulk_merge, which gives the following: # Z1->Z2 is a pre-existing function record, selected as this component's root (Z1->Z2) <- {A1, X1, Y1, (X1.a->X1.r), (Y1.a->Y1.r),...} # This component says: (Z1->Z2)=A1=X1=Y1=... # X1 and Y1 are now equal! # What about X1.a=Y1.a, X1.r=Y1.r? # check_components once more, and we get to the X1.a/X1.r level [Z1=X1.a, Z2=X1.r, Z1=Y1.a, Z2=Y1.r] # Upon publishing, we get this via transitivity, then loop: Z1=X1.a=Y1.a ``` ![[dphm-fig-uf-rounds.svg]] Any deeper structure "missed" from the root-only comparison will be examined in subsequent rounds. We only need the component scan to expose one level per round. Comparing types through the root element may change _when_ we discover a constraint, but not _if_. Once normalization drops already-satisfied equations, an empty frontier means all the root-comparison equations already hold in our UF. This also means that there's nothing left we _need_ to recurse into, because the children of a function type must *also* agree with *their* roots, because `normalize` dropped them. ### Why the loop finishes If the frontier isn't empty, it contains a pair of distinct components that the next publication must merge, or otherwise reject as incompatible. That's **progress**: unfinished work forces a new merge or an error. Components merge and never split, meaning the number of distinct components decreases **monotonically**. There were `O(N)` initial components, we don't introduce any, and each loop has to merge at least one pair of components. Thus there are at most `O(N)` rounds until monotone convergence. Since each round settles (at least) one level across all function types, there are in fact at most `D <= N` rounds. ### A quick correctness argument We never added an arbitrary restriction: every equality was required, and we didn't skip any consequences. The read-back type is therefore the most general one, the principal type, with a distinct type variable for every non-rigid component. The rigid-root rule guarantees that we never report an unknown (`TVar`) where a function or atom was required. Amazingly, for just principal typing, we don't actually need an "Up" direction (congruence), i.e. to go from `A=X, B=Y` to `(A->B)=(X->Y)`[^15]. ## What's next Arguments aren't proofs, and this post has handwaved away not only proofs but even arguments -- we're doubly-handwaved! That being said, at least there's prior art in this direction. Even if you buy the general correctness arguments, I also haven't given you any good reason to expect that this algorithm (err, family of algorithms) would be GPU-amenable. I can _say_ "it looks decent on CUDA", at least compared to a baseline sequential Rust solver on large ASTs (`N > 10^6`). But I think it's better to just give out the code + benchmarks. Speaking of real-world performance, there are many optimizations I haven't brought up here. Many of which even came from myself, surprisingly. I guess there's still a bit of time left for that kind of hobbyism. One simple optimization: you can add an extra Down per loop, which amortizes merging. And here's one which may be less obvious because it's less optimization and more ... uh, well, literally less optimization: just use `CAS` for `bulk_merge` when updating a type's parent. Since parallel compare-and-swap has only one winner per attempt, its asymptotic runtime is the number of potential conflicts: `O(constraints) = O(N)` (per loop). Practically, there's going to be like `2` conflicts. Maybe `2.5`, if you're unlucky. If this argument makes you sad, you might be a theorist! Or just really good at algorithms -- the `O(log(N))` version is no joke. There's also a "simpler" `O(log^2(N))` [algorithm](https://arxiv.org/html/1812.06177v5#S3) for parallel CC which can be adapted from CRCW to CREW (which is far more reasonable for approximating real parallel hardware). Of course, there's also the obvious other question: what about polymorphism? Well... it might be a bad time to be short on (V)RAM. ## Closing thoughts ...for now CUDA code will be out... soon! At least there's a [sequential sketch](https://gist.github.com/wiwa/c8e60f36e2a63045dd4a0427ff1767fe) for now. This has been a long and difficult post to write, so sorry if it hasn't been the clearest. In fact, the simplified "merge and decompose" version I presented is far from what I even started off with, which was a rather chaotic mess. I also had this Down-closure step called `frozen_unify` which was pretty much classic recursive unification, except iteratively with an explicit stack. It did (partial) Up congruence at the same time, because why not -- that's what typical unification code would do. Turns out, it was both unnecessary (for principal typing) and insufficient (for global congruence). Oh well. I'm _so_ glad I don't have to exposition that. This post has also been 3 years in the... well, not making. Mostly just in the not-doing, and only approximately a couple months in the making, then another month or so in the writing. Most of _that_ was just remembering what the hell even I did, more prior-art research and, tangentially, evolving implementations/optimizations. I still hate waiting for things. Thanks for reading! ___ ## AI Aside Approximately 90%+ of this was typed up by me and my brain. Not including graphics (...those are hard). I tried using AI more for writing, and had it draft multiple attempts at expositions, but I simply didn't like them for the most part. I couldn't even follow along some of them, and I'm the one who came up with the algorithm in the first place! Ironically, I now somehow have the feeling that using AI would be "more technically correct" for algorithmic exposition. That being said, AI was quite helpful for editing, even if it were mostly annoying, and for making sure the footnotes were correctly numbered. However, AI was definitely instrumental in helping me even get this blog post out in the first place. I was able to use it to better understand and simplify the algorithm, a process which was a lot less "automatic" than one would think or hope for. It helped me clean up old files (which I had previously left in bad states), found prior art, wrote a bunch of tests, and even wrote proofs in Lean. For the Lean part, I found that, left to its own devices, AI was prone to either underproving, or possibly worse, going on insane rabbit holes. No, we don't need to embed CUDA's `atomicCAS` in Lean (exaggerating, but not by much). What was kind of surprisingly awesome was having it pull down real-world AST examples (e.g. Elm, SML, OCaml), compiling them into a useful format for the solver for performance testing, and generating test inputs which had some similar statistics. It should be obvious, but there's a massive difference between AI now as opposed to 3 years ago, when it was effectively worse than useless, failing to even work through a simple lambda calculus interpreter without hallucinating. My first chat with Claude was back in July 2023, soon after Claude 2's release. Back then, it was a lot less capable, but also a lot less arrogant. The auto-generated chat name: "STLC implementation with Algorithm J". Crazy thing is that I didn't even remember this, until Claude somehow pulled it up in a recent chat! AI: very fun when it works, mildly despairing when it doesn't (or when it works _too_ well), and insanity-inducing when it literally does the exact opposite of what you agreed on 5 minutes ago. [^1]: Turns out this is harder than I expected, and not only because my first attempt was simply stratification. [^2]: Not really. Stacks are monoids, which is the hint that "it uses a stack" doesn't make an algorithm serial: [The stack monoid revisited](https://news.ycombinator.com/item?id=27164009). [^3]: One such prior art: [Parallel Type-checking with Saturating LVars](https://www.ccs.neu.edu/home/samth/parallel-typecheck-draft.pdf). [^4]: My first attempt at DPHM used a pretty literal 0CFA shape, but I departed from it in an attempt to make let-polymorphism (and the entire algorithm) easier to reason about. Not that I was able to make let-poly _good_, though -- not even correct! [^5]: Surprisingly, we won't need this for our decomposition-only solver. [^6]: The occurs check is itself a parallel graph problem (cycle detection on the component graph), and it can be amortized or run once after the loop instead of every round. Bookkeeping note: for infinite-typed programs (i.e. occurs-check failure), rejection time will still be `O(N)` (or rather, `O(N*log(N))` in our specific sketch). [^7]: Okay, there's also a third way, "Up" congruence, which is not necessary for principal typing, but is useful for tooling: `A = X, B = Y` => `A->B = X->Y` [^8]: We write `\` instead of `λ` because I cannot be typing `λ` all the time: `\x.foo` instead of `λx.foo`. [^9]: Bellia and Occhiuto: [N-axioms Parallel Unification](https://journals.sagepub.com/doi/abs/10.3233/FUN-2003-55203), Fundamenta Informaticae 55 (2003). Their baseline `UNIFY` works in similar rounds: decompose every pair of equal terms one level, take the transitive closure, and repeat until nothing changes, checking for clashes and cycles at the end. Their contribution `Ax-UNIFY` is... quadratic space and processors? Why would you do this. [^10]: Even types like `A1 => A2 => ... => A{n}` are typically the curried form of a high-arity function `(A1, A2, ...) => A{n}`. We can treat such "wide" functions as contributing just one layer of `D`: depth comes from sequential dependency, and a multi-arity function exposes all of its constraints at once. Such an extension will not be shown here. [^11]: Then again, being ~1000 days late for just this post... sorry, I have [a company to build](https://www.paraquery.com). [^12]: A lambda's constraint mentions the arrow `binder_type(x) -> type(body)`; an application's mentions `type(a) -> type(f a)`. Each of those is one `TFn` record, allocated up front, so the loop never allocates. [^13]: We can store every type, regardless of var/atom/fn, as a `u64`, distinguishably: `list[Type] ~ list[u64]`, and `list[TInfo] ~ list[u96] ~ list[Vector3] (lol)`. With native 2-ary functions `(A, B) -> C`, `TInfo ~ u128`. When (V)RAM is premium real estate this becomes a questionable encoding. Micro-optimization note: one way to understand a type by its ID alone is to assign type IDs like `[tatoms | tvars | tfns]`, i.e. IDs of `TFn`s are always higher than for `TAtom`s and `TVar`s. [^14]: `bulk_merge` only merges types. The function structure still matters: equating `A -> B` with `X -> Y` requires equating their children, and that's `check_components`'s job, not `bulk_merge`'s. Likewise the occurs check is separate. [^15]: However, without Up, the UF doesn't necessarily equate all "equal" types, i.e. they might still be in different components, even though they should be equivalent and we do read them out to be the same types. To get this global congruence, we need one level of Up-congruence per round. We'd need a GPU hashmap for this.