Catalog vs. Unison

PFCL language reference · composure.systems · part of /catalog/related-work

Unison is the closest prior art to the PFCL catalog model, and the comparison worth stating most carefully. Both systems identify code by the hash of its content rather than by a file path or a version number. This page compares the two directly: where they're the same idea, and the two places they diverge — alpha-equivalence, and update propagation.

1.What's the same

Unison's own documentation states the shared premise plainly: a codebase is "a structured object" in which "terms and types are identified by their implementation, not just their name," and the codebase format stores "a hash of the syntax tree of a term or type" rather than storing code as text files.[1] This is the same starting move the PFCL catalog makes — identity as a hash of content, name as separate metadata.

The consequence Unison draws from this is one PFCL draws too: dependency conflicts, in the traditional sense, cannot occur. Unison's own framing of this is worth quoting closely, because it's the same claim made from the same premise:

"Dependency conflicts are, fundamentally, due to different definitions 'competing' for the same names... Consider an Email type, one from v1 of Alice's library, and another from v2... it's perfectly fine to have two different Email types floating around the codebase. They exist as different types, with different hashes, and you can work with both at the same time."[2]

This is structurally identical to the diamond-dependency argument on /identity §4: there's nothing to conflict over, because there's no shared mutable name for two different things to compete for.

Caching follows from the same premise in both systems. Unison states that once a definition is parsed and typechecked, "no one has to do that ever again" — the result is cached permanently, keyed by hash, and the cache is part of the codebase format itself, not a build artifact that can go stale.[3] The PFCL catalog's caching model — identity as cache key at every layer, no invalidation — is the same idea, for the same reason: a hash-keyed cache can't go stale, because the key changes if and only if the content does.

Naming as a separate layer is the same design decision in both systems. Unison's documentation states this directly, with an analogy worth citing in full: "Unison definitions are like stars in the sky. We can discover new stars and create new star maps that pick different names for the stars, but the stars exist independently of what we choose to call them."[4] That's the identity/naming separation specified on /identity §1, arrived at independently and stated almost the same way.

2.Where they diverge: alpha-equivalence

This is the sharpest and most concrete difference between the two systems, and it's a difference in the hash function itself, not just in tooling built on top of it.

Unison's own FAQ documents its hashing algorithm directly. For a (possibly mutually recursive) group of definitions, Unison first replaces every bound variable with a De Bruijn index — a position-based reference that doesn't depend on what the variable was named — and only then hashes the resulting structure: "this transformation makes the elements of the cycle independent of any names."[5] The practical result, described in an independent write-up of the language: writing the same function "with different names, even with different variable names... Unison will just store one function."[6]

This means Unison's identity function is extensional up to alpha-equivalence — two definitions that are alpha-equivalent hash to the same value and are, as far as the codebase is concerned, the same definition.

PFCL's identity function stops one step earlier, deliberately. Per /identity §2–§3, identity is the hash of canonical source text — canonicalization removes only whitespace and comments, and performs no variable renaming, no De Bruijn conversion, no normalization of any kind. Two alpha-equivalent PFCL definitions — differing only in a bound-variable name — have different identities.

The PFCL design document frames this as a ladder: any admission of a semantic quotient into identity has no principled stopping point short of undecidability, and alpha-equivalence is the first, most tempting rung of that ladder. Unison's own hashing algorithm is a real, working counterexample to the "no principled stopping point" framing taken literally — Unison does stop at alpha, and only at alpha, and has run in production at that stopping point for years. The PFCL position isn't that stopping at alpha is unworkable; it's a different design choice, trading Unison's automatic deduplication of alpha-variants for a simpler, purely-textual identity function with no normalization step to specify, implement, or reason about the soundness of. Where Unison folds alpha matching into identity itself, PFCL pushes it into the graded equivalence relation instead — see /catalog/equivalence grade 1 — where it sits as one recognized case among several rather than as a property of identity.

3.Where they diverge: update propagation

