Crate polytype

A Hindley-Milner polymorphic typing system.

For brevity, the documentation heavily uses the two provided macros when creating types.

A TypeScheme is a type that may have universally quantified type variables. A Context keeps track of assignments made to type variables so that you may manipulate Types, which are unquantified and concrete. Hence a TypeScheme can be instantiated, using TypeScheme::instantiate, into a Context in order to produce a corresponding Type. Two Types under a particular Context can be unified using Context::unify, which may record new type variable assignments in the Context.

Examples

The basics:

use polytype::{ptp, tp, Context};

// filter: ∀α. (α → bool) → [α] → [α]
let t = ptp!(0; @arrow[
    tp!(@arrow[tp!(0), tp!(bool)]),
    tp!(list(tp!(0))),
    tp!(list(tp!(0))),
]);

// Quantified type schemes provide polymorphic behavior.
assert_eq!(t.to_string(), "∀t0. (t0 → bool) → list(t0) → list(t0)");

// We can instantiate type schemes to remove quantifiers
let mut ctx = Context::default();
let t = t.instantiate(&mut ctx);
assert_eq!(t.to_string(), "(t0 → bool) → list(t0) → list(t0)");

// We can register a substitution for t0 in the context:
ctx.extend(0, tp!(int));
let t = t.apply(&ctx);
assert_eq!(t.to_string(), "(int → bool) → list(int) → list(int)");

Extended example:

use polytype::{ptp, tp, Context};

// reduce: ∀α. ∀β. (β → α → β) → β → [α] → β
// We can represent the type scheme of reduce using the included macros:
let t = ptp!(0, 1; @arrow[
    tp!(@arrow[tp!(1), tp!(0), tp!(1)]),
    tp!(1),
    tp!(list(tp!(0))),
    tp!(1),
]);
assert_eq!(t.to_string(), "∀t0. ∀t1. (t1 → t0 → t1) → t1 → list(t0) → t1");

// Let's consider reduce when applied to a function that adds two ints

// First, we create a new typing context to manage typing bookkeeping.
let mut ctx = Context::default();

// Let's create a type representing binary addition.
let tplus = tp!(@arrow[tp!(int), tp!(int), tp!(int)]);
assert_eq!(tplus.to_string(), "int → int → int");

// We instantiate the type scheme of reduce within our context
// so new type variables will be distinct
let t = t.instantiate(&mut ctx);
assert_eq!(t.to_string(), "(t1 → t0 → t1) → t1 → list(t0) → t1");

// By unifying, we can ensure function applications obey type requirements.
let treturn = ctx.new_variable();
let targ1 = ctx.new_variable();
let targ2 = ctx.new_variable();
ctx.unify(
    &t,
    &tp!(@arrow[
        tplus.clone(),
        targ1.clone(),
        targ2.clone(),
        treturn.clone(),
    ]),
).expect("unifies");

// We can also now infer what arguments are needed and what gets returned
assert_eq!(targ1.apply(&ctx), tp!(int));             // inferred arg 1: int
assert_eq!(targ2.apply(&ctx), tp!(list(tp!(int))));  // inferred arg 2: list(int)
assert_eq!(treturn.apply(&ctx), tp!(int));           // inferred return: int

// Finally, we can see what form reduce takes by applying the new substitution
let t = t.apply(&ctx);
assert_eq!(t.to_string(), "(int → int → int) → int → list(int) → int");

Macros

ptp

Creates a TypeScheme (convenience for common patterns).

tp

Creates a Type (convenience for common patterns).

Structs

Context

A type environment. Useful for reasoning about Types (e.g unification, type inference).

ContextChange

Allow types to be reified for use in a different context. See Context::merge.

ParseError

Enums

Type

Represents monotypes (fully instantiated, unquantified types).

TypeScheme

Represents polytypes (uninstantiated, universally quantified types).

UnificationError

Errors during unification.

Traits

Infer

An interface for things that are typable.

Name

Types require a Name for comparison.

Type Aliases

Variable

Represents a type variable (an unknown type).