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
//! # type_lang
//!
//! The type-system substrate of a compiler front-end: a representation for types,
//! a [`Unifier`] that makes two types equal and records what that requires, and a
//! structured [`TypeError`] for when they cannot be made equal.
//!
//! It owns the soundness-critical core — type terms, inference variables, and
//! first-order unification — and nothing else. A language's own type rules (its
//! primitives, its subtyping, its coercions) layer on top by choosing what each
//! constructor means; this crate stores and compares those constructors but never
//! interprets them. It does no parsing and renders no diagnostics: it assigns types
//! to a syntax tree the caller walks, and a [`TypeError`] maps cleanly onto a
//! rendered diagnostic in the caller's own type names.
//!
//! ## The model
//!
//! A [`Type`] is one of two shapes: an inference [`TyVar`], or a [`TyCon`] applied
//! to zero or more argument types. Those two shapes describe every first-order
//! type — `int` is a constructor with no arguments, `List<int>` is `List` applied
//! to `int`, and `(int) -> bool` is a function constructor applied to `int` and
//! `bool`. Constructors are opaque tags the consumer assigns; equal tags are the
//! same type former.
//!
//! A [`Unifier`] holds the inference variables and the substitution over them. It
//! [`fresh`](Unifier::fresh)ens variables, [`unify`](Unifier::unify)es two types —
//! binding variables so the two become equal, or failing with a [`TypeError`] — and
//! [`resolve`](Unifier::resolve)s a type back to its most concrete known form. The
//! algorithm is textbook first-order unification: constructors match only on equal
//! head and arity, a variable binds to any type guarded by an occurs check, and the
//! result is a most-general unifier.
//!
//! ## Quickstart
//!
//! ```
//! use type_lang::{TyCon, Type, Unifier};
//!
//! // The consumer assigns meaning to constructor tags.
//! const FUNCTION: TyCon = TyCon::new(0);
//! const INT: TyCon = TyCon::new(1);
//! const BOOL: TyCon = TyCon::new(2);
//!
//! let mut unifier = Unifier::new();
//! let arg = unifier.fresh();
//! let ret = unifier.fresh();
//!
//! // We have inferred a call site needs a function (?arg) -> ?ret,
//! // and the callee is known to be (int) -> bool.
//! let needed = Type::app(FUNCTION, [Type::var(arg), Type::var(ret)]);
//! let callee = Type::app(FUNCTION, [Type::con(INT), Type::con(BOOL)]);
//! unifier.unify(&needed, &callee)?;
//!
//! // Unification has discovered the argument and result types.
//! assert_eq!(unifier.resolve(&Type::var(arg)), Type::con(INT));
//! assert_eq!(unifier.resolve(&Type::var(ret)), Type::con(BOOL));
//! # Ok::<(), type_lang::TypeError>(())
//! ```
//!
//! ## Stability
//!
//! As of `1.0` the public surface is **stable** and follows Semantic Versioning: no
//! breaking changes before `2.0`. [`TypeError`] is `#[non_exhaustive]`, so a new
//! failure mode is an additive, minor change, and the MSRV (Rust 1.85) only rises in
//! a minor release. The full promise is in
//! [`docs/API.md`](https://github.com/jamesgober/type-lang/blob/main/docs/API.md#stability).
extern crate alloc;
pub use TypeError;
pub use ;
pub use Unifier;