When a definition changes in Unison, the update command automatically propagates the new definition to its transitive dependents, provided the old and new types are compatible. Unison's own FAQ walks the mechanism directly: after updating foo, "Unison assumes... you want to propagate the updated definition of foo to the set of transitive dependents of the old term... This propagation works recursively, so it deals with dependents of bar as well, and their dependents in turn, and so on."[7] If the old and new types aren't compatible, automatic propagation stops, and the update has to be resolved by hand at that frontier.

PFCL has no equivalent propagation step. Per /identity §4, a fix produces a new identity; the name is rebound to point at it; callers referencing the name pick up the new identity the next time they're loaded and resolved — there is no rewriting of the dependents' own bodies, because a caller referencing a name was never storing a copy of the callee's hash inside itself the way Unison's propagation model implies. The two models solve adjacent but different problems: Unison's propagation asks "how do I push a change through everything that already committed to the old definition's hash," which is a real question in a system where dependents capture callee hashes directly. PFCL's rebind model doesn't have that question in the same form, because name resolution happens at load time rather than being baked into a dependent's stored representation — the trade-off is that PFCL's callers are only ever as current as their next load, where Unison's propagation actively pushes the update to them.

4.Where they diverge: canonical form scope

Related to section 2 but broader: Unison's canonical form is a property of the compiled/typechecked representation — the hashed structure is a processed AST with names erased and cycles restructured, not the source text. PFCL's canonical form is a property of the source text itself — canonicalization is "parse and reprint," a much smaller transformation, possible in PFCL specifically because the grammar has no infix operators and no syntactic sugar to normalize away (see /identity §3). Unison's richer canonicalization is necessary background for its alpha-folding (section 2 above); PFCL's narrower one is what keeps sha256sum sufficient to verify identity without needing to run any part of the language's own toolchain first.

5.Summary table

PropertyUnisonPFCL catalog
Identity basisHash of typechecked, name-erased ASTHash of canonical source text
Alpha-equivalent definitionsSame identity (deduplicated automatically)Different identities
Verifiable withUnison's own toolchain (typecheck + hash)sha256sum alone
NamingSeparate mutable mapping ("star map")Separate mutable mapping (name→hash)
Update mechanismAutomatic propagation to compatible dependentsName rebind; dependents resolve on next load
Diamond dependenciesStructurally avoided (different hashes coexist)Structurally avoided (different hashes coexist)
CachingPermanent, hash-keyed, part of codebase formatPermanent, hash-keyed, part of catalog model

Notes

  1. Unison Language. docs Unison — Codebase and tooling setup / codebase-editor-design. "The Unison codebase format has a few key properties: Terms and types are identified by their implementation, not just their name. The codebase stores a hash of the syntax tree of a term or type." github.com/unisonweb/unison
  2. Unison Language. docs Unison — The big idea. unison-lang.org/docs/the-big-idea
  3. Unison Language. docs Unison — The big idea. "Once anyone has parsed and typechecked a definition and added it to the codebase, no one has to do that ever again." unison-lang.org/docs/the-big-idea
  4. Unison Language. unison/docs/codebase-editor-design.markdown. github.com/unisonweb/unison
  5. Unison Language. docs Unison — General Unison FAQ's. "We treat a set of mutually recursive definitions as a single 'cycle' for hashing purposes... this transformation makes the elements of the cycle independent of any names." unison-lang.org/docs/usage-topics/general-faqs
  6. Athaydes, R. A look at Unison: a revolutionary programming language. Independent third-party account, cited for the practical restatement of the De Bruijn-hashing consequence documented in note 5; verify against official Unison documentation before relying on this specific phrasing. renato.athaydes.com
  7. Unison Language. docs Unison — General Unison FAQ's. "Unison assumes that... you want to propagate the updated definition of foo to the set of transitive dependents of the old term... This propagation works recursively." unison-lang.org/docs/usage-topics/general-faqs

References

  1. PFCL. Identity: why identity stays intensional, and the naming layer. /identity.
  2. PFCL. Equivalence: the graded relation, including alpha-normalization at grade 1. /catalog/equivalence.
  3. PFCL. Catalog: content addressing, admission, retirement. /catalog.