# 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. ## 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.) But let's just get to it now! ### What Okay, maybe "Towards GPU Type Inference" was a bit too much hype. 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 we might sneakily, handwavedly even call it GPGPU-able. "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 is a massive pain, and doesn't really change the outcome much (...probably). 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 proof-checker, please. There's a whole parallel computer sitting right there, whether GPU or multicore (SIMD) CPU. ## Isn't Type Inference Serial? Typically, yes. Algorithm W and its state-mutating cousin, Algorithm J, are basically 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. STLC type inference (i.e. 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, lol. 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 is: write down one constraint per AST node, then solve them. Take an application `f x`. We don't know the type of `f` or `x`. But `f` had better be a function that accepts whatever `x` is and returns whatever `f x` is. Name those three types `F`, `X`, `R`: ```python F = X->R # or Eq(F,X->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. ### Two ways to get more equalities Given a pile 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) = (C -> D)` gives `A = C` and `B = D`. There are also two ways to fail: a clash (`Int = Bool`, or `Int = A -> B`), and an infinite (cyclic) type (`X = X -> R`, from `\x. x x`[^8]). That being said, 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 at once is just 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_, emit two child constraints. The key is that this actually exposes more information. The trick: to get all the information we'll need, we only need to consider `N` rather than `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, technically, we can sometimes produce more than one "level" of constraints at once, I don't believe that matters asymptotically -- we need to publish and globally sync. Publishing a Down round is what merges two components. That allows us to compare new pairs of functions for new constraints in the next Down round, and we loop. What this algorithm does per loop is have each processor (thread/worker) look at a type and "deepen" it layer by layer, e.g. something like: ```python round 0: A1 round 1: B1->B2 round 2: (Bool->C1)->(C2->Int) round 3: (Bool->(D1->Int))->(Int->Int) ... ``` This per-level deepening is also not a new invention. Well, at the time, I thought it was new, 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, simultaneously. Round one settles which unknowns are functions. Round two settles their children (their argument and result types). Of the children, those who are functions get _their_ children settled in Round 3, and so on. 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)) ``` 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's 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 ideas about "performance" (e.g. making everything compact integer arrays). 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). Python code (illustrative/sequential), CUDA, 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 = O(N) parallel processors on a CREW machine**. ### 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 BinderId = Int # NodeId of a variable's binder 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 `N`: ```python nodes: Array[Expr] # NodeId -> Expr binders: Array[BinderId] # NodeId -> BinderId types: Array[TInfo] # NodeId -> TInfo @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, res) # a function whose children are type IDs; arg -> res ``` Variables (binders and occurrences) initially map to `TVar`. Literals map to `TAtom`. Allocate function descriptors as needed for lambdas[^12]. `N` records, all allocated up front. 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]. 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. #### 2. Initial Constraints Emit one constraint (equation) per node 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))` | Emitting these is an embarrassingly parallel map, and each equation is effectively a `u64` (a pair of `u32` types). The initial state is an array of type records (`TInfo`), an array of constraints, and an array-based union-find (`UF`) with every type in its own component. ```python types: Array[TInfo] initial_constraints: Array[Eq] uf: UF = UF(parents: Array[TypeId]) # TypeId -> TypeId ``` ### 3. The Loop A slightly more detailed sketch: ```python constraints: Array[Eq] = initial_constraints while constraints: uf = bulk_merge(uf, constraints) # publish constraints = check_components(uf) # Down, one level constraints = normalize(uf, constraints) # drop satisfied equations, 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. 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. We ask two extra things of 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 is one of them, 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. #### check_components To me, the surprising _star_ of the show is `check_components`. It looks too cheap. `check_components` says: for each component, pair all its elements (types) against its root, then decompose into equations of their children. `(A->B)=(C->D)` implies `A=C, B=D`. ```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_roots = [(F, uf.root(F)) for F in uf if is_fn(F)] # "Down" decomposition return [ eq for F, R in fn_roots 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? 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 can get two different constraints: ```python F=A->B # from f x F=C->D # from f y ``` The connected component of `F` might look like this: ```python # Every element points to the root; uf.parents[type_id] == (A->B).type_id (A->B) <- {F, A->B, C->D, X->Y,...} ``` Naively, we can compare every function in the component and produce equalities from them. However, even if we were to memoize, we would still need `O(N^2)` comparisons, i.e. `O(N)` time on `O(N)` processors. The trick: why do we need to compare every pair? We know they must all be equal to the root: ```python C->D generates [A=C,B=D] # Down one level from (A->B)=(C->D) X->Y generates [A=X,B=Y] ... # A->B generates nothing because A->B *is* A->B, wow! ``` 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 to the global UF structure. 2. `check_components`: inspect the UF for newly-found work. 3. Loop if there's work left after `normalize`. ## Why this works We have two things to worry about: inventing an equality that isn't required (or possibly wrong), and failing to discover one that _is_ required. Then: does it stop, and is the answer the principal type? ### Our constraints are constrained The initial constraints are the STLC typing rules. An application really does require the function to accept the argument's type and return the result's type; a lambda really does have the type `type(arg)->type(body)` (wow!). After that, we only get equalities two ways: transitivity (`bulk_merge`) and Down (`check_components`). Both are consequences: any typing satisfying `A = B` and `B = C` satisfies `A = C`; any typing satisfying `(A->B) = (C->D)` satisfies `A = C` and `B = D`. So every equality we ever hold is required by the program. Nothing is invented. That's **preservation**. ### We don't skip consequences What about constraints hiding in the comparisons we skipped? Comparing two function records directly would equate their arguments and results. Comparing both with the anchor forces those same equalities through the anchor’s children: ```python # Given a UF looking like this: (A1->A2) <- {(B1->B2),(C1->C2),...} # x.a, x.r are just short for x.arg, x.ret (B1.a->B1.r) <- {B1,...} # Assuming B1 is a function type, else we're done (C1.a->C1.r) <- {C1,...} (B2.a->B2.r) <- {B2,...} (C2.a->C2.r) <- {C2,...} ... # check_components gives: [A1=B1, A2=B2, A1=C1, A2=C2,...] # Publish via bulk_merge, which gives the following: # D1->D2 is just the root of the component (D1->D2) <- {A1, B1, C1,...} # we find that B1 and C1 are the same component # This component says: A1=B1=C1=(D1->D2) # check_components once more, and we get to the B1.a level [D1=B1.a, D2=B1.r, D1=C1.a, D2=C1.r] # Upon publishing, we get this via transitivity: D1=B1.a=C1.a ``` Any deeper structure "missed" from the anchor-only comparison will be examined in subsequent rounds. We only need the component scan to expose one level per round. Comparing through the anchor may change _when_ we discover a constraint, but not _if_. After normalization drops already-satisfied equations, an empty frontier means all the anchor-comparison equations already hold. The argument above then says every all-pairs decomposition equation holds too. This also means that there's nothing left we _need_ to recurse into, because the children of a function type *also* agree with *their* representatives. ### Why the loop finishes If the frontier isn't empty, it contains a pair of distinct components that the next publication must merge, or reject as incompatible. That's **progress**: unfinished work forces a new merge or an error. Components merge, never split, meaning the number of distinct components decreases **monotonically**. There were `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 `N` rounds. ### A quick correctness argument We never added an arbitrary restriction: every equality was required (preservation), and we didn't skip any consequences. The read-back type is therefore the most general one, 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 the "Up" direction (congruence), i.e. to go from `A=C, B=D` to `(A->B)=(C->D)`[^15]. ## What's next Regardless, arguments are not 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. 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 (array index). Asymptotically, `O(constraints) = O(N)`. Practically, there's going to be like `2` conflicts. Maybe `2.5` if you're unlucky. There's also a semi-simple `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). Another, simpler optimization: you can add one more Down per loop. 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 Code will be out... soon! At least the Python version. Then you can take your favorite AI and probably have it give you a better idea of what I'm claiming. This has been a long and difficult post to write, so sorry if it hasn't been the clearest. In fact, the simple "decompose and bulk merge" 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 basically did classic recursive unification, except iteratively, before merging. 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. ___ ## AI Aside Probably something like 90%+ of this was typed up by me and my brain. I tried using AI more, 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 still really helpful for editing, even if mostly annoying. And for making sure the footnotes were correctly numbered. AI was also instrumental in helping me even get this blog post out, helping me clean up old files I had previously left in bad states, finding prior art, testing, and even literally Lean-ifying things so I could be less antsy. Extremely importantly, it helped me simplify the algorithm, which was a lot less "automatic" than one would think. 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. AI: very fun when it works, mildly despairing when it doesn't (and when it works _too_ well), 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. I might rather go straight to "R2", System F restricted to rank-2 types, where the polymorphism is expressed as relations between types instead of levels. [^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)`. [^7]: Okay, there's also a third way, "Up" congruence, which is not necessary for principal typing, but is useful for tooling: `A = C, B = D` => `A->B = C->D` [^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. [^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. [^14]: `bulk_merge` only merges types. The function structure still matters: equating `A -> B` with `C -> D` 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.