Struct polytype::Context

pub struct Context<N: Name = &'static str> { /* fields omitted */ }

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

Contexts track substitutions and generate fresh type variables.

Methods

impl<N: Name> Context<N>

pub fn substitution(&self) -> &HashMap<Variable, Type<N>>

The substitution managed by the context.

pub fn extend(&mut self, v: Variable, t: Type<N>)

Create a new substitution for Type::Variable number v to the Type t.

pub fn new_variable(&mut self) -> Type<N>

Create a new Type::Variable from the next unused number.

Examples

let mut ctx = Context::default();

// Get a fresh variable
let t0 = ctx.new_variable();
assert_eq!(t0, Type::Variable(0));

// Instantiating a polytype will yield new variables
let t = ptp!(0, 1; @arrow[tp!(0), tp!(1), tp!(1)]);
let t = t.instantiate(&mut ctx);
assert_eq!(t.to_string(), "t1 → t2 → t2");

// Get another fresh variable
let t3 = ctx.new_variable();
assert_eq!(t3, Type::Variable(3));

pub fn unify(     &mut self,     t1: &Type<N>,     t2: &Type<N> ) -> Result<(), UnificationError<N>>

Create constraints within the context that ensure t1 and t2 unify.

Examples

let mut ctx = Context::default();

let t1 = tp!(@arrow[tp!(int), tp!(0)]);
let t2 = tp!(@arrow[tp!(1), tp!(bool)]);
ctx.unify(&t1, &t2).expect("unifies");

let t1 = t1.apply(&ctx);
let t2 = t2.apply(&ctx);
assert_eq!(t1, t2);  // int → bool

Unification errors leave the context unaffected. A UnificationError::Failure error happens when symbols don't match:

let mut ctx = Context::default();

let t1 = tp!(@arrow[tp!(int), tp!(0)]);
let t2 = tp!(@arrow[tp!(bool), tp!(1)]);
let res = ctx.unify(&t1, &t2);

if let Err(UnificationError::Failure(left, right)) = res {
    // failed to unify t1 with t2.
    assert_eq!(left, tp!(int));
    assert_eq!(right, tp!(bool));
} else { unreachable!() }

An UnificationError::Occurs error happens when the same type variable occurs in both types in a circular way. Ensure you instantiate your types properly, so type variables don't overlap unless you mean them to.

let mut ctx = Context::default();

let t1 = tp!(1);
let t2 = tp!(@arrow[tp!(bool), tp!(1)]);
let res = ctx.unify(&t1, &t2);

if let Err(UnificationError::Occurs(v)) = res {
    // failed to unify t1 with t2 because of circular type variable occurrence.
    // t1 would have to be bool -> bool -> ... ad infinitum.
    assert_eq!(v, 1);
} else { unreachable!() }

pub fn unify_fast(     &mut self,     t1: Type<N>,     t2: Type<N> ) -> Result<(), UnificationError<N>>

Like unify, but may affect the context even under failure. Hence, use this if you discard the context upon failure.

pub fn merge(&mut self, other: Context<N>) -> ContextChange

Merge two type contexts. Every Type that corresponds to the other context must be reified using ContextChange::reify.

Examples

let mut ctx = Context::default();
let a = ctx.new_variable();
let b = ctx.new_variable();
ctx.unify(&Type::arrow(a, b), &tp!(@arrow[tp!(int), tp!(bool)])).unwrap();
// ctx uses t0 and t1

let mut ctx2 = Context::default();
let pt = ptp!(0, 1; @arrow[tp!(0), tp!(1)]);
let mut t = pt.instantiate(&mut ctx2);
ctx2.extend(0, tp!(bool));
assert_eq!(t.apply(&ctx2).to_string(), "bool → t1");
// ctx2 uses t0 and t1

let ctx_change = ctx.merge(ctx2);
// rewrite all terms under ctx2 using ctx_change
ctx_change.reify(&mut t);
assert_eq!(t.to_string(), "t2 → t3");
assert_eq!(t.apply(&ctx).to_string(), "bool → t3");

assert_eq!(ctx.new_variable(), tp!(4));

Trait Implementations

impl<N: Debug + Name> Debug for Context<N>

fn fmt(&self, f: &mut Formatter) -> Result

Formats the value using the given formatter.

impl<N: Clone + Name> Clone for Context<N>

fn clone(&self) -> Context<N>

Returns a copy of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl<N: Name> Default for Context<N>

fn default() -> Self

Returns the "default value" for a type.