type-lang 1.0.0

Type representation, unification, and inference scaffolding.
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178

# type-lang v0.2.0 — The unification core

**The core the scaffold was built for.** v0.2.0 implements the soundness-critical
layer: a representation for types, inference variables, and first-order unification
with an occurs check. A type checker is written against exactly this — make two
types equal, find out what that forces the unknowns to be, or learn precisely why
they cannot be made equal. Everything a particular language adds on top (its
primitives, its subtyping, its coercions) is expressed in terms of this core, which
stores and compares type constructors but never interprets them.

## What is type-lang?

The type-system substrate of a compiler front-end. It owns the type representation
and the unification/substitution machinery, and nothing else — it does no parsing
and renders no diagnostics. It assigns types to a syntax tree the caller walks, and
its structured errors map cleanly onto a rendered diagnostic in the caller's own
type names. It is one of the semantic crates of the `-lang` language-construction
family.

## What's new in 0.2.0

### `Type` — the type term

A type is one of two shapes: an inference variable, or a constructor applied to
zero or more argument types. Those two shapes describe every first-order type — a
primitive is a constructor with no arguments, `List<int>` is `List` applied to
`int`, and a function is a constructor applied to its parameter and result types.

```rust
use type_lang::{TyCon, Type};

const FUNCTION: TyCon = TyCon::new(0);
const INT: TyCon = TyCon::new(1);
const BOOL: TyCon = TyCon::new(2);

// (int) -> bool
let signature = Type::app(FUNCTION, [Type::con(INT), Type::con(BOOL)]);
assert_eq!(signature.head(), Some(FUNCTION));
assert_eq!(signature.args().len(), 2);
```

Constructors (`TyCon`) are opaque numeric tags the consumer assigns and keeps
stable, so the same core serves any language. Variables (`TyVar`) are opaque handles
minted by the unifier; there is no public constructor, so a variable can only come
from the unifier that can resolve it.

### `Unifier` — variables, substitution, and unification

The `Unifier` mints fresh variables, makes two types equal — recording the variable
bindings that requires — and resolves a type back to its most concrete known form.

```rust
use type_lang::{TyCon, Type, Unifier};

const FUNCTION: TyCon = TyCon::new(0);
const INT: TyCon = TyCon::new(1);

let mut unifier = Unifier::new();
let arg = unifier.fresh();
let ret = unifier.fresh();

// Unify the inferred (?arg) -> ?ret against the known (int) -> int.
let inferred = Type::app(FUNCTION, [Type::var(arg), Type::var(ret)]);
let known = Type::app(FUNCTION, [Type::con(INT), Type::con(INT)]);
unifier.unify(&inferred, &known).expect("same constructor and arity");

assert_eq!(unifier.resolve(&Type::var(arg)), Type::con(INT));
assert_eq!(unifier.resolve(&Type::var(ret)), Type::con(INT));
```

Unification is the textbook first-order algorithm: two constructors match only on
equal head and arity, and their arguments are then unified pairwise; a variable
unifies with any type by being bound to it, guarded by an occurs check so a variable
can never be bound to a type that contains it. The substitution produced is a
most-general unifier. The implementation is iterative — unification and the occurs
check use explicit work stacks rather than recursion — so an arbitrarily deep type
cannot overflow the call stack.

`unify` is not transactional: a call that binds a variable and then hits a conflict
keeps the binding it already made. To try a unification without committing, clone
the unifier first and keep the clone only on success.

### `TypeError` — defined failures, not panics

Unification fails in exactly two ways, each carrying the offending types resolved
under the substitution at the point of failure:

```rust
use type_lang::{TyCon, Type, TypeError, Unifier};

const INT: TyCon = TyCon::new(0);
const LIST: TyCon = TyCon::new(1);

let mut unifier = Unifier::new();

// A constructor clash.
let err = unifier.unify(&Type::con(INT), &Type::con(LIST)).unwrap_err();
assert!(matches!(err, TypeError::Mismatch { .. }));

// An infinite type, caught by the occurs check.
let v = unifier.fresh();
let recursive = Type::app(LIST, [Type::var(v)]);
let err = unifier.unify(&Type::var(v), &recursive).unwrap_err();
assert!(matches!(err, TypeError::Occurs { .. }));
```

`TypeError` is `#[non_exhaustive]`, so a future failure mode is an additive change.

### `serde`, property tests, and benchmarks

Behind the `serde` feature, `Type`, `TyVar`, `TyCon`, and the whole `Unifier`
serialise, so a type term or an entire inference state round-trips through any serde
format. The unification invariants from `dev/DIRECTIVES.md` — soundness, symmetry,
idempotent resolution, reflexivity, and the occurs check — are covered by `proptest`
over randomly generated type terms, and `criterion` benchmarks track variable
minting, unification, and resolution as the terms grow.

## Dependencies: ast, symbol, diag

The roadmap slated `ast-lang`, `symbol-lang`, and `diag-lang` to be wired at this
stage "when first used." They are **not** wired in v0.2.0, and the deferral is
recorded in `dev/ROADMAP.md` with its reason: the unification core is self-contained
and uses none of them. Wiring an unused dependency would violate the project's
dependency policy. Integration with a syntax tree, a symbol table, and a diagnostic
renderer is the consumer's to make — `TypeError` is designed to map onto a
`diag-lang` diagnostic — and these crates will be wired only if and when a
consumer-facing pass inside type-lang needs them.

## Breaking changes

**None against published code.** This is the first release with a public surface;
v0.1.0 had none. The surface is documented in full in `docs/API.md` and settles
across the rest of the 0.x series before it is frozen at `1.0`.

## Verification

```bash
cargo fmt --all -- --check
cargo clippy --all-targets -- -D warnings
cargo clippy --all-targets --all-features -- -D warnings
cargo test
cargo test --all-features
RUSTDOCFLAGS="-D warnings" cargo doc --no-deps --all-features
cargo +1.85 build --all-features
cargo audit
cargo deny check
```

All green on Linux (WSL2 Ubuntu) and Windows x86_64, Rust stable 1.95 and MSRV 1.85.
Counts at this tag: 29 unit and integration tests plus 19 doctests on default
features; 32 plus 19 with `--all-features` (the serde round-trips). The `criterion`
suite shows unification scaling with term size as expected.

## What's next

- **1.0.0 — API freeze.** Settle and freeze the public surface, mark `docs/API.md`
  stable with a recorded SemVer promise, and run the full property-test and
  benchmark suite green across all three platforms.

## Installation

```toml
[dependencies]
type-lang = "0.2"
```

MSRV: Rust 1.85.

## Documentation

- [README](https://github.com/jamesgober/type-lang/blob/main/README.md)
- [API Reference](https://github.com/jamesgober/type-lang/blob/main/docs/API.md)
- [CHANGELOG](https://github.com/jamesgober/type-lang/blob/main/CHANGELOG.md)

---

**Full diff:** [`v0.1.0...v0.2.0`](https://github.com/jamesgober/type-lang/compare/v0.1.0...v0.2.0).
**Changelog:** [`CHANGELOG.md`](https://github.com/jamesgober/type-lang/blob/main/CHANGELOG.md#020---2026-06-29).