Crate polytype [−] [src]
A Hindley-Milner polymorphic typing system.
For brevity, the documentation heavily uses the three 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 Type
s, 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 Type
s
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::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!(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 register a substiution for t0 in the context: ctx.extend(0, tp!(int)); 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: let t = ptp!(0, 1; @arrow[ tp!(@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, 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!(format!("{}", &tplus), "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!(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, &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!(format!("{}", &t), "(int → int → int) → int → list(int) → int");
Macros
ptp |
Creates a |
tp |
Creates a |
Structs
Context |
A type environment. Useful for reasoning about |
Enums
Type |
Represents monotypes (fully instantiated, unquantified types). |
TypeSchema |
Represents polytypes (uninstantiated, universally quantified types). |
UnificationError |
Errors during unification. |
Type Definitions
Variable |
Represents a type variable (an unknown type). |