type_lang/lib.rs
1//! # type_lang
2//!
3//! The type-system substrate of a compiler front-end: a representation for types,
4//! a [`Unifier`] that makes two types equal and records what that requires, and a
5//! structured [`TypeError`] for when they cannot be made equal.
6//!
7//! It owns the soundness-critical core — type terms, inference variables, and
8//! first-order unification — and nothing else. A language's own type rules (its
9//! primitives, its subtyping, its coercions) layer on top by choosing what each
10//! constructor means; this crate stores and compares those constructors but never
11//! interprets them. It does no parsing and renders no diagnostics: it assigns types
12//! to a syntax tree the caller walks, and a [`TypeError`] maps cleanly onto a
13//! rendered diagnostic in the caller's own type names.
14//!
15//! ## The model
16//!
17//! A [`Type`] is one of two shapes: an inference [`TyVar`], or a [`TyCon`] applied
18//! to zero or more argument types. Those two shapes describe every first-order
19//! type — `int` is a constructor with no arguments, `List<int>` is `List` applied
20//! to `int`, and `(int) -> bool` is a function constructor applied to `int` and
21//! `bool`. Constructors are opaque tags the consumer assigns; equal tags are the
22//! same type former.
23//!
24//! A [`Unifier`] holds the inference variables and the substitution over them. It
25//! [`fresh`](Unifier::fresh)ens variables, [`unify`](Unifier::unify)es two types —
26//! binding variables so the two become equal, or failing with a [`TypeError`] — and
27//! [`resolve`](Unifier::resolve)s a type back to its most concrete known form. The
28//! algorithm is textbook first-order unification: constructors match only on equal
29//! head and arity, a variable binds to any type guarded by an occurs check, and the
30//! result is a most-general unifier.
31//!
32//! ## Quickstart
33//!
34//! ```
35//! use type_lang::{TyCon, Type, Unifier};
36//!
37//! // The consumer assigns meaning to constructor tags.
38//! const FUNCTION: TyCon = TyCon::new(0);
39//! const INT: TyCon = TyCon::new(1);
40//! const BOOL: TyCon = TyCon::new(2);
41//!
42//! let mut unifier = Unifier::new();
43//! let arg = unifier.fresh();
44//! let ret = unifier.fresh();
45//!
46//! // We have inferred a call site needs a function (?arg) -> ?ret,
47//! // and the callee is known to be (int) -> bool.
48//! let needed = Type::app(FUNCTION, [Type::var(arg), Type::var(ret)]);
49//! let callee = Type::app(FUNCTION, [Type::con(INT), Type::con(BOOL)]);
50//! unifier.unify(&needed, &callee)?;
51//!
52//! // Unification has discovered the argument and result types.
53//! assert_eq!(unifier.resolve(&Type::var(arg)), Type::con(INT));
54//! assert_eq!(unifier.resolve(&Type::var(ret)), Type::con(BOOL));
55//! # Ok::<(), type_lang::TypeError>(())
56//! ```
57//!
58//! ## Stability
59//!
60//! As of `1.0` the public surface is **stable** and follows Semantic Versioning: no
61//! breaking changes before `2.0`. [`TypeError`] is `#[non_exhaustive]`, so a new
62//! failure mode is an additive, minor change, and the MSRV (Rust 1.85) only rises in
63//! a minor release. The full promise is in
64//! [`docs/API.md`](https://github.com/jamesgober/type-lang/blob/main/docs/API.md#stability).
65
66#![cfg_attr(not(feature = "std"), no_std)]
67#![cfg_attr(docsrs, feature(doc_cfg))]
68#![deny(missing_docs)]
69#![forbid(unsafe_code)]
70
71extern crate alloc;
72
73mod error;
74mod ty;
75mod unify;
76
77pub use error::TypeError;
78pub use ty::{TyCon, TyVar, Type};
79pub use unify::Unifier;