Crate polytype

A Hindley-Milner polymorphic typing system.

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

A TypeSchema 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 TypeSchema can be instantiated, using TypeSchema::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 schemas provide polymorphic behavior.
assert_eq!(t.to_string(), "∀t0. (t0 → bool) → list(t0) → list(t0)");

// We can instantiate type schemas 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 schema 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 schema 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 TypeSchema (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.

Enums

Type	Represents monotypes (fully instantiated, unquantified types).
TypeSchema	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 Definitions

Variable

Represents a type variable (an unknown type).