Struct polytype::Context
[−]
[src]
pub struct Context { /* fields omitted */ }
A type environment. Useful for reasoning about Type
s (e.g unification,
type inference).
Contexts track substitutions and generate fresh type variables.
Methods
impl Context
[src]
pub fn substitution(&self) -> &HashMap<Variable, Type>
[src]
The substitution managed by the context.
pub fn extend(&mut self, v: Variable, t: Type)
[src]
Create a new substitution for Type::Variable
number v
to the
Type
t
.
pub fn new_variable(&mut self) -> Type
[src]
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!(format!("{}", t), "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, t2: &Type) -> Result<(), UnificationError>
[src]
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!() }
Trait Implementations
impl Debug for Context
[src]
fn fmt(&self, __arg_0: &mut Formatter) -> Result
[src]
Formats the value using the given formatter. Read more
impl Clone for Context
[src]
fn clone(&self) -> Context
[src]
Returns a copy of the value. Read more
fn clone_from(&mut self, source: &Self)
1.0.0[src]
Performs copy-assignment from source
. Read more