Crate polytype

A Hindley-Milner polymorphic typing system.

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

Examples

The basics:

use polytype::Context;

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

assert!(t.is_polymorphic());
assert_eq!(format!("{}", &t), "(t0 → bool) → list(t0) → list(t0)");

// we can substitute t0 with unification in a type context:
let mut ctx = Context::default();
ctx.unify(&tp!(0), &tp!(int)).expect("unifies");

let t = t.apply(&ctx);
assert!(!t.is_polymorphic());
assert_eq!(format!("{}", &t), "(int → bool) → list(int) → list(int)");

More about instantiation, and unification:

use polytype::Context;

// reduce: (β → α → β) → β → [α] → β
let t = arrow![
    arrow![tp!(1), tp!(0), tp!(1)],
    tp!(1),
    tp!(list(tp!(0))),
    tp!(1),
];

assert!(t.is_polymorphic());
assert_eq!(format!("{}", &t), "(t1 → t0 → t1) → t1 → list(t0) → t1");

// lets consider reduce when applied to a function that adds two ints
let tplus = arrow![tp!(int), tp!(int), tp!(int)];
assert_eq!(format!("{}", &tplus), "int → int → int");

// instantiate polymorphic types within our context so new type variables will be distinct
let mut ctx = Context::default();
let t = t.instantiate_indep(&mut ctx);

// by unifying, we can ensure valid function application and infer what gets returned
let treturn = ctx.new_variable();
ctx.unify(
    &t,
    &arrow![
        tplus.clone(),
        tp!(int),
        tp!(list(tp!(int))),
        treturn.clone(),
    ],
).expect("unifies");
assert_eq!(treturn.apply(&ctx), tp!(int));  // inferred return: int

// now that unification has happened with ctx, 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 a Type::Arrow of tp0 → tp1 → ... (convenience for nested arrows).
tp	Creates a Type::Constructed or Type::Variable (convenience for common pattern).

Structs

Arrow	A curried function.
Context	Context is a type environment, keeping track of substitutions and type variables. Useful for unifying (and inferring) types.

Enums

Type	Represents a type in the Hindley-Milner polymorphic typing system.
UnificationError