type-lang 1.0.0

Highlights

• First-order unification with an occurs check, so a variable can never be bound to a type that contains itself. The substitution produced is a most-general unifier.
• Language-agnostic type representation: constructors are opaque tags the consumer assigns meaning to, so the same core expresses primitives, generics, functions, and tuples.
• Iterative core — unification and the occurs check use explicit work stacks, so a deeply nested type cannot overflow the call stack.
• no_std-friendly (needs only alloc), with optional serde for serialising type terms and inference state.
• No panics in shipping code; every failure is a defined TypeError. #![forbid(unsafe_code)].

Installation

[dependencies]
type-lang = "1.0"

Usage

A consumer assigns meaning to constructor tags, then unifies the types it builds. Unification discovers what the inference variables must be:

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

// The consumer's constructor table — the tags are arbitrary but stable.
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();

// A call site needs a function (?arg) -> ?ret; the callee is (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).expect("same constructor and arity");

// Unification solved both variables.
assert_eq!(unifier.resolve(&Type::var(arg)), Type::con(INT));
assert_eq!(unifier.resolve(&Type::var(ret)), Type::con(BOOL));

Failures are values, not panics — a mismatch carries the clashing types, and a self-referential type is rejected by the occurs check:

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

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

let mut unifier = Unifier::new();

// Different constructors do not unify.
let err = unifier.unify(&Type::con(INT), &Type::con(LIST)).unwrap_err();
assert!(matches!(err, TypeError::Mismatch { .. }));

// ?v = List<?v> would be an infinite type.
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 { .. }));

See docs/API.md for the full reference.

Feature flags

Contributing

See dev/DIRECTIVES.md for engineering standards and the definition of done. Before a PR: cargo fmt --all, cargo clippy --all-targets --all-features -- -D warnings, and cargo test --all-features must be clean.