Crate polytype

A Hindley-Milner polymorphic typing system.

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

Examples

The basics:

use polytype::Context;

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

// Quantified type schemas provide polymorphic behavior.
assert_eq!(format!("{}", &t), "∀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!(format!("{}", &t), "(t0 → bool) → list(t0) → list(t0)");

// We can substitute for t0 using unification in a type Context:
ctx.unify(&tp!(0), &tp!(int)).expect("unifies");
let t = t.apply(&ctx);
assert_eq!(format!("{}", &t), "(int → bool) → list(int) → list(int)");

Extended example:

use polytype::Context;

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

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

// First, let's create a type representing binary addition.
let tplus = arrow![tp!(int), tp!(int), tp!(int)];
assert_eq!(format!("{}", &tplus), "int → int → int");

// Let's also create a new typing context to manage typing bookkeeping.
let mut ctx = Context::default();

// Then, let's instantiate the type schema of reduce within our context
// so new type variables will be distinct
let t = t.instantiate(&mut ctx);
assert_eq!(format!("{}", &t), "(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,
    &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: int
assert_eq!(treturn.apply(&ctx), tp!(int));           // inferred return: int

// Finally, we can see what form reduce takes
let t = t.apply(&ctx);
assert_eq!(format!("{}", &t), "(int → int → int) → int → list(int) → int");

Macros

arrow	Creates an arrow of tp0 → tp1 → ... (convenience for nested arrows).
ptp	Creates a TypeSchema::Polytype or TypeSchema::Monotype (convenience for common pattern).
tp	Creates a Type::Constructed or Type::Variable (convenience for common pattern).

Structs

Context

Represents a type environment. Useful for reasoning about types (e.g unification, type inference).

Enums

Type	Represents monotypes (fully instantiated, unquantified types).
TypeSchema	Represents polytypes (uninstantiated, universally quantified types).
UnificationError	Represents errors in unification.

Type Definitions

Variable

Represents a type variable (an unknown type).