polytype
A Hindley-Milner polymorphic typing system.
Implements type inference via unification.
Usage
[dependencies]
polytype = "1.0"
Provided by polytype
are the
Type
enum and
the Context
struct.
The basics:
# #[macro_use] extern crate polytype;
use polytype::{Context, Type};
# fn main() {
let t0 = Type::Variable(0);
let tbool = Type::Constructed("bool", vec![]);
fn tlist(tp: Type) -> Type {
Type::Constructed("list", vec![Box::new(tp)])
}
let t = arrow![
arrow![t0.clone(), tbool],
tlist(t0.clone()),
tlist(t0.clone()),
];
assert!(t.is_polymorphic());
assert_eq!(format!("{}", &t),
"(t0 → bool) → list(t0) → list(t0)");
let mut ctx = Context::default();
let tint = Type::Constructed("int", vec![]);
ctx.unify(&t0, &tint).expect("unifies");
let t = t.apply(&ctx);
assert!(!t.is_polymorphic());
assert_eq!(format!("{}", &t),
"(int → bool) → list(int) → list(int)");
# }
More about instantiation, and unification:
# #[macro_use] extern crate polytype;
use polytype::{Context, Type};
# fn main() {
let t0 = Type::Variable(0);
let t1 = Type::Variable(1);
fn tlist(tp: Type) -> Type {
Type::Constructed("list", vec![Box::new(tp)])
}
let t = arrow![
arrow![
t1.clone(),
t0.clone(),
t1.clone(),
],
t1.clone(),
tlist(t0.clone()),
t1.clone(),
];
assert!(t.is_polymorphic());
assert_eq!(format!("{}", &t),
"(t1 → t0 → t1) → t1 → list(t0) → t1");
let tint = Type::Constructed("int", vec![]);
let tplus = arrow![tint.clone(), tint.clone(), tint.clone()]; assert_eq!(format!("{}", &tplus), "int → int → int");
let mut ctx = Context::default();
let t = t.instantiate_indep(&mut ctx);
let treturn = ctx.new_variable();
ctx.unify(
&t,
&arrow![
tplus.clone(),
tint.clone(),
tlist(tint.clone()),
treturn.clone(),
],
).expect("unifies");
assert_eq!(treturn.apply(&ctx), tint.clone());
let t = t.apply(&ctx);
assert_eq!(format!("{}", t),
"(int → int → int) → int → list(int) → int");
# }