Type aliases for Unison#6243
Draft
runarorama wants to merge 22 commits into
Draft
Conversation
Add the data-model scaffolding for transparent type aliases: - RtTypeAlias variant on ReferenceType, shared by type and ability-row aliases (the namespace entry stores which kind it is). - Unison.TypeAlias (v1) and U.Codebase.TypeAlias (v2): paramNames + body representations; arity, dependencies, vmap/rmap/amap helpers. - Unison.TypeEntry: sum over Decl and TypeAlias for codebase API returns. - TermParser doc-link handlers treat RtTypeAlias the same as RtType. See docs/type-aliases.markdown for the full design. Storage and codebase API land in follow-up commits.
Local storage: - New ObjectType.TypeAliasComponent (4) and TempEntityType.TypeAliasComponentType (5) - U.Codebase.Sqlite.TypeAlias.Format with TypeAliasFormat / SyncTypeAliasFormat - Serialization put/get/decompose/recompose + decoder wrappers - saveTypeAlias / loadTypeAliasByReference / isTypeAliasReference at Ops layer - Reference-only (non-recursive) refs in alias body; alias entries are not components (pos always 0). Dependents index updated on save. - Schema bumped to 27 with a no-op migration that signals format support. Codebase API: - Codebase record gains getTypeAlias, getTypeEntry, isTypeAlias, putTypeAlias. - TypeAlias body conversions (v2 <-> v1) in SqliteCodebase.Conversions. - putTypeAlias requires dependencies to already exist (no buffered defer needed; aliases are non-recursive). Share sync protocol: - New Share.TypeAliasComponent record + JSON instances; TAC constructor on Share.Entity; EntityType.TypeAliasComponentType. - CBOR wire format extended with TypeAliasComponentTag (5). - tempEntityToEntity / entityToTempEntity wired bidirectionally. - EntityValidation reports UnsupportedEntityType for aliases for now (matches how PatchDiff / NamespaceDiff are handled); real hash verification waits until alias hashing semantics are finalised.
Hash inputs:
- Outer tag byte 3 (distinct from terms=1 and decls=2).
- Body wrapped in absChain over the parameter names so alpha-equivalence
on params falls out of the existing ABT hashing machinery for free.
- Inner Alias tag distinguishes alias bodies from raw type bodies.
- Ability-row canonicalization is inherited from TypeF's Hashable1
instance (Effects sorts and dedupes its element hashes).
Result: type alias Endo a = a -> a and type alias Endo x = x -> x produce
the same ReferenceId; {IO, Exception, Http} and {Http, Exception, IO}
canonicalize identically. Aliases are non-recursive single-element
components (pos = 0).
Wiring:
- Unison.Hashing.V2.TypeAlias module + re-export from Unison.Hashing.V2.
- v2ToH2TypeAlias in Convert2 for v2 -> h2 conversion.
- U.Codebase.TypeAlias.Hashing.verifyTypeAliasFormatHash impl resolves
local refs against the alias's lookup vectors, converts to the v1
hashing form, hashes, and compares.
- HashHandle gains verifyTypeAliasFormatHash and a new TypeAliasHashingError.
- v2HashHandle wired with the new implementation.
- EntityValidation no longer stubs aliases as UnsupportedEntityType; it
decodes and validates them the same way decls are validated.
Adds the `type alias <name> <params> = <type-expression>` surface syntax. Aliases don't accept `structural`/`unique` modifiers (parser rejects). The lexer now emits a Reserved token for the `alias` keyword so the parser can match it positionally after `type` rather than as an identifier; `alias` was already in the reserved keyword set, so this doesn't break any existing source. Elaboration lands as the next slice: `synDeclsToDecls` raises `TypeAliasNotYetImplemented` (a new structured error variant) so users get a clear "the parser sees it; the elaborator doesn't yet" message rather than a confusing parse error. The error is rendered by PrintError with a pointer to docs/type-aliases.markdown. Includes a unit test confirming the surface syntax parses and the structured error is produced.
Aliases declared in a `.u` file are now expanded inline at use sites within data and effect constructor types. The alias declarations themselves are stripped from the resulting UnisonFile — they live as parse-time substitution machinery, with no codebase persistence yet. Unison.TypeAlias.Expand: - `expand`: walks a Type and replaces saturated alias applications with their bodies. Unsaturated uses produce `UnsaturatedAliasUse` errors. - `normalize`: topo-sorts aliases and pre-expands cross-references so each body is alias-free. Returns `AliasCycle` on dependency cycles. - Bare references to non-nullary aliases are detected as unsaturated. FileParser.synDeclsToDecls: - Partitions parsed decls into data, effect, and alias maps. - Normalizes the aliases (cycle detection). - Expands aliases in every data/effect constructor type. - Aliases never appear in the resulting data/effect declarations. New parse errors `UnsaturatedTypeAlias` and `TypeAliasCycle` replace the `TypeAliasNotYetImplemented` stub for normal use; PrintError renders both. The old `TypeAliasNotYetImplemented` variant stays as a fallback for codepaths the elaborator hasn't grown into yet (term type sigs). Tests cover successful expansion in data decls, the unsaturated-use error, and the cycle error. Term type signatures still go through the old codepath; expanding aliases inside terms is the next slice.
…ected Clarifies the design's stance on unsaturated alias application. Unison's Type.F has no Lam constructor; introducing one (or repurposing the bare ABT.Abs binder in Type) would be a separate language feature. Until that lands, aliases are saturated substitution macros — partial application is rejected by the elaborator. A note in expand explains the why for future readers who wonder why we don't just curry.
`f : Endo Nat; f x = x` now works alongside `type alias Endo a = a -> a` in the same file. The alias is substituted in the term's type-annotation node before name resolution runs — `bindNames` would otherwise fail to resolve the alias name as a type ref. - Unison.TypeAlias.Expand.expandInTerm: walks a Term via ABT.transformM, applies `expand` to every Type carried by a `Term.Ann` node. That's the only place `Term.F` carries inline types; Constructor/Request/TypeLink use References and don't need expansion. - FileParser.synDeclsToDecls now returns the normalized alias map as a third element. The aliases stay file-local for now — no codebase persistence — but they're available to expand into terms. - Expansion runs after `Term.generalizeTypeSignatures` and before `Term.bindNames`, so the alias body's free type vars (which the alias body inherits naturally) get generalized correctly and the resulting alias-free type then resolves through name binding as usual. - Unsaturated alias use inside term sigs produces the same `UnsaturatedTypeAlias` parse error as it would in decls. Test confirms `type alias Endo a = a -> a; f : Endo Nat; f x = x` parses cleanly.
`type alias Web = {IO, Exception}` now parses and expands correctly when
used inside `->{...}` rows. The alias's body is an `Effects [...]` list;
at use sites inside another row, the body is spliced (flattened in) and
the resulting row is deduped by structural equality (ignoring source
annotations).
- TypeParser exports `effectList` so alias bodies can use `{...}`
syntax in addition to regular type expressions. `synTypeAliasDeclP`
tries the row form first, falls back to value-type for non-row aliases.
- Expand.expand handles the `Type.Effects` case by recursing into each
element, splicing any nested `Effects` produced by row-alias expansion,
and deduping with `dedupRow`. Set semantics matches the design doc.
- Whether an alias is a type alias or a row alias is determined by the
body's shape — no separate keyword. Kind misuse (row alias in type
position, or vice versa) surfaces as an ordinary kind error from the
inferencer, not a bespoke alias error.
Test confirms `{IO, Exception}` aliases work as the qualifier on a
function arrow.
Adds a typeAliasesId field to UnisonFile and TypecheckedUnisonFile so aliases survive parsing through typechecking — they were previously consumed for in-file expansion only. The field carries (Reference.Id, TypeAlias) pairs. - synDeclsToDecls now returns the alias map with hashes computed via Hashing.hashTypeAlias. The hashes are deterministic within the file but not yet cross-codebase canonical, because alias bodies still contain free type Vars (name resolution hasn't run on alias bodies). Resolving bodies and rehashing is a follow-up. - Hashing.V2.Convert exposes hashTypeAlias which goes v1 -> h2 via a new m2hTypeAlias helper and reuses the existing hashing infrastructure. - All places that construct UnisonFileId / TypecheckedUnisonFileId or call typecheckedUnisonFile pass mempty / propagate the alias map as appropriate (Codebase, Codebase.Runtime, FileParsers, HandleInput, HandleInput.Run, HandleInput.AddRun, SlurpResult, Cli.Pretty, Cli.TypeCheck). - prettyUnisonFile renders aliases via _aliases for now — actually printing them goes in a follow-up; this just keeps the existing pretty-printer working through the structural change. In-file expansion still works exactly as before: 299 tests pass. Aliases are now in scope to be persisted by the codebase-add flow in the next slice.
End-to-end persistence: when a typechecked file containing type aliases is added to the codebase, each alias gets stored via `putTypeAlias`. The flow uses the hashing we already wired up in earlier commits. - Codebase.addDefsToCodebase iterates typeAliasesId' on the file and calls putTypeAlias for each alias (alongside the existing decl and term persistence). - Schema migration 023 inserts a row into object_type_description for type_id = 4 (TypeAliasComponent), and createSchema now invokes the migration so freshly created codebases include the row. Without this, saveObject hit a foreign-key constraint failure. - DeclPrinter exposes prettyTypeAlias and prettyTypeAliasHeader, rendering aliases as `type alias <Name> <params> = <body>`. Cli.Pretty.prettyUnisonFile threads aliases through alongside data and effect decls. Aliases are NOT yet added to typecheckedToNames: the slurp / Load path calls unsafeGetTypeDeclaration on type-position refs found in the namespace, and that throws on alias refs. Cross-file alias lookup (making `view Endo` work) is a follow-up that wires the codebase to distinguish alias refs from decl refs at lookup time. Transcript `unison-src/transcripts/type-aliases.md` runs cleanly to the end — the file with `type alias Endo a = a -> a; f : Endo Nat` parses, expands (`f` shows as `Nat -> Nat`), and `add` persists both. 299 tests still pass.
Three transcripts that exercise the follow-up gaps and currently fail:
- type-aliases-view.md — `view Endo` after add. Fails: alias not in Names,
so the lookup reports "names not found in codebase."
- type-aliases-slurp.md — alias declared alongside a term. Runs to
completion but the "Loading changes detected" output only lists the
term; the alias is invisible. (Negative-evidence test.)
- type-aliases-cross-file.md — alias declared in one stanza, used in a
later stanza (separate scratch file). Fails: parser can't resolve
`Endo` because the codebase's alias entries aren't consulted at name
resolution time.
These three failures bracket the remaining work:
1. view alias → needs alias-aware lookup + display
2. slurp shows alias → needs SlurpResult to carry alias entries
3. cross-file → needs name resolution to fetch alias bodies from the
codebase and expand inline before hashing
Each transcript will start passing as the corresponding piece lands.
The "Loading changes detected" output now lists added type aliases alongside terms and decls: + type alias Endo a = a -> a + f : Nat -> Nat Output.Typechecked gains a Map Symbol (TypeAlias Symbol Ann) field populated from the typechecked file's typeAliasesId'; the renderer in OutputMessages renders them via prettyTypeAlias and includes them in the existAdds check so the legend appears. Aliases aren't yet diffed against the codebase (no update/delete status) — they're always shown as adds. That parity lands when alias refs flow through the existing slurp diff machinery.
Previously synDeclsToDecls computed alias hashes from bodies that still contained free type Vars — `Var "Nat"` instead of `Ref natRef`. That meant the persisted alias hash was sensitive to source spelling rather than to the actual references it pointed at, and was not cross-codebase canonical. Now the flow is: 1. synDeclsToDecls returns aliases without hashes (just the body with unresolved Vars). 2. After environmentFor produces the file's resolved Names env, each alias body is name-resolved via Type.Names.bindNames — bound params stay as free Vars, everything else resolves to a TypeReference. 3. The resolved body is then fed to Hashing.hashTypeAlias, producing a hash that depends only on the param structure and the refs the body actually mentions. Two files declaring the same alias text against the same external types now compute the same hash; cross-file alias lookup gets back a body whose refs are already canonical, so downstream typechecking sees real Refs, not unresolved Vars. 299 tests still pass; the type-aliases transcript still completes.
Alias-aware lookup + display now plumbed through `view`: - typecheckedToNames includes aliases (Name → DerivedId), so name lookup for view/find returns the alias's Reference.Id. - Update2.typecheckedUnisonFileToBranchUpdates adds aliases to the Branch's types slot via BranchUtil.makeAddTypeName. Aliases now exist in the namespace after `add`. - Backend.displayType now returns Maybe — Nothing for refs that don't point at a decl (i.e. alias refs). New Backend.displayTypeAlias handles the alias case. Backend.definitionsByName populates a new typeAliasResults field on DefinitionResults. - ShowDefinition.showDefinitions / renderCodePretty / renderToConsole / renderToFile threaded with `Map TypeReference (DisplayObject () (TypeAlias Symbol Ann))`. Aliases render via DeclPrinter.prettyTypeAlias. - slurpTypes (in Load.hs) filters out alias refs before diffing, so the decl-shaped slurp diff doesn't crash on alias refs. Aliases are surfaced in the slurp output by the parallel path added in the previous commit. - Callers of the now-Maybe displayType updated: DefinitionSummary defaults to MissingObject; Local.Definitions / EditNamespace / EditDependents / LSP.Util.Wrappers thread mempty for the new typeAliases parameter where it isn't relevant. `type-aliases-view.md` transcript now passes: `view Endo` renders `type alias Endo a = a -> a`. The cross-file transcript still fails, but now in KindInference — the second file's parser sees Endo as a type ref but the kind inferencer can't classify an alias ref. That's the next slice.
Aliases were eagerly expanded at parse time so they never appeared in stored types or hashes. With lazy expansion they keep their refs in stored types: `f : Endo Nat` and `g : Nat -> Nat` are distinct definitions, alias names round-trip through view/slurp, and the alias becomes part of dependent identity. - TypeLookup carries `typeAliases` and is populated from the file (declsToTypeLookup) and from the codebase (typeLookupForDependencies) - KindInference gains `inferAliases` and `aliasComponentConstraints`, registering each alias ref with kind `k_1 -> ... -> k_n -> *` from its body - Typechecker.Context threads a `TypeAliasMap` reader through MT and whnf-expands alias refs at the head of types in subtype/check - FileParser puts file-local aliases in the Names env so bindNames resolves alias names to refs; eager expansion calls (expandInTerm / expand / expandAliasRefsInUnisonFile) are removed - SqliteCodebase decl coherency treats alias refs as zero-constructor entries instead of crashing on a missing DeclComponent - Transcript outputs now show preserved alias names
runarorama
changed the title
…sweep, propagate alias updates
- Delete docs/type-aliases.markdown — the lazy-expansion design now lives
in the PR body, so the file would be stale either way.
- Contextualize `alias`: drop it from the lexer/parser reserved-keyword
list and recognize it only as the second token of a `type alias`
declaration. Existing code using `alias` as an identifier parses
again.
- Remove the never-constructed `TypeAliasNotYetImplemented` parse error
and its renderer, the unused `Unison.TypeAlias.labeledDependencies`,
and the Var-/Ref-based `Unison.TypeAlias.Expand` API (`expand`,
`expandAll`, `expandInTerm`, `expandRefs`, `expandRefsInTerm`,
`ExpansionError`, `RefExpansionError`). `normalize` keeps a private
Var-substitution helper for alias-of-alias flattening.
- Wire cross-file alias update propagation:
- `UF.typeNamespaceBindings(Map)` and `UF.dependencies` include
aliases, so Update2 discovers dependents of an updated alias and
`typeLookupForDependencies` pulls in alias-body decls.
- `getDataConstructors` whnf-expands the scrutinee type so a `match`
against an alias-headed type sees the underlying decl ref.
- `makeUniqueTypeGuids` and `Codebase.UniqueTypeGuidLookup` skip
alias refs (they have no unique-type guid).
- New transcripts: `alias-identifier.md` (contextual keyword) and
`type-aliases-update.md` (compatible and incompatible alias body
changes).
…rences
Removes or rewrites comments that:
- Describe the old eager-expansion design (UnisonFile.Type.typeAliasesId,
SynTypeAliasDecl, FileParser synDeclsToDecls step 3)
- Point at the deleted docs/type-aliases.markdown (U.Codebase.TypeAlias,
Unison.TypeEntry)
- Restate the design principle redundantly at call sites of whnfAlias
- Trivia and bragging ("at the cost of a tiny bit of wasted envelope",
"No special preprocessing is needed at this layer")
- Were obvious from the code (typeNamespaceBindingsMap "includes alias
entries", "structural pass-through")
- Were overly confident or speculative (TypeLookup amap variance claim,
putTypeAlias call sequencing advice)
Also trims the cross-file transcript's repeated closing paragraph.
Aliases that reference other aliases used to be flattened at parse time
('normalize'/'expandVarRefs'), so `type alias Endo2 a = Endo (Endo a)`
landed in the codebase as `(a -> a) -> (a -> a)` with no dependency on
`Endo`. That was inconsistent with the lazy story for term/decl uses of
aliases.
Now alias references in alias bodies are preserved. `Endo2` stores
`Endo (Endo a)`, depends on `Endo`, and is re-emitted when `Endo`'s body
changes.
- `TypeAlias.Expand.normalize` is replaced by `inDependencyOrder`: it
cycle-checks and topologically sorts but no longer rewrites bodies.
- `FileParser.synDeclsToDecls` returns aliases in dependency order; the
alias-body name-resolution step folds across them so each alias's
`bindNames` sees an env extended with the already-hashed earlier
aliases. This means an alias body's free-Var reference to another
alias resolves to a ref before hashing.
- `Queries.getTransitiveDependentsWithinScope` now reports
`TypeAliasComponent` dependents in the types slot (previously dropped
as "impossible"), so an alias-as-dependent surfaces from the standard
query.
- `UpdateUtils.hydrateRefs` skips alias refs (and a new `hydrateAliases`
loads them separately).
- New `UpdateUtils.propagateAliasUpdates` + `aliasDependentsInOrder`:
for each alias dependent in dependency order, substitute updated refs
in the body, re-hash via `hashTypeAlias`, persist, and emit branch
updates (annihilate name + add name pointing at the new ref). The
substitution map accumulates so chains (Endo3 -> Endo2 -> Endo) flow
through in one pass.
- `Update2` partitions alias dependents from the render/re-typecheck
flow, seeds the substitution map from the user's added/updated names,
and appends the propagated alias branch updates after the primary
ones.
- New transcript `type-aliases-chain.md`: declares `Endo` and
`Endo2 a = Endo (Endo a)`, updates `Endo`, and verifies `view Endo2`
re-renders against the new alias.
The parser tests caught two cases that don't fit the single-phase alias
resolution:
- A data decl whose constructor references an in-file alias
(`type Box = Box (Endo Nat)`)
- An alias whose body references an in-file decl
(`type alias Web = {Foo, Bar}` where `Foo` and `Bar` are file-local
abilities)
These have mutual ordering requirements: decls want aliases hashed first,
aliases want decls hashed first. Split the alias batch in two and
sandwich `environmentFor` between them.
- `FileParser.file`: partition aliases by whether the body mentions any
file decl. Hash the "before" batch against `namesStart`; run
`environmentFor` with `namesStart + aliases-before`; then hash the
"after" batch against the now-populated decl env.
- `KindInference.inferDeclsFromState` mirrors the split: caller threads
a starting `SolveState` so alias kind UVars from phase 1 are already
registered when `inferDecls` runs (decl ctors can find them), and
phase-3 alias bodies see decl refs from `inferDecls`.
- `Context.doKindInference` orchestrates: `inferAliases (before)` →
`inferDeclsFromState` → `inferAliases (after)` → `kindCheckAnnotations`.
- Drop the parser-level `typeAliasUnsaturatedTest`. Under lazy expansion,
saturation is enforced at kindcheck (an alias has kind
`* -> ... -> *` and a use site at kind `*` is a mismatch). New
transcript `type-aliases-unsaturated.md` covers the kindcheck path.
Bonus: proofs (.github/workflows/proofs/{tests,transcripts}.txt)
refreshed with passing attestations.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Introduces
type aliasdeclarations to Unison.E.g.
A partially-applied type alias is not allowed and results in a helpful error. A type alias has no runtime representation.
Design overview
Storage. A type alias is a kind of namespace entry alongside terms and decls. It has its own reference tag (
RtTypeAlias), its own SQLite object type (TypeAliasComponent), its own on-disk format (U/Codebase/Sqlite/TypeAlias/Format.hs), and its own Share-sync entity (TypeAliasComponentType). The schema bump is additive — migration023-add-type-alias-support.sqljust registers the new object-type row.Hashing. Alias bodies are name-resolved (external refs bound) before hashing. The hash uses outer tag byte
3, putting aliases in a separate hash space from terms (1) and decls (2). Once defined, an alias's canonical hash is fixed.Lazy expansion. Alias refs stay in stored types verbatim. The typechecker doesn't pre-expand them; it dereferences on demand at the head of types in
subtypeandcheckviawhnfAlias. So:f : Endo Natandg : Nat -> Natare distinct definitions with distinct hashes, even when their bodies coincide.Endoorphans every term that references it (same as deleting a data decl).view, slurp diffs, and the PPE all render the alias name as the user wrote it.Kindcheck. Each file-local alias gets a kind UVar registered via
inferAliases, constrained tok_1 -> ... -> k_n -> *from constraints generated against its body. Codebase aliases ride in throughTypeLookup.typeAliases, populated bytypeLookupForDependencieswalking through alias bodies' dependencies.Surface syntax.
type alias <Name> [params] = <type expression>. Ability-row aliases (bodies of the form{IO, Exception, ...}) are supported and spliced into the surrounding row at use sites with set semantics (flatten + dedupe).Out of scope
Test plan
stack exec transcripts -- type-aliases(basic, slurp, view, cross-file — all pass)stack exec transcripts)