Struct polytype::Context [−][src]
Expand description
A type environment. Useful for reasoning about Type
s (e.g unification,
type inference).
Contexts track substitutions and generate fresh type variables.
Implementations
The substitution managed by the context.
Clears the substitution managed by the context.
Examples
let mut ctx = Context::default();
// Get a fresh variable
let t0 = ctx.new_variable();
let t1 = ctx.new_variable();
let clean = ctx.clone();
if let Type::Variable(N) = t0 {
ctx.extend(N, tp![t1]);
let dirty = ctx.clone();
ctx.clean();
assert_eq!(clean, ctx);
assert_ne!(clean, dirty);
}
Removes previous substitutions added to the Context
until there are only n
remaining.
Create a new substitution for Type::Variable
number v
to the
Type
t
.
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));
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!() }
Like unify
, but may affect the context even under failure. Hence, use this if you
discard the context upon failure.
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));
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
Auto Trait Implementations
impl<N = &'static str> !RefUnwindSafe for Context<N>
impl<N> UnwindSafe for Context<N> where
N: UnwindSafe,
Blanket Implementations
Mutably borrows from an owned value. Read more
Compare self to key
and return true
if they are equal.