Struct polytype::Context [] [src]

pub struct Context { /* fields omitted */ }

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

Methods

impl Context
[src]

[src]

[src]

Create a new substitution for the type variable numbered v to the type t.

[src]

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

[src]

Create constraints within the context that ensure the two types unify.

Examples

let mut ctx = Context::default();

let t1 = arrow![tp!(int), tp!(0)];
let t2 = 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);

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

let mut ctx = Context::default();

let t1 = arrow![tp!(int), tp!(0)];
let t2 = 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 (or instantiate_indep) 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 = 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!() }

Trait Implementations

impl Debug for Context
[src]

[src]

Formats the value using the given formatter.

impl Clone for Context
[src]

[src]

Returns a copy of the value. Read more

1.0.0
[src]

Performs copy-assignment from source. Read more

impl Default for Context
[src]

[src]

Returns the "default value" for a type. Read more