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 confine(&mut self, keep: &[Variable])

Confines the substitution to those which act on the given variables.

Examples

let mut ctx = Context::default();
let v0 = ctx.new_variable();
let v1 = ctx.new_variable();
ctx.unify(&v0, &tp!(int));
ctx.unify(&v1, &tp!(bool));

{
    let sub = ctx.substitution();
    assert_eq!(sub.len(), 2);
    assert_eq!(sub[&0], tp!(int));
    assert_eq!(sub[&1], tp!(bool));
}

// confine the substitution to v1
ctx.confine(&[1]);
let sub = ctx.substitution();
assert_eq!(sub.len(), 1);
assert_eq!(sub[&1], tp!(bool));

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

Merge two type contexts.

Every Type (TypeSchema) that corresponds to the other context must be reified using ContextChange::reify_type (ContextChange::reify_typeschema). Any Variable in sacreds will not be changed by the context (i.e. reification will ignore it).

Examples

Without sacred variables, which assumes that all type variables between the contexts are distinct:

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, vec![]);
// rewrite all terms under ctx2 using ctx_change
ctx_change.reify_type(&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));

With sacred variables, which specifies which type variables are equivalent in both contexts:

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 a = ctx2.new_variable();
let b = ctx2.new_variable();
let mut t = Type::arrow(a, b);
ctx2.extend(0, tp!(bool));
assert_eq!(t.apply(&ctx2).to_string(), "bool → t1");
// ctx2 uses t0 and t1

// t1 from ctx2 is preserved *and* constrained by ctx
let ctx_change = ctx.merge(ctx2, vec![1]);
// rewrite all terms under ctx2 using ctx_change
ctx_change.reify_type(&mut t);
assert_eq!(t.to_string(), "t2 → t1");
assert_eq!(t.apply(&ctx).to_string(), "bool → bool");

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

Trait Implementations

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

fn eq(&self, other: &Context<N>) -> bool

This method tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Context<N>) -> bool

This method tests for !=.

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

fn default() -> Self

Returns the "default value" for a type.

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: Eq + Name> Eq for Context<N>

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

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

Formats the value using the given formatter.