From d6426866d0818f3a6e96b18b7ad18df64d0fc95a Mon Sep 17 00:00:00 2001 From: Josh Rule Date: Fri, 2 Jul 2021 06:39:30 -0700 Subject: [PATCH 1/3] enhancement: rewrite polytype to use interning --- Cargo.toml | 3 + src/context.rs | 701 ++++++++++++++++----------------- src/lib.rs | 343 +++++++++------- src/macros.rs | 260 ++++++------ src/parser.rs | 130 ++---- src/source.rs | 174 ++++++++ src/substitution.rs | 274 +++++++++++++ src/types.rs | 939 ++++++++++++++++++++++++-------------------- 8 files changed, 1667 insertions(+), 1157 deletions(-) create mode 100644 src/source.rs create mode 100644 src/substitution.rs diff --git a/Cargo.toml b/Cargo.toml index 12a56a7..2108a1c 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -17,8 +17,11 @@ default = ["parser"] parser = ["nom"] [dependencies] +fnv = "1.0" indexmap = "1.0" itertools = "0.8" +smallvec = "1.4" +typed-arena = "2.0" [dependencies.nom] version = "=4.1.1" diff --git a/src/context.rs b/src/context.rs index 937b916..ebf3691 100644 --- a/src/context.rs +++ b/src/context.rs @@ -1,439 +1,412 @@ -use crate::{Name, Type, TypeSchema, Variable}; -use indexmap::IndexMap; -use std::{cell::RefCell, collections::HashMap, error, fmt}; +use crate::{Name, Schema, Ty, Type, TypeSchema, Variable}; +use fnv::FnvHashMap; +use itertools::Itertools; +use std::{ + borrow::Borrow, + cell::RefCell, + hash::{Hash, Hasher}, +}; +use typed_arena::Arena; -/// Errors during unification. -#[derive(Debug, Clone, PartialEq)] -pub enum UnificationError { - /// `Occurs` happens when occurs checks fail (i.e. a type variable is - /// unified recursively). The id of the bad type variable is supplied. - Occurs(Variable), - /// `Failure` happens when symbols or type variants don't unify because of - /// structural differences. - Failure(Type, Type), +struct Interner<'a, K>(RefCell>); + +struct SliceInterner<'a, K>(RefCell>); + +impl<'a, K: Eq + Hash> Interner<'a, K> { + fn with_capacity(n: usize) -> Self { + Interner(RefCell::new(FnvHashMap::with_capacity_and_hasher( + n, + Default::default(), + ))) + } + pub fn intern(&self, value: K, make: impl FnOnce(K) -> &'a K) -> &'a K + where + K: Borrow, + Q: Hash + Eq, + { + let mut table = self.0.borrow_mut(); + // TODO: might not be super-efficient + if let Some((k, _)) = table.get_key_value(&value) { + &k + } else { + let k = make(value); + table.insert(k, ()); + k + } + } +} + +impl<'a, K> Default for Interner<'a, K> { + fn default() -> Self { + Interner(RefCell::new(FnvHashMap::default())) + } } -impl fmt::Display for UnificationError { - fn fmt(&self, f: &mut fmt::Formatter<'_>) -> Result<(), fmt::Error> { - match *self { - UnificationError::Occurs(v) => write!(f, "Occurs({})", v), - UnificationError::Failure(ref t1, ref t2) => { - write!(f, "Failure({}, {})", t1.show(false), t2.show(false)) - } + +impl<'a, K: Eq + Hash> SliceInterner<'a, K> { + pub fn with_capacity(n: usize) -> Self { + SliceInterner(RefCell::new(FnvHashMap::with_capacity_and_hasher( + n, + Default::default(), + ))) + } + pub fn intern(&self, value: &[K], make: impl FnOnce(&[K]) -> &'a [K]) -> &'a [K] { + let mut table = self.0.borrow_mut(); + // TODO: might not be super-efficient + let opt: Option<(&&'a [K], _)> = table.get_key_value(value); + if let Some((k, _)) = opt { + *k + } else { + let k = make(value); + table.insert(k, ()); + k } } } -impl error::Error for UnificationError { - fn description(&self) -> &'static str { - "unification failed" + +impl<'a, K> Default for SliceInterner<'a, K> { + fn default() -> Self { + SliceInterner(RefCell::new(FnvHashMap::default())) } } -/// A type environment. Useful for reasoning about [`Type`]s (e.g unification, -/// type inference). +#[derive(Copy)] +/// The universe within which a [`Variable`], [`Type`], or [`TypeSchema`] +/// exists. /// -/// Contexts track substitutions and generate fresh type variables. +/// A `TypeContext` interns these values for more efficient reasoning. That is, +/// it stores owned copies of [`Type`]s and [`TypeSchema`]s. Whenever +/// requested, it returns a reference to these values in the form of a [`Ty`] or +/// [`Schema`]. These reference types are the primary way end-users interact +/// with types. /// +/// [`Variable`]: struct.Variable.html /// [`Type`]: enum.Type.html -#[derive(Debug, Clone, PartialEq, Eq)] -pub struct Context { - /// A set of constraints mapping from [`Variable`]s to [`Type`]s. - /// - /// [`Type`]: enum.Type.html - /// [`Variable`]: type.Variable.html - pub(crate) substitution: IndexMap>, - /// Some operations on [`Type`]s, notably [`apply`] and [`apply_mut`] - /// perform path compression as they operate. Path compression is a - /// technique commonly used in [Union-Find data structures]. We apply it - /// here so that whenever a chain of substitutions is traversed, each - /// variable is updated to point to its ultimate value. For example, the - /// chain: - /// - /// `t0 ↦ t1`, `t1 ↦ t2`, and `t2 ↦ int` - /// - /// becomes - /// - /// `t0 ↦ int`, `t1 ↦ int`, and `t2 ↦ int` - /// - /// Rather than updating the actual mappings, `Context` maintains this cache - /// of compressed mappings. - /// - /// [Union-Find data structure]: https://en.wikipedia.org/wiki/Disjoint-set_data_structure - /// [`Type`]: enum.Type.html - /// [`apply`]: enum.Type.html#method.apply - /// [`apply_mut`]: enum.Type.html#method.apply_mut - pub(crate) path_compression_cache: RefCell>>, - /// A counter used to generate fresh [`Variable`]s - /// - /// [`Variable`]: type.Variable.html - next: Variable, +/// [`TypeSchema`]: enum.TypeSchema.html +/// [`Ty`]: type.Ty.html +/// [`Schema`]: type.Schema.html +pub struct TypeContext<'ctx, N: Name = &'static str> { + ctx: &'ctx Context<'ctx, N>, } -impl Default for Context { - fn default() -> Self { - Context { - substitution: IndexMap::new(), - path_compression_cache: RefCell::new(HashMap::new()), - next: 0, - } + +impl<'ctx, N: Name> PartialEq for TypeContext<'ctx, N> { + fn eq(&self, other: &Self) -> bool { + std::ptr::eq(self.ctx, other.ctx) } } -impl Context { - /// The substitution managed by the context. - pub fn substitution(&self) -> &IndexMap> { - &self.substitution + +impl<'ctx, N: Name> std::fmt::Debug for TypeContext<'ctx, N> { + fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result { + write!(f, "TypeContext<'ctx, N> {{ ctx: {:p} }}", self.ctx) } - /// The number of constraints in the substitution. - pub fn len(&self) -> usize { - self.substitution.len() +} + +impl<'ctx, N: Name> Eq for TypeContext<'ctx, N> {} + +impl<'ctx, N: Name> Clone for TypeContext<'ctx, N> { + fn clone(&self) -> Self { + TypeContext { ctx: self.ctx } } - /// `true` if the substitution has any constraints, else `false`. - pub fn is_empty(&self) -> bool { - self.substitution.is_empty() +} + +impl<'ctx, N: Name> Hash for TypeContext<'ctx, N> { + fn hash(&self, state: &mut H) { + (self.ctx as *const Context<'ctx, N>).hash(state) } - /// Clears the substitution managed by the context. +} + +/// The inner type managed by a [`TypeContext`]. A `Context` is not manipulated directly. +/// +/// [`TypeContext`]: struct.TypeContext.html +pub struct Context<'ctx, N: Name = &'static str> { + schema_arena: &'ctx Arena>, + schema_map: Interner<'ctx, TypeSchema<'ctx, N>>, + type_arena: &'ctx Arena>, + type_map: Interner<'ctx, Type<'ctx, N>>, + name_arena: &'ctx Arena, + name_map: Interner<'ctx, N>, + arg_arena: &'ctx Arena>, + arg_map: SliceInterner<'ctx, Ty<'ctx, N>>, +} + +/// This is the most straightforward way to gain access to a [`TypeContext`]. +/// +/// `with_ctx` creates a [`TypeContext`], `ctx`, with `n` slots pre-allocated in +/// each arena, calls `f(ctx)`, and returns the result. +/// +/// # Examples +/// +/// ``` +/// # use polytype::{ptp, tp, with_ctx, Context, Source, Substitution, Variable}; +/// let t_string = with_ctx(32, |ctx| { +/// // filter: ∀α. (α → bool) → [α] → [α] +/// let t = ptp!(ctx, 0; @arrow[ +/// tp!(ctx, @arrow[tp!(ctx, 0), tp!(ctx, bool)]), +/// tp!(ctx, list(tp!(ctx, 0))), +/// tp!(ctx, list(tp!(ctx, 0))), +/// ]); +/// t.to_string() +/// }); +/// assert_eq!(t_string, "∀t0. (t0 → bool) → list(t0) → list(t0)"); +/// ``` +/// +/// [`TypeContext`]: struct.TypeContext.html +pub fn with_ctx(n: usize, f: F) -> R +where + F: FnOnce(TypeContext<'_, M>) -> R, +{ + let schemaa: Arena> = Arena::with_capacity(n); + let typea: Arena> = Arena::with_capacity(n); + let namea: Arena = Arena::with_capacity(n); + let tya: Arena> = Arena::with_capacity(n); + let ctx = Context::with_capacity(&schemaa, &typea, &namea, &tya, n); + let ctx: TypeContext<'_, M> = TypeContext::new(&ctx); + f(ctx) +} + +impl<'ctx, N: Name> TypeContext<'ctx, N> { + /// Create a new `TypeContext` from a [`Context`]. /// /// # Examples /// /// ``` - /// # use polytype::{Type, Context, ptp, tp}; - /// 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); - /// } + /// # use typed_arena::Arena; + /// # use polytype::{ptp, tp, Context, TypeContext, Type, TypeSchema, Ty}; + /// let schemaa: Arena> = Arena::with_capacity(10); + /// let typea: Arena> = Arena::with_capacity(10); + /// let namea: Arena<&'static str> = Arena::with_capacity(10); + /// let tya: Arena> = Arena::with_capacity(10); + /// let context = Context::with_capacity(&schemaa, &typea, &namea, &tya, 10); + /// let ctx = TypeContext::new(&context); + /// let t = ptp!(ctx, 0; @arrow[ + /// tp!(ctx, @arrow[tp!(ctx, 0), tp!(ctx, 1)]), + /// tp!(ctx, list(tp!(ctx, 0))), + /// tp!(ctx, list(tp!(ctx, 1))), + /// ]); + /// assert_eq!(t.to_string(), "∀t0. (t0 → t1) → list(t0) → list(t1)"); /// ``` - pub fn clean(&mut self) { - self.substitution.clear(); - self.path_compression_cache.get_mut().clear(); - } - /// Removes previous substitutions added to the `Context` until there are only `n` remaining. - pub fn rollback(&mut self, n: usize) { - self.path_compression_cache.get_mut().clear(); - if n == 0 { - self.substitution.clear(); - } else { - while n < self.substitution.len() { - self.substitution.pop(); - } - } - } - /// Create a new substitution for [`Type::Variable`] number `v` to the - /// [`Type`] `t`. /// - /// [`Type`]: enum.Type.html - /// [`Type::Variable`]: enum.Type.html#variant.Variable - pub fn extend(&mut self, v: Variable, t: Type) { - if v >= self.next { - self.next = v + 1 - } - self.substitution.insert(v, t); + /// [`Context`]: struct.Context.html + pub fn new(ctx: &'ctx Context<'ctx, N>) -> Self { + TypeContext { ctx } } - /// Create a new [`Type::Variable`] from the next unused number. + /// Intern a variable [`Type`]. /// /// # Examples /// /// ``` - /// # use polytype::{Type, Context, ptp, tp}; - /// 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)); + /// # use polytype::{with_ctx, TypeContext, Variable}; + /// with_ctx(32, |ctx: TypeContext<'_>| { + /// let t = ctx.intern_tvar(Variable(0)); + /// assert_eq!(t.to_string(), "t0"); + /// }); /// ``` /// - /// [`Type::Variable`]: enum.Type.html#variant.Variable - pub fn new_variable(&mut self) -> Type { - self.next += 1; - Type::Variable(self.next - 1) + /// [`Type`]: enum.Type.html + pub fn intern_tvar(&self, v: Variable) -> Ty<'ctx, N> { + let t = Type::Variable(v); + self.ctx + .type_map + .intern(t, |t| self.ctx.type_arena.alloc(t)) } - /// Create constraints within the context that ensure `t1` and `t2` - /// unify. + /// Intern a `&[`[`Ty`]`]`. /// /// # Examples /// + /// ```ignore + /// # use polytype::{with_ctx, Variable}; + /// # use itertools::Itertools; + /// with_ctx(32, |ctx| { + /// let ts = ctx.intern_args(&[tp!(ctx, int), tp!(ctx, bool)]); + /// assert_eq!(format!("[{}]", ts.iter().format!(", ")), "[int, bool]"); + /// }); /// ``` - /// # use polytype::{Context, tp}; - /// 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 - /// ``` + /// [`Ty`]: type.Ty.html + pub(crate) fn intern_args(&self, args: &[Ty<'ctx, N>]) -> &'ctx [Ty<'ctx, N>] { + self.ctx.arg_map.intern(args, |args| { + self.ctx.arg_arena.alloc_extend(args.iter().copied()) + }) + } + /// Intern a non-variable [`Type`]. /// - /// Unification errors leave the context unaffected. A - /// [`UnificationError::Failure`] error happens when symbols don't match: + /// # Examples /// /// ``` - /// # use polytype::{Context, UnificationError, tp}; - /// 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!() } + /// # use polytype::{tp, with_ctx, TypeContext, Variable}; + /// with_ctx(32, |ctx| { + /// let name = ctx.intern_name("dict"); + /// let t = ctx.intern_tcon(name, &[tp!(ctx, int), tp!(ctx, bool)]); + /// assert_eq!(t.to_string(), "dict(int,bool)"); + /// }); /// ``` /// - /// 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. - /// - /// ``` - /// # use polytype::{Context, UnificationError, tp}; - /// let mut ctx = Context::default(); + /// [`Type`]: enum.Type.html + pub fn intern_tcon(&self, head: &'ctx N, args: &[Ty<'ctx, N>]) -> Ty<'ctx, N> { + let body = self.intern_args(args); + let t = Type::Constructed(head, body); + self.ctx + .type_map + .intern(t, |t| self.ctx.type_arena.alloc(t)) + } + /// Intern a function (i.e. arrow) [`Type`]. /// - /// let t1 = tp!(1); - /// let t2 = tp!(@arrow[tp!(bool), tp!(1)]); - /// let res = ctx.unify(&t1, &t2); + /// # Examples /// - /// 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!() } + /// ``` + /// # use polytype::{tp, with_ctx, TypeContext, Variable}; + /// with_ctx(32, |ctx| { + /// let t = ctx.arrow(tp!(ctx, 0), tp!(ctx, bool)); + /// assert_eq!(t.to_string(), "t0 → bool"); + /// }); /// ``` /// - /// [`UnificationError::Failure`]: enum.UnificationError.html#variant.Failure - /// [`UnificationError::Occurs`]: enum.UnificationError.html#variant.Occurs - /// [`instantiate`]: enum.Type.html#method.instantiate - pub fn unify(&mut self, t1: &Type, t2: &Type) -> Result<(), UnificationError> { - let rollback_n = self.substitution.len(); - let t1 = t1.apply(self); - let t2 = t2.apply(self); - let result = self.unify_internal(t1, t2); - if result.is_err() { - self.rollback(rollback_n); - } - result - } - /// Like [`unify`], but may affect the context even under failure. Hence, use this if you - /// discard the context upon failure. - /// - /// [`unify`]: #method.unify - pub fn unify_fast( - &mut self, - mut t1: Type, - mut t2: Type, - ) -> Result<(), UnificationError> { - t1.apply_mut(self); - t2.apply_mut(self); - self.unify_internal(t1, t2) - } - /// unify_internal may mutate the context even with an error. The context on - /// which it's called should be discarded if there's an error. - fn unify_internal(&mut self, t1: Type, t2: Type) -> Result<(), UnificationError> { - if t1 == t2 { - return Ok(()); - } - match (t1, t2) { - (Type::Variable(v), t2) => { - if t2.occurs(v) { - Err(UnificationError::Occurs(v)) - } else { - self.extend(v, t2); - Ok(()) - } - } - (t1, Type::Variable(v)) => { - if t1.occurs(v) { - Err(UnificationError::Occurs(v)) - } else { - self.extend(v, t1); - Ok(()) - } - } - (Type::Constructed(n1, a1), Type::Constructed(n2, a2)) => { - if n1 != n2 { - Err(UnificationError::Failure( - Type::Constructed(n1, a1), - Type::Constructed(n2, a2), - )) - } else { - for (mut t1, mut t2) in a1.into_iter().zip(a2) { - t1.apply_mut(self); - t2.apply_mut(self); - self.unify_internal(t1, t2)?; - } - Ok(()) - } - } - } + /// [`Type`]: enum.Type.html + pub fn arrow(&self, alpha: Ty<'ctx, N>, beta: Ty<'ctx, N>) -> Ty<'ctx, N> { + let head = self.intern_name(N::arrow()); + self.intern_tcon(head, &[alpha, beta]) } - /// Confines the substitution to those which act on the given variables. + /// Intern a nested sequence of left-associative functions (i.e. arrow) as a + /// single [`Type`]. /// /// # Examples /// /// ``` - /// # use polytype::{Context, tp}; - /// 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)); + /// # use polytype::{tp, with_ctx, TypeContext, Variable}; + /// with_ctx(32, |ctx| { + /// let t = ctx.arrow_slice(&[tp!(ctx, 0), tp!(ctx, int), tp!(ctx, bool)]); + /// assert_eq!(t.to_string(), "t0 → int → bool"); + /// }); /// ``` - pub fn confine(&mut self, keep: &[Variable]) { - let mut substitution = IndexMap::new(); - for v in keep { - substitution.insert(*v, self.substitution[v].clone()); - } - self.substitution = substitution; - } - /// 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). + /// [`Type`]: enum.Type.html + pub fn arrow_slice(&self, tps: &[Ty<'ctx, N>]) -> Ty<'ctx, N> { + tps.iter() + .rev() + .copied() + .fold1(|x, y| self.arrow(y, x)) + .unwrap_or_else(|| panic!("cannot create a type from nothing")) + } + /// Intern a [`Ty`] as a [`TypeSchema::Monotype`]. /// /// # Examples /// - /// Without sacred variables, which assumes that all type variables between the contexts are - /// distinct: - /// /// ``` - /// # use polytype::{Type, Context, ptp, tp}; - /// 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 + /// # use polytype::{tp, with_ctx, TypeContext, Variable}; + /// with_ctx(32, |ctx| { + /// let t = tp!(ctx, @arrow[tp!(ctx, 0), tp!(ctx,int), tp!(ctx, bool)]); + /// let schema = ctx.intern_monotype(t); + /// assert_eq!(schema.to_string(), "t0 → int → bool"); + /// }); + /// ``` /// - /// 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 + /// [`Ty`]: type.Ty.html + /// [`TypeSchema::Monotype`]: enum.TypeSchema.html#variant.Monotype + pub fn intern_monotype(&self, inner: Ty<'ctx, N>) -> Schema<'ctx, N> { + let t = TypeSchema::Monotype(inner); + self.ctx + .schema_map + .intern(t, |t| self.ctx.schema_arena.alloc(t)) + } + /// Intern a [`Ty`] as a [`TypeSchema::Polytype`]. /// - /// 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"); + /// # Examples /// - /// assert_eq!(ctx.new_variable(), tp!(4)); /// ``` - /// - /// With sacred variables, which specifies which type variables are equivalent in both - /// contexts: - /// + /// # use polytype::{tp, with_ctx, TypeContext, Variable}; + /// with_ctx(32, |ctx| { + /// let t = tp!(ctx, @arrow[tp!(ctx, 0), tp!(ctx,int), tp!(ctx, bool)]); + /// let mono = ctx.intern_monotype(t); + /// let poly = ctx.intern_polytype(Variable(0), mono); + /// assert_eq!(poly.to_string(), "∀t0. t0 → int → bool"); + /// }); /// ``` - /// # use polytype::{Type, Context, tp}; - /// 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 + /// [`Ty`]: type.Ty.html + /// [`TypeSchema::Polytype`]: enum.TypeSchema.html#variant.Polytype + pub fn intern_polytype(&self, v: Variable, body: Schema<'ctx, N>) -> Schema<'ctx, N> { + let t = TypeSchema::Polytype(v, body); + self.ctx + .schema_map + .intern(t, |t| self.ctx.schema_arena.alloc(t)) + } + /// Intern a type constructor name. /// - /// // 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"); + /// # Examples /// - /// assert_eq!(ctx.new_variable(), tp!(4)); /// ``` - /// [`ContextChange::reify_type`]: struct.ContextChange.html#method.reify_type - /// [`ContextChange::reify_typeschema`]: struct.ContextChange.html#method.reify_typeschema - /// [`Type`]: enum.Type.html - /// [`TypeSchema`]: enum.TypeSchema.html - /// [`Variable`]: type.TypeSchema.html - pub fn merge(&mut self, other: Context, sacreds: Vec) -> ContextChange { - let delta = self.next; - for (v, tp) in other.substitution { - self.substitution.insert(delta + v, tp); - } - // this is intentionally wasting variable space when there are sacreds: - self.next += other.next; - ContextChange { delta, sacreds } + /// # use polytype::{tp, with_ctx, TypeContext, Variable}; + /// with_ctx(32, |ctx| { + /// let bool_name = ctx.intern_name("bool"); + /// assert_eq!(*bool_name, "bool"); + /// }); + /// ``` + pub fn intern_name(&self, n: N) -> &'ctx N { + self.ctx + .name_map + .intern(n, |n| self.ctx.name_arena.alloc(n)) } } -/// Allow types to be reified for use in a different context. See [`Context::merge`]. -/// -/// [`Context::merge`]: struct.Context.html#method.merge -pub struct ContextChange { - delta: usize, - sacreds: Vec, -} -impl ContextChange { - /// Reify a [`Type`] for use under a merged [`Context`]. +impl<'ctx, N: Name> Context<'ctx, N> { + /// Create a `Context`. /// - /// [`Type`]: enum.Type.html - /// [`Context`]: struct.Context.html - pub fn reify_type(&self, tp: &mut Type) { - match tp { - Type::Constructed(_, args) => { - for arg in args { - self.reify_type(arg) - } - } - Type::Variable(n) if self.sacreds.contains(n) => (), - Type::Variable(n) => *n += self.delta, + /// # Examples + /// + /// ``` + /// # use typed_arena::Arena; + /// # use polytype::{ptp, tp, Context, TypeContext, Type, TypeSchema, Ty}; + /// let schemaa: Arena> = Arena::with_capacity(10); + /// let typea: Arena> = Arena::with_capacity(10); + /// let namea: Arena<&'static str> = Arena::with_capacity(10); + /// let tya: Arena> = Arena::with_capacity(10); + /// let context = Context::new(&schemaa, &typea, &namea, &tya); + /// ``` + pub fn new( + schema_arena: &'ctx Arena>, + type_arena: &'ctx Arena>, + name_arena: &'ctx Arena, + arg_arena: &'ctx Arena>, + ) -> Self { + Context { + schema_arena, + schema_map: Interner::default(), + type_arena, + type_map: Interner::default(), + name_arena, + name_map: Interner::default(), + arg_arena, + arg_map: SliceInterner::default(), } } - /// Reify a [`TypeSchema`] for use under a merged [`Context`]. + /// Create a `Context` and reserve capacity for type interning. /// - /// [`TypeSchema`]: enum.TypeSchema.html - /// [`Context`]: struct.Context.html - pub fn reify_typeschema(&self, tpsc: &mut TypeSchema) { - match tpsc { - TypeSchema::Monotype(tp) => self.reify_type(tp), - TypeSchema::Polytype { variable, body } => { - *variable += self.delta; - self.reify_typeschema(body); - } + /// # Examples + /// + /// ``` + /// # use typed_arena::Arena; + /// # use polytype::{ptp, tp, Context, TypeContext, Type, TypeSchema, Ty}; + /// let schemaa: Arena> = Arena::with_capacity(10); + /// let typea: Arena> = Arena::with_capacity(10); + /// let namea: Arena<&'static str> = Arena::with_capacity(10); + /// let tya: Arena> = Arena::with_capacity(10); + /// let context = Context::with_capacity(&schemaa, &typea, &namea, &tya, 10); + /// ``` + pub fn with_capacity( + schema_arena: &'ctx Arena>, + type_arena: &'ctx Arena>, + name_arena: &'ctx Arena, + arg_arena: &'ctx Arena>, + n: usize, + ) -> Self { + Context { + schema_arena, + schema_map: Interner::with_capacity(n), + type_arena, + type_map: Interner::with_capacity(n), + name_arena, + name_map: Interner::with_capacity(n), + arg_arena, + arg_map: SliceInterner::with_capacity(n), } } } diff --git a/src/lib.rs b/src/lib.rs index c23edd4..df34b0f 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -1,113 +1,132 @@ //! A [Hindley-Milner polymorphic typing system]. //! -//! For brevity, the documentation heavily uses the two provided macros when -//! creating types. -//! //! A [`TypeSchema`] is a type that may have universally quantified type -//! variables. A [`Context`] keeps track of assignments made to type variables -//! so that you may manipulate [`Type`]s, which are unquantified and concrete. -//! Hence a `TypeSchema` can be instantiated, using [`TypeSchema::instantiate`], -//! into a `Context` in order to produce a corresponding `Type`. Two `Type`s -//! under a particular `Context` can be unified using [`Context::unify`], which -//! may record new type variable assignments in the `Context`. +//! variables. You can use [`TypeSchema::instantiate`] to produce a +//! corresponding [`Type`], which is unquantified. Both can contain +//! [`Variable`]s, which are concrete but unknown types. [`Type::unify`] unifies +//! two [`Type`]s, recording constraints on [`Variable`]s in a [`Substitution`]. +//! The [`Infer`] trait provides a simple interface for using these abilities to +//! support custom type inference and type checking algorithms. All types are +//! managed within a given [`TypeContext`], which interns type information for +//! faster inference. As a result, most user-facing access comes by way of +//! [`Schema`] and [`Ty`], references to interned [`TypeSchema`]s and [`Type`]s, +//! respectively. +//! +//! For brevity, the documentation heavily uses the two provided macros [`tp`] +//! and [`ptp`] when creating types. //! //! # Examples //! //! The basics: //! //! ``` -//! use polytype::{ptp, tp, Context}; +//! use polytype::{ptp, tp, with_ctx, Context, Source, Substitution, Variable}; //! -//! // filter: ∀α. (α → bool) → [α] → [α] -//! let t = ptp!(0; @arrow[ -//! tp!(@arrow[tp!(0), tp!(bool)]), -//! tp!(list(tp!(0))), -//! tp!(list(tp!(0))), -//! ]); +//! // Types are defined with respect to a given TypeContext. Here, it's `ctx`. +//! with_ctx(32, |ctx| { +//! // filter: ∀α. (α → bool) → [α] → [α] +//! let t = ptp!(ctx, 0; @arrow[ +//! tp!(ctx, @arrow[tp!(ctx, 0), tp!(ctx, bool)]), +//! tp!(ctx, list(tp!(ctx, 0))), +//! tp!(ctx, list(tp!(ctx, 0))), +//! ]); //! -//! // Quantified type schemas provide polymorphic behavior. -//! assert_eq!(t.to_string(), "∀t0. (t0 → bool) → list(t0) → list(t0)"); +//! // Quantified type schemas provide polymorphic behavior. +//! assert_eq!(t.to_string(), "∀t0. (t0 → bool) → list(t0) → list(t0)"); //! -//! // We can instantiate type schemas to remove quantifiers -//! let mut ctx = Context::default(); -//! let t = t.instantiate(&mut ctx); -//! assert_eq!(t.to_string(), "(t0 → bool) → list(t0) → list(t0)"); +//! // We can instantiate type schemas to remove quantifiers +//! let mut source = Source::default(); +//! let t = t.instantiate(&ctx, &mut source); +//! assert_eq!(t.to_string(), "(t0 → bool) → list(t0) → list(t0)"); //! -//! // We can register a substitution for t0 in the context: -//! ctx.extend(0, tp!(int)); -//! let t = t.apply(&ctx); -//! assert_eq!(t.to_string(), "(int → bool) → list(int) → list(int)"); +//! // We can register a substitution for t0 in the context: +//! let mut sub = Substitution::with_capacity(ctx, 32); +//! sub.add(Variable(0), tp!(ctx, int)); +//! let t = t.apply(&sub); +//! assert_eq!(t.to_string(), "(int → bool) → list(int) → list(int)"); +//! }) //! ``` //! //! Extended example: //! //! ``` -//! use polytype::{ptp, tp, Context}; +//! use polytype::{ptp, tp, with_ctx, Context, Source, Type}; //! -//! // reduce: ∀α. ∀β. (β → α → β) → β → [α] → β -//! // We can represent the type schema of reduce using the included macros: -//! let t = ptp!(0, 1; @arrow[ -//! tp!(@arrow[tp!(1), tp!(0), tp!(1)]), -//! tp!(1), -//! tp!(list(tp!(0))), -//! tp!(1), -//! ]); -//! assert_eq!(t.to_string(), "∀t0. ∀t1. (t1 → t0 → t1) → t1 → list(t0) → t1"); +//! with_ctx(32, |ctx| { +//! // reduce: ∀α. ∀β. (β → α → β) → β → [α] → β +//! let t = ptp!(ctx, 0, 1; @arrow[ +//! tp!(ctx, @arrow[tp!(ctx, 1), tp!(ctx, 0), tp!(ctx, 1)]), +//! tp!(ctx, 1), +//! tp!(ctx, list(tp!(ctx, 0))), +//! tp!(ctx, 1), +//! ]); +//! assert_eq!(t.to_string(), "∀t0. ∀t1. (t1 → t0 → t1) → t1 → list(t0) → t1"); //! -//! // Let's consider reduce when applied to a function that adds two ints +//! // We also create a source of fresh type variables. +//! let mut src = Source::default(); //! -//! // First, we create a new typing context to manage typing bookkeeping. -//! let mut ctx = Context::default(); +//! // Consider reduce when applied to a function that adds two `ints`. //! -//! // Let's create a type representing binary addition. -//! let tplus = tp!(@arrow[tp!(int), tp!(int), tp!(int)]); -//! assert_eq!(tplus.to_string(), "int → int → int"); +//! // Let's create a type representing binary addition. +//! let tint = tp!(ctx, int); +//! let tplus = tp!(ctx, @arrow[tint, tint, tint]); +//! assert_eq!(tplus.to_string(), "int → int → int"); //! -//! // We instantiate the type schema of reduce within our context -//! // so new type variables will be distinct -//! let t = t.instantiate(&mut ctx); -//! assert_eq!(t.to_string(), "(t1 → t0 → t1) → t1 → list(t0) → t1"); +//! // We instantiate the type schema of reduce within our context +//! // so new type variables will be distinct +//! let t = t.instantiate(&ctx, &mut src); +//! assert_eq!(t.to_string(), "(t1 → t0 → t1) → t1 → list(t0) → t1"); //! -//! // By unifying, we can ensure function applications obey type requirements. -//! let treturn = ctx.new_variable(); -//! let targ1 = ctx.new_variable(); -//! let targ2 = ctx.new_variable(); -//! ctx.unify( -//! &t, -//! &tp!(@arrow[ -//! tplus.clone(), -//! targ1.clone(), -//! targ2.clone(), -//! treturn.clone(), -//! ]), -//! ).expect("unifies"); +//! // By unifying, we can ensure function applications obey type requirements. +//! let treturn = tp!(ctx, src.fresh()); +//! let targ1 = tp!(ctx, src.fresh()); +//! let targ2 = tp!(ctx, src.fresh()); +//! let sub = Type::unify(&[( +//! t, +//! tp!(ctx, @arrow[ +//! tplus, +//! targ1, +//! targ2, +//! treturn, +//! ]) +//! )], &ctx).expect("unifies"); //! -//! // We can also now infer what arguments are needed and what gets returned -//! assert_eq!(targ1.apply(&ctx), tp!(int)); // inferred arg 1: int -//! assert_eq!(targ2.apply(&ctx), tp!(list(tp!(int)))); // inferred arg 2: list(int) -//! assert_eq!(treturn.apply(&ctx), tp!(int)); // inferred return: int +//! // We can also now infer what arguments are needed and what gets returned +//! assert_eq!(targ1.apply(&sub), tint); // inferred arg 1: int +//! assert_eq!(targ2.apply(&sub), tp!(ctx, list(tint))); // inferred arg 2: list(int) +//! assert_eq!(treturn.apply(&sub), tint); // inferred return: int //! -//! // Finally, we can see what form reduce takes by applying the new substitution -//! let t = t.apply(&ctx); -//! assert_eq!(t.to_string(), "(int → int → int) → int → list(int) → int"); +//! // Finally, we can see what form reduce takes by applying the new substitution +//! let t = t.apply(&sub); +//! assert_eq!(t.to_string(), "(int → int → int) → int → list(int) → int"); +//! }) //! ``` //! -//! [`Context`]: struct.Context.html -//! [`Context::unify`]: struct.Context.html#method.unify +//! [`ptp`]: macro.ptp.html +//! [`tp`]: macro.tp.html +//! [`Infer`]: trait.Infer.html +//! [`Substitution`]: struct.Substitution.html //! [`Type`]: enum.Type.html +//! [`Type::unify`]: enum.Type.html#method.unify +//! [`TypeContext`]: struct.TypeContext.html //! [`TypeSchema::instantiate`]: enum.TypeSchema.html#method.instantiate //! [`TypeSchema`]: enum.TypeSchema.html +//! [`Schema`]: type.Schema.html +//! [`Ty`]: type.Ty.html //! [Hindley-Milner polymorphic typing system]: https://en.wikipedia.org/wiki/Hindley–Milner_type_system mod context; mod macros; -#[cfg(feature = "parser")] mod parser; +mod source; +mod substitution; mod types; -pub use context::{Context, ContextChange, UnificationError}; -pub use parser::ParseError; -pub use types::{Type, TypeSchema, Variable}; +pub use context::{with_ctx, Context, TypeContext}; +pub use source::{Source, SourceChange}; +use std::hash::Hash; +pub use substitution::{Snapshot, Substitution}; +pub use types::{Schema, Ty, Type, TypeSchema, UnificationError, Variable}; /// Types require a `Name` for comparison. /// @@ -119,30 +138,38 @@ pub use types::{Type, TypeSchema, Variable}; /// Using static strings: /// /// ``` -/// # use polytype::Type; -/// let t = Type::Constructed("int", vec![]) -/// # ; +/// # use polytype::with_ctx; +/// with_ctx(32, |ctx| { +/// let tint = ctx.intern_tcon(ctx.intern_name("int"), &[]); +/// }) /// ``` /// /// A custom implementation: /// /// ``` -/// # use polytype::{Type, Name}; -/// #[derive(Clone, PartialEq, Eq)] +/// # use polytype::{with_ctx, Name}; +/// #[derive(Clone, PartialEq, Eq, Hash)] /// struct N(u8); /// /// impl Name for N { +/// type ParseError = &'static str; /// fn arrow() -> Self { /// N(0) /// } +/// fn parse(s: &str) -> Result { +/// s.parse::().map(|n| N(n)).or(Err("failed to parse Name")) +/// } /// } /// -/// let t: Type = Type::Constructed(N(1), vec![]) -/// # ; +/// with_ctx(32, |ctx| { +/// let tint = ctx.intern_tcon(ctx.intern_name(N(1)), &[]); +/// }) /// ``` /// /// [`arrow`]: #tymethod.arrow -pub trait Name: Clone + Eq { +pub trait Name: Clone + Eq + Hash { + /// A description of a failed `Name` parse. + type ParseError; /// A specific name representing an arrow must be declared. fn arrow() -> Self; /// A way of displaying the name. @@ -153,15 +180,14 @@ pub trait Name: Clone + Eq { /// with [`show`]. /// /// [`show`]: #method.show - fn parse(_s: &str) -> Result { - Err(ParseError) - } - + fn parse(s: &str) -> Result; + /// Returns `true` if the name represents an arrow, else `false`. fn is_arrow(&self) -> bool { *self == Self::arrow() } } impl Name for &'static str { + type ParseError = &'static str; /// The rightwards arrow in unicode: `→`. #[inline(always)] fn arrow() -> &'static str { @@ -173,10 +199,10 @@ impl Name for &'static str { } /// **LEAKY** because it gives the string a static lifetime. #[inline(always)] - fn parse(s: &str) -> Result<&'static str, ParseError> { + fn parse(s: &str) -> Result<&'static str, Self::ParseError> { Ok(unsafe { &mut *Box::into_raw(s.to_string().into_boxed_str()) }) } - /// The rightwards arrow in unicode: `→`. + /// Checks whether a name is the rightwards arrow in unicode: `→`. #[inline(always)] fn is_arrow(&self) -> bool { *self == "→" @@ -190,30 +216,38 @@ impl Name for &'static str { /// In the simplest case, you statically know what the type is: /// /// ``` -/// use polytype::{tp, Infer, Type, UnificationError}; +/// use polytype::{tp, with_ctx, Infer, Ty, TypeContext, UnificationError}; /// /// struct MyPrimitive; -/// impl Infer<()> for MyPrimitive { -/// fn infer(&self, _ctx: &()) -> Result { -/// Ok(tp!(my_thing_tp)) +/// impl<'ctx> Infer<'ctx, TypeContext<'ctx>> for MyPrimitive { +/// fn infer(&self, ctx: &TypeContext<'ctx>) -> Result, UnificationError<'ctx>> { +/// Ok(tp!(ctx, my_thing_tp)) /// } /// } /// -/// assert_eq!(MyPrimitive.infer(&()), Ok(tp!(my_thing_tp))); +/// with_ctx(32, |ctx| { +/// assert_eq!(MyPrimitive.infer(&ctx), Ok(tp!(ctx, my_thing_tp))); +/// }) /// ``` /// /// A more complex case builds a new type given typed items. /// /// ``` -/// use polytype::{ptp, tp, Context, Infer, Type, TypeSchema, UnificationError}; +/// use polytype::{ +/// ptp, tp, with_ctx, Source, Substitution, Infer, +/// Ty, Type, TypeContext, Schema, UnificationError +/// }; /// use std::cell::RefCell; /// -/// type MyCtx = RefCell; // the RefCell allows us to mutate the context during inference +/// // the RefCell allows us to mutate the context during inference +/// type MyCtx<'ctx> = RefCell<(Source, TypeContext<'ctx>)>; /// -/// struct Primitive(TypeSchema); -/// impl Infer for Primitive { -/// fn infer(&self, ctx: &MyCtx) -> Result { -/// Ok(self.0.instantiate(&mut ctx.borrow_mut())) +/// struct Primitive<'ctx>(Schema<'ctx>); +/// impl<'ctx> Infer<'ctx, MyCtx<'ctx>> for Primitive<'ctx> { +/// fn infer(&self, ctx: &MyCtx<'ctx>) -> Result, UnificationError<'ctx>> { +/// let mut inner = ctx.borrow_mut(); +/// let tctx = inner.1; +/// Ok(self.0.instantiate(&tctx, &mut inner.0)) /// } /// } /// @@ -221,28 +255,35 @@ impl Name for &'static str { /// left: A, /// right: B, /// } -/// impl, B: Infer> Infer for Application { -/// fn infer(&self, ctx: &MyCtx) -> Result { +/// impl<'ctx, A, B> Infer<'ctx, MyCtx<'ctx>> for Application +/// where +/// A: Infer<'ctx, MyCtx<'ctx>>, +/// B: Infer<'ctx, MyCtx<'ctx>> +/// { +/// fn infer(&self, ctx: &MyCtx<'ctx>) -> Result, UnificationError<'ctx>> { /// let ft = self.left.infer(ctx)?; /// let xt = self.right.infer(ctx)?; /// let mut ctx = ctx.borrow_mut(); -/// let ret = ctx.new_variable(); -/// ctx.unify(&ft, &Type::arrow(xt, ret.clone()))?; -/// Ok(ret.apply(&ctx)) +/// let tctx = ctx.1; +/// let ret = tp![tctx, ctx.0.fresh()]; +/// let sub = Type::unify(&[(ft, tctx.arrow(xt, ret))], &tctx)?; +/// Ok(ret.apply(&sub)) /// } /// } /// -/// let f = Primitive(ptp!(@arrow[tp!(foo), tp!(bar)])); -/// let x = Primitive(ptp!(foo)); -/// let fx = Application { left: f, right: x }; -/// let ctx = RefCell::new(Context::default()); -/// assert_eq!(fx.infer(&ctx), Ok(tp!(bar))); +/// with_ctx(32, |ctx| { +/// let f = Primitive(ptp!(ctx, @arrow[tp!(ctx, foo), tp!(ctx, bar)])); +/// let x = Primitive(ptp!(ctx, foo)); +/// let fx = Application { left: f, right: x }; +/// let c = RefCell::new((Source::default(), ctx)); +/// assert_eq!(fx.infer(&c), Ok(tp!(ctx, bar))); +/// }) /// ``` /// /// A more sophisticated case has the types maintained externally: /// /// ``` -/// use polytype::{ptp, tp, Context, Infer, Type, TypeSchema, UnificationError}; +/// use polytype::{ptp, tp, with_ctx, Infer, Schema, Source, Substitution, Ty, Type, TypeContext, UnificationError, Variable}; /// use std::{cell::RefCell, collections::HashMap}; /// /// // in this example, every Term has a Type defined through the Lexicon @@ -250,61 +291,67 @@ impl Name for &'static str { /// GlobalVariable(u32), /// Application { op: u32, args: Vec }, /// } -/// struct Lexicon { -/// ctx: RefCell, -/// ops: HashMap, -/// global_vars: RefCell>, +/// struct Lexicon<'ctx> { +/// src: RefCell, +/// sub: RefCell>, +/// ctx: TypeContext<'ctx>, +/// ops: HashMap>, +/// global_vars: RefCell>>, /// } /// -/// impl Infer for Term { -/// fn infer(&self, lex: &Lexicon) -> Result { +/// impl<'ctx> Infer<'ctx, Lexicon<'ctx>> for Term { +/// fn infer(&self, lex: &Lexicon<'ctx>) -> Result, UnificationError<'ctx>> { /// match self { /// Term::GlobalVariable(v) => Ok(lex /// .global_vars /// .borrow_mut() /// .entry(*v) -/// .or_insert_with(|| lex.ctx.borrow_mut().new_variable()) -/// .clone()), +/// .or_insert_with(|| lex.ctx.intern_tvar(Variable(lex.src.borrow_mut().fresh())))), /// Term::Application { op, args } => { -/// let mut arg_types: Vec = args +/// let mut arg_types: Vec = args /// .into_iter() /// .map(|arg| arg.infer(lex)) /// .collect::, _>>()?; -/// let mut ctx = lex.ctx.borrow_mut(); -/// let ret = ctx.new_variable(); -/// arg_types.push(ret.clone()); -/// let func_type = lex.ops[op].instantiate(&mut ctx); -/// ctx.unify(&func_type, &Type::from(arg_types))?; -/// Ok(ret.apply(&ctx)) +/// let mut src = lex.src.borrow_mut(); +/// let ret = lex.ctx.intern_tvar(Variable(src.fresh())); +/// arg_types.push(ret); +/// let func_type = lex.ops[op].instantiate(&lex.ctx, &mut src); +/// Type::unify_with_sub(&[(func_type, lex.ctx.arrow_slice(&arg_types))], &mut lex.sub.borrow_mut())?; +/// Ok(ret.apply(&lex.sub.borrow())) /// } /// } /// } /// } /// -/// let mut h = HashMap::new(); -/// h.insert(0, ptp!(0; @arrow[tp!(0), tp!(foo)])); -/// h.insert(1, ptp!(@arrow[tp!(bar), tp!(baz)])); -/// let lex = Lexicon { -/// ctx: RefCell::new(Context::default()), -/// ops: h, -/// global_vars: RefCell::new(HashMap::new()), -/// }; -/// let term = Term::Application { -/// op: 0, -/// args: vec![Term::Application { -/// op: 1, -/// args: vec![Term::GlobalVariable(42)], -/// }], -/// }; -/// assert_eq!(term.infer(&lex), Ok(tp!(foo))); -/// assert_eq!( -/// lex.global_vars -/// .borrow() -/// .get(&42) -/// .map(|t| t.apply(&lex.ctx.borrow())), -/// Some(tp!(bar)) -/// ); +/// with_ctx(32, |ctx| { +/// let mut h = HashMap::new(); +/// h.insert(0, ptp!(ctx, 0; @arrow[tp!(ctx, 0), tp!(ctx, foo)])); +/// h.insert(1, ptp!(ctx, @arrow[tp!(ctx, bar), tp!(ctx, baz)])); +/// let lex = Lexicon { +/// src: RefCell::new(Source::default()), +/// sub: RefCell::new(Substitution::with_capacity(ctx, 32)), +/// ops: h, +/// global_vars: RefCell::new(HashMap::new()), +/// ctx, +/// }; +/// let term = Term::Application { +/// op: 0, +/// args: vec![Term::Application { +/// op: 1, +/// args: vec![Term::GlobalVariable(42)], +/// }], +/// }; +/// assert_eq!(term.infer(&lex), Ok(tp!(ctx, foo))); +/// assert_eq!( +/// lex.global_vars +/// .borrow() +/// .get(&42) +/// .map(|t| t.apply(&lex.sub.borrow())), +/// Some(tp!(ctx, bar)) +/// ); +/// }) /// ``` -pub trait Infer { - fn infer(&self, ctx: &Context) -> Result, E>; +pub trait Infer<'ctx, Context, E = UnificationError<'ctx>, N: Name = &'static str> { + /// Given a context, return a principal typing or fail. + fn infer(&self, ctx: &Context) -> Result, E>; } diff --git a/src/macros.rs b/src/macros.rs index a559c8c..ce0ed4f 100644 --- a/src/macros.rs +++ b/src/macros.rs @@ -1,27 +1,16 @@ -/// Creates a [`Type`][] (convenience for common patterns). +/// Creates a [`Ty`] (convenience for common patterns). /// -/// Specifically, a `Type<&'static str>`, where all names are static strings. +/// Specifically, a `&Type<'ctx, &'static str>`, where all names are static strings. /// /// ```rust,ignore /// // Equivalent to: -/// Type::Constructed(ident, vec![ +/// &'ctx Type::Constructed(ident, vec![ /// tp1, /// tp2, /// ... /// ]) /// // or -/// Type::Variable(n) -/// // or -/// Type::arrow( -/// tp0, -/// Type::arrow( -/// tp1, -/// Type::arrow( -/// tp2, -/// ..., -/// ) -/// ) -/// ) +/// &'ctx Type::Variable(n) /// ``` /// /// # Examples @@ -29,98 +18,118 @@ /// Make a primitive type: /// /// ``` -/// # use polytype::{tp, Type}; -/// let t = tp!(int); -/// assert_eq!(format!("{}", t), "int"); +/// # use polytype::{tp, with_ctx}; +/// # with_ctx(32, |ctx| { +/// let t_macro = tp!(ctx, int); +/// assert_eq!(t_macro.to_string(), "int"); /// // Equivalent to: -/// let t_eq = Type::Constructed("int", vec![]); -/// assert_eq!(t, t_eq); +/// let name = ctx.intern_name("int"); +/// let t_manual = ctx.intern_tcon(name, &[]); +/// assert_eq!(t_macro, t_manual); +/// # }) /// ``` /// /// Make a variable type: /// /// ``` -/// # use polytype::{tp, Type}; -/// let t = tp!(0); -/// assert_eq!(format!("{}", t), "t0"); +/// # use polytype::{tp, with_ctx, Ty, Variable}; +/// # with_ctx(32, |ctx| { +/// # ctx.intern_name("int"); +/// let t_macro = tp!(ctx, 0); +/// assert_eq!(t_macro.to_string(), "t0"); /// // Equivalent to: -/// let t_eq = Type::Variable(0); -/// assert_eq!(t, t_eq); +/// let t_manual = ctx.intern_tvar(Variable(0)); +/// assert_eq!(t_macro, t_manual); +/// # }) /// ``` /// /// Make a composite type: /// /// ``` -/// # use polytype::{tp, Type}; -/// let tint = tp!(int); -/// let tstr = tp!(str); -/// let t = tp!(dict(tstr, tint)); -/// assert_eq!(format!("{}", t), "dict(str,int)"); +/// # use polytype::{tp, with_ctx, Ty, Variable}; +/// # with_ctx(32, |ctx| { +/// let t_macro = tp!(ctx, dict(tp!(ctx, str), tp!(ctx, int))); +/// assert_eq!(t_macro.to_string(), "dict(str,int)"); /// // Equivalent to: -/// let t_eq = Type::Constructed("dict", vec![ -/// Type::Constructed("str", vec![]), -/// Type::Constructed("int", vec![]), -/// ]); -/// assert_eq!(t, t_eq); +/// let nint = ctx.intern_name("int"); +/// let nstr = ctx.intern_name("str"); +/// let ndict = ctx.intern_name("dict"); +/// let tint_manual = ctx.intern_tcon(nint, &[]); +/// let tstr_manual = ctx.intern_tcon(nstr, &[]); +/// let t_manual = ctx.intern_tcon(ndict, &[tstr_manual, tint_manual]); +/// assert_eq!(t_macro, t_manual); +/// # }) /// ``` /// /// Make an arrow: /// /// ``` -/// # use polytype::{tp, Type}; -/// let t = tp!(@arrow[Type::Variable(0), Type::Variable(1), Type::Variable(2)]); -/// assert_eq!(format!("{}", t), "t0 → t1 → t2"); +/// # use polytype::{tp, with_ctx, Ty, Variable}; +/// # with_ctx(32, |ctx| { +/// # ctx.intern_name("int"); +/// let t_macro = tp!(ctx, @arrow[tp!(ctx, 0), tp!(ctx, 1), tp!(ctx, 2)]); +/// assert_eq!(t_macro.to_string(), "t0 → t1 → t2"); /// // Equivalent to: -/// let t_eq = Type::arrow( -/// Type::Variable(0), -/// Type::arrow( -/// Type::Variable(1), -/// Type::Variable(2), -/// ) -/// ); -/// assert_eq!(t, t_eq); +/// let t_0 = ctx.intern_tvar(Variable(0)); +/// let t_1 = ctx.intern_tvar(Variable(1)); +/// let t_2 = ctx.intern_tvar(Variable(2)); +/// let t_manual = ctx.arrow_slice(&[t_0, t_1, t_2]); +/// assert_eq!(t_macro, t_manual); +/// # }) /// ``` /// /// Nest them for more complex types: /// /// ``` -/// # use polytype::{tp, Type}; +/// # use polytype::{tp, with_ctx, Ty, Variable}; +/// # with_ctx(32, |ctx| { /// // mapi: (int → α → β) → [α] → [β] -/// let t = tp!(@arrow[ -/// tp!(@arrow[tp!(int), tp!(0), tp!(1)]), -/// tp!(list(tp!(0))), -/// tp!(list(tp!(1))), +/// let t = tp!(ctx, @arrow[ +/// tp!(ctx, @arrow[tp!(ctx, int), tp!(ctx, 0), tp!(ctx, 1)]), +/// tp!(ctx, list(tp!(ctx, 0))), +/// tp!(ctx, list(tp!(ctx, 1))), /// ]); -/// assert_eq!(format!("{}", t), "(int → t0 → t1) → list(t0) → list(t1)"); +/// assert_eq!(t.to_string(), "(int → t0 → t1) → list(t0) → list(t1)"); +/// # }) /// ``` /// -/// [`Type`]: enum.Type.html +/// [`Ty`]: type.Ty.html #[macro_export] macro_rules! tp { - ($n:ident) => ($crate::Type::Constructed(stringify!($n), Vec::new())); - ($n:ident($($x:expr),*)) => { - $crate::Type::Constructed(stringify!($n), vec![$($x),*]) + // name of context and name of type. + ($ctx:ident, $n:ident) => { + $ctx.intern_tcon($ctx.intern_name(stringify!($n)), &[]) }; - ($n:ident($($x:expr,)*)) => ($crate::tp!($n($($x),*))); - ($n:expr) => ($crate::Type::Variable($n) as $crate::Type<&'static str>); - (@arrow[$x:expr]) => ($x as $crate::Type<&'static str>); - (@arrow[$x:expr, $($xs:expr),*]) => ( - match ($x, $crate::tp!(@arrow[$($xs),+])) { - (arg, ret) => $crate::Type::arrow(arg, ret) + // name of context, name of head, a comma-separated list of expressions + ($ctx:ident, $n:ident($($x:expr),*)) => { + $ctx.intern_tcon($ctx.intern_name(stringify!($n)), &[$($x),*]) + }; + // name of context, name of head, + // TODO: is this necessary? + ($ctx:ident, $n:ident($($x:expr,)*)) => ($crate::tp!($ctx, $n($($x),*))); + // name of context, numerical value that is a variable value. + ($ctx:ident, $n:expr) => ($ctx.intern_tvar($crate::Variable($n))); + // Not sure why this is here...shouldn't be a valid type. + // TODO: revise this to make sure arrows always have two? + ($ctx:ident, @arrow[$x:expr]) => ($x); + ($ctx:ident, @arrow[$x:expr, $($xs:expr),*]) => ( + match ($x, $crate::tp!($ctx, @arrow[$($xs),+])) { + (arg, ret) => $ctx.arrow(arg, ret) } ); - (@arrow[$x:expr, $($xs:expr,)*]) => ($crate::tp!(@arrow[$x, $($xs),*])) + // another rule matching + ($ctx:ident, @arrow[$x:expr, $($xs:expr,)*]) => ($crate::tp!($ctx, @arrow[$x, $($xs),*])) } -/// Creates a [`TypeSchema`][] (convenience for common patterns). +/// Creates a [`Schema`] (convenience for common patterns). /// -/// Specifically, a `TypeSchema<&'static str>`, where all names are static strings. +/// Specifically, a `&Schema<'ctx, &'static str>`, where all names are static strings. /// /// ```rust,ignore /// // Equivalent to: -/// TypeSchema::Monotype(tp) +/// &'ctx TypeSchema::Monotype(tp) /// // Or -/// TypeSchema::Polytype { +/// &'ctx TypeSchema::Polytype { /// variable1, /// body: Box::new(TypeSchema::Polytype { /// variable2, @@ -129,27 +138,29 @@ macro_rules! tp { /// } /// ``` /// -/// This behaves much like [`tp!`], but this gives a [`TypeSchema`] and you can +/// This behaves much like [`tp!`], but this gives a [`Schema`] and you can /// express quantified type variables in a prefixed comma-delimited list. There /// are three usage patterns, shown in the examples below. /// /// # Examples /// /// If you don't want to do any quantification, using `ptp!` on its own is just -/// like wrapping [`tp!`] with a [`TypeSchema::Monotype`]: +/// like wrapping a [`Type`] with a [`TypeSchema::Monotype`]: /// /// ``` -/// # use polytype::{ptp, tp, Type, TypeSchema}; -/// let t = ptp!(dict(tp!(str), tp!(int))); -/// assert_eq!(format!("{}", t), "dict(str,int)"); +/// # use polytype::{tp, ptp, with_ctx}; +/// # with_ctx(32, |ctx| { +/// let t_macro = ptp!(ctx, dict(tp!(ctx, str), tp!(ctx, int))); +/// assert_eq!(t_macro.to_string(), "dict(str,int)"); /// // Equivalent to: -/// let t_eq = TypeSchema::Monotype( -/// Type::Constructed("dict", vec![ -/// Type::Constructed("str", vec![]), -/// Type::Constructed("int", vec![]), -/// ]) -/// ); -/// assert_eq!(t, t_eq); +/// let nint = ctx.intern_name("int"); +/// let nstr = ctx.intern_name("str"); +/// let ndict = ctx.intern_name("dict"); +/// let tint_manual = ctx.intern_tcon(nint, &[]); +/// let tstr_manual = ctx.intern_tcon(nstr, &[]); +/// let t_manual = ctx.intern_monotype(ctx.intern_tcon(ndict, &[tstr_manual, tint_manual])); +/// assert_eq!(t_macro, t_manual); +/// # }) /// ``` /// /// If you want to do quantification over a known monotype, precede the type @@ -157,73 +168,66 @@ macro_rules! tp { /// subsequent monotype is treated like the [`tp!`] macro): /// /// ``` -/// # use polytype::{ptp, tp, Type, TypeSchema}; -/// let t = ptp!(0, 1; @arrow[tp!(0), tp!(1), tp!(0)]); -/// assert_eq!(format!("{}", t), "∀t0. ∀t1. t0 → t1 → t0"); +/// # use polytype::{tp, ptp, Variable, with_ctx}; +/// # with_ctx(32, |ctx| { +/// # ctx.intern_name("int"); +/// let t_macro = ptp!(ctx, 0, 1; @arrow[tp!(ctx, 0), tp!(ctx, 1), tp!(ctx, 0)]); +/// assert_eq!(t_macro.to_string(), "∀t0. ∀t1. t0 → t1 → t0"); /// // Equivalent to: -/// let t_eq = TypeSchema::Polytype { -/// variable: 0, -/// body: Box::new(TypeSchema::Polytype { -/// variable: 1, -/// body: Box::new(TypeSchema::Monotype( -/// Type::arrow( -/// Type::Variable(0), -/// Type::arrow( -/// Type::Variable(1), -/// Type::Variable(0), -/// ) -/// ) -/// )) -/// }) -/// }; -/// assert_eq!(t, t_eq); +/// let t_0 = ctx.intern_tvar(Variable(0)); +/// let t_1 = ctx.intern_tvar(Variable(1)); +/// let t_arrow = ctx.arrow_slice(&[t_0, t_1, t_0]); +/// let t_manual = ctx.intern_polytype( +/// Variable(0), +/// ctx.intern_polytype( +/// Variable(1), +/// ctx.intern_monotype(t_arrow), +/// ) +/// ); +/// assert_eq!(t_macro, t_manual); +/// # }) /// ``` /// /// If you want want do quantification over an existing [`TypeSchema`], use a /// comma after the quantified variables: /// /// ``` -/// # use polytype::{ptp, tp, Type, TypeSchema}; -/// let inner = tp!(@arrow[tp!(0), tp!(1), tp!(0)]); -/// let t = ptp!(0, 1, TypeSchema::Monotype(inner.clone())); -/// assert_eq!(format!("{}", t), "∀t0. ∀t1. t0 → t1 → t0"); +/// # use polytype::{tp, ptp, Variable, with_ctx}; +/// # with_ctx(32, |ctx| { +/// # ctx.intern_name("int"); +/// let inner = ptp!(ctx, @arrow[tp!(ctx, 0), tp!(ctx, 1), tp!(ctx, 0)]); +/// let t_macro = ptp!(ctx, 0, 1, inner); +/// assert_eq!(t_macro.to_string(), "∀t0. ∀t1. t0 → t1 → t0"); /// // Equivalent to: -/// let t_eq = TypeSchema::Polytype { -/// variable: 0, -/// body: Box::new(TypeSchema::Polytype { -/// variable: 1, -/// body: Box::new(TypeSchema::Monotype(inner)) -/// }) -/// }; -/// assert_eq!(t, t_eq); +/// let t_manual = ctx.intern_polytype( +/// Variable(0), +/// ctx.intern_polytype( +/// Variable(1), +/// inner, +/// ) +/// ); +/// assert_eq!(t_macro, t_manual); +/// # }) /// ``` /// +/// [`TypeSchema`]: enum.TypeSchema.html /// [`TypeSchema::Polytype`]: enum.TypeSchema.html#variant.Polytype /// [`TypeSchema::Monotype`]: enum.TypeSchema.html#variant.Monotype -/// [`TypeSchema`]: enum.TypeSchema.html +/// [`Schema`]: type.Schema.html /// [`Type`]: enum.Type.html /// [`tp!`]: macro.tp.html #[macro_export] macro_rules! ptp { - ($n:expr; $($t:tt)+) => { - $crate::TypeSchema::Polytype { - variable: $n, - body: Box::new($crate::TypeSchema::Monotype($crate::tp!($($t)+))), - } + ($ctx:ident, $n:expr; $($t:tt)+) => { + $ctx.intern_polytype($crate::Variable($n), $crate::ptp!($ctx, $($t)+)) }; - ($n:expr, $body:expr) => { - $crate::TypeSchema::Polytype { - variable: $n, - body: Box::new($body), - } + ($ctx:ident, $n:expr, $body:expr) => { + $ctx.intern_polytype($crate::Variable($n), $body) }; - ($n:expr, $($t:tt)+) => { - $crate::TypeSchema::Polytype { - variable: $n, - body: Box::new($crate::ptp!($($t)+)), - } + ($ctx:ident, $n:expr, $($t:tt)+) => { + $ctx.intern_polytype($crate::Variable($n), $crate::ptp!($ctx, $($t)+)) }; - ($($t:tt)+) => { - $crate::TypeSchema::Monotype($crate::tp!($($t)+)) + ($ctx:ident, $($t:tt)+) => { + $ctx.intern_monotype($crate::tp!($ctx, $($t)+)) }; } diff --git a/src/parser.rs b/src/parser.rs index 037e905..5a79cf5 100644 --- a/src/parser.rs +++ b/src/parser.rs @@ -1,19 +1,16 @@ +use crate::{Name, Schema, Ty, TypeContext, Variable}; +#[allow(unused_imports)] +use nom::call; // FIXME see https://github.com/Geal/nom/pull/871 use nom::{alpha, digit, types::CompleteStr}; use nom::{ alt, alt_sep, call_m, do_parse, error_position, expr_res, map, map_res, method, opt, sep, separated_list, tag, wrap_sep, ws, }; - -#[allow(unused_imports)] -use nom::call; // FIXME see https://github.com/Geal/nom/pull/871 - -use std::marker::PhantomData; use std::num::ParseIntError; -use crate::{Name, Type, TypeSchema}; +pub struct Parser<'ctx, N: Name>(TypeContext<'ctx, N>); -#[derive(Debug)] -/// A failed parse. +#[derive(Copy, Clone, Debug, PartialEq, Eq, Hash)] pub struct ParseError; impl std::fmt::Display for ParseError { @@ -24,14 +21,20 @@ impl std::fmt::Display for ParseError { impl std::error::Error for ParseError {} -pub fn parse_type(input: &str) -> Result, ParseError> { - match Parser::default().monotype(CompleteStr(input)).1 { +pub fn parse_type<'ctx, N: Name>( + ctx: &TypeContext<'ctx, N>, + input: &str, +) -> Result, ParseError> { + match Parser::new(ctx.clone()).monotype(CompleteStr(input)).1 { Ok((_, t)) => Ok(t), _ => Err(ParseError), } } -pub fn parse_typeschema(input: &str) -> Result, ParseError> { - match Parser::default().polytype(CompleteStr(input)).1 { +pub fn parse_typeschema<'ctx, N: Name>( + ctx: &TypeContext<'ctx, N>, + input: &str, +) -> Result, ParseError> { + match Parser::new(ctx.clone()).polytype(CompleteStr(input)).1 { Ok((_, t)) => Ok(t), _ => Err(ParseError), } @@ -41,38 +44,38 @@ fn nom_usize(inp: CompleteStr<'_>) -> Result { inp.parse() } -// hack for polymorphism with nom -pub struct Parser(PhantomData); -impl Default for Parser { - fn default() -> Self { - Parser(PhantomData) +impl<'ctx, N: Name> Parser<'ctx, N> { + fn new(ctx: TypeContext<'ctx, N>) -> Self { + Parser(ctx) } } -impl Parser { +impl<'ctx, N: Name> Parser<'ctx, N> { method!( - var, CompleteStr<'_>, Type>, + var, CompleteStr<'_>, Ty<'ctx, N>>, self, - do_parse!(tag!("t") >> num: map_res!(digit, nom_usize) >> (Type::Variable(num))) + do_parse!( + tag!("t") >> num: map_res!(digit, nom_usize) >> (self.0.intern_tvar(Variable(num))) + ) ); method!( - constructed_simple, CompleteStr<'_>, Type>, + constructed_simple, CompleteStr<'_>, Ty<'ctx, N>>, self, do_parse!( name_raw: alpha - >> name: expr_res!(N::parse(&name_raw)) - >> (Type::Constructed(name, vec![])) + >> name: expr_res!(N::parse(&name_raw).map(|name| self.0.intern_name(name))) + >> (self.0.intern_tcon(name, self.0.intern_args(&[]))) ) ); - method!(constructed_complex, CompleteStr<'_>, Type>, mut self, + method!(constructed_complex, CompleteStr<'_>, Ty<'ctx, N>>, mut self, do_parse!( name_raw: alpha >> - name: expr_res!(N::parse(&name_raw)) >> + name: expr_res!(N::parse(&name_raw).map(|name| self.0.intern_name(name))) >> tag!("(") >> args: separated_list!(tag!(","), ws!(call_m!(self.monotype))) >> tag!(")") >> - (Type::Constructed(name, args))) + (self.0.intern_tcon(name, self.0.intern_args(&args)))) ); - method!(arrow, CompleteStr<'_>, Type>, mut self, + method!(arrow, CompleteStr<'_>, Ty<'ctx, N>>, mut self, do_parse!( alpha: ws!(alt!(call_m!(self.parenthetical) | call_m!(self.var) | @@ -80,89 +83,32 @@ impl Parser { call_m!(self.constructed_simple))) >> alt!(tag!("→") | tag!("->")) >> beta: ws!(call_m!(self.monotype)) >> - (Type::arrow(alpha, beta))) + (self.0.arrow(alpha, beta))) ); - method!(parenthetical, CompleteStr<'_>, Type>, mut self, + method!(parenthetical, CompleteStr<'_>, Ty<'ctx, N>>, mut self, do_parse!( tag!("(") >> interior: call_m!(self.arrow) >> tag!(")") >> (interior)) ); - method!(binding, CompleteStr<'_>, TypeSchema>, mut self, + method!(binding, CompleteStr<'_>, Schema<'ctx, N>>, mut self, do_parse!( opt!(tag!("∀")) >> tag!("t") >> variable: map_res!(digit, nom_usize) >> ws!(tag!(".")) >> - body: map!(call_m!(self.polytype), Box::new) >> - (TypeSchema::Polytype{variable, body})) + body: call_m!(self.polytype) >> + (self.0.intern_polytype(Variable(variable), body))) ); - method!(monotype, CompleteStr<'_>, Type>, mut self, + method!(monotype, CompleteStr<'_>, Ty<'ctx, N>>, mut self, alt!(call_m!(self.arrow) | call_m!(self.var) | call_m!(self.constructed_complex) | call_m!(self.constructed_simple)) ); - method!(polytype, CompleteStr<'_>, TypeSchema>, mut self, + method!(polytype, CompleteStr<'_>, Schema<'ctx, N>>, mut self, alt!(call_m!(self.binding) | - map!(call_m!(self.monotype), TypeSchema::Monotype)) + map!(call_m!(self.monotype), |t| self.0.intern_monotype(t))) ); } -impl TypeSchema { - /// Parse a [`TypeSchema`] from a string. This round-trips with [`Display`]. - /// This is a **leaky** operation and should be avoided wherever possible: - /// names of constructed types will remain until program termination. - /// - /// The "for-all" `∀` is optional. - /// - /// # Examples - /// - /// ``` - /// # use polytype::{ptp, tp, TypeSchema}; - /// let t_par = TypeSchema::parse("∀t0. t0 -> t0").expect("valid type"); - /// let t_lit = ptp!(0; @arrow[tp!(0), tp!(0)]); - /// assert_eq!(t_par, t_lit); - /// - /// let s = "∀t0. ∀t1. (t1 → t0 → t1) → t1 → list(t0) → t1"; - /// let t: TypeSchema<&'static str> = TypeSchema::parse(s).expect("valid type"); - /// let round_trip = t.to_string(); - /// assert_eq!(s, round_trip); - /// ``` - /// - /// [`Display`]: https://doc.rust-lang.org/std/fmt/trait.Display.html - /// [`TypeSchema`]: enum.TypeSchema.html - pub fn parse(s: &str) -> Result, ParseError> { - parse_typeschema(s) - } -} -impl Type { - /// Parse a type from a string. This round-trips with [`Display`]. This is a - /// **leaky** operation and should be avoided wherever possible: names of - /// constructed types will remain until program termination. - /// - /// # Examples - /// - /// ``` - /// # use polytype::{tp, Type}; - /// let t_par = Type::parse("int -> hashmap(str, list(bool))").expect("valid type"); - /// let t_lit = tp!(@arrow[ - /// tp!(int), - /// tp!(hashmap( - /// tp!(str), - /// tp!(list(tp!(bool))), - /// )), - /// ]); - /// assert_eq!(t_par, t_lit); - /// - /// let s = "(t1 → t0 → t1) → t1 → list(t0) → t1"; - /// let t: Type<&'static str> = Type::parse(s).expect("valid type"); - /// let round_trip = t.to_string(); - /// assert_eq!(s, round_trip); - /// ``` - /// - /// [`Display`]: https://doc.rust-lang.org/std/fmt/trait.Display.html - pub fn parse(s: &str) -> Result, ParseError> { - parse_type(s) - } -} diff --git a/src/source.rs b/src/source.rs new file mode 100644 index 0000000..776acbf --- /dev/null +++ b/src/source.rs @@ -0,0 +1,174 @@ +use crate::{Name, Schema, Ty, Type, TypeContext, TypeSchema, Variable}; + +/// A way to generate fresh [`Variable`]s. +/// +/// [`Variable`]: struct.Variable.html +#[derive(Copy, Clone, Debug, PartialEq, Eq, Hash)] +pub struct Source(pub(crate) usize); + +/// Allow types to be reified for use under a different [`Source`]. +/// +/// [`Source`]: struct.Source.html +pub struct SourceChange { + pub(crate) delta: usize, + pub(crate) sacreds: Vec, +} + +impl Source { + /// Get a fresh bare [`Variable`]. + /// + /// # Examples + /// + /// ``` + /// # use polytype::{tp, with_ctx, Source, TypeContext}; + /// with_ctx(32, |ctx: TypeContext<'_>| { + /// let mut src = Source::default(); + /// assert_eq!(src.fresh(), 0); + /// assert_eq!(src.fresh(), 1); + /// assert_eq!(src.fresh(), 2); + /// }); + /// ``` + /// + /// [`Variable`]: type.Variable.html + pub fn fresh(&mut self) -> usize { + let var = self.0; + self.0 += 1; + var + } + /// Combine two `Source`s. + /// + /// This merges `other` into `self` and produces a [`SourceChange`], which + /// can be used to transform the values produced by `other` to be consistent + /// with the state of `self` after the merge. Values passed in as `sacreds` + /// are considered to be shared between the two `Source`s. + /// + /// # Examples + /// + /// ``` + /// # use polytype::{tp, with_ctx, Source, TypeContext, Variable}; + /// with_ctx(32, |ctx: TypeContext<'_>| { + /// let mut src_1 = Source::default(); + /// src_1.fresh(); + /// src_1.fresh(); + /// let mut src_2 = Source::default(); + /// src_2.fresh(); + /// src_2.fresh(); + /// let change = src_1.merge(src_2, vec![Variable(1)]); + /// assert_eq!(src_1.fresh(), 4); + /// + /// let t_original = tp!(ctx, @arrow[tp!(ctx, 0), tp!(ctx, 1)]); + /// assert_eq!(t_original.to_string(), "t0 → t1"); + /// + /// let t_reified = change.reify_type(t_original, &ctx); + /// assert_eq!(t_reified.to_string(), "t2 → t1"); + /// }); + /// ``` + /// + /// [`Variable`]: type.Variable.html + pub fn merge(&mut self, other: Self, sacreds: Vec) -> SourceChange { + let delta = self.0; + // this is intentionally wasting variable space when there are sacreds: + self.0 += other.0; + SourceChange { delta, sacreds } + } +} + +impl Default for Source { + fn default() -> Self { + Source(0) + } +} + +impl SourceChange { + /// Reify a [`Ty`] for use under a new [`Source`]. + /// + /// # Examples + /// + /// ``` + /// # use polytype::{tp, with_ctx, Source, TypeContext, Variable}; + /// with_ctx(32, |ctx: TypeContext<'_>| { + /// let mut src_1 = Source::default(); + /// src_1.fresh(); + /// src_1.fresh(); + /// let mut src_2 = Source::default(); + /// src_2.fresh(); + /// src_2.fresh(); + /// let change = src_1.merge(src_2, vec![Variable(1)]); + /// assert_eq!(src_1.fresh(), 4); + /// + /// let t_original = tp!(ctx, @arrow[tp!(ctx, 0), tp!(ctx, 1)]); + /// assert_eq!(t_original.to_string(), "t0 → t1"); + /// + /// let t_reified = change.reify_type(t_original, &ctx); + /// assert_eq!(t_reified.to_string(), "t2 → t1"); + /// }); + /// ``` + /// + /// [`Source`]: struct.Source.html + /// [`Ty`]: type.Ty.html + pub fn reify_type<'ctx, N: Name>( + &self, + tp: Ty<'ctx, N>, + ctx: &TypeContext<'ctx, N>, + ) -> Ty<'ctx, N> { + match *tp { + Type::Constructed(head, args) => { + let mut new_args = Vec::with_capacity(args.len()); + for arg in args { + new_args.push(self.reify_type(arg, ctx)); + } + let new_args = ctx.intern_args(&new_args); + ctx.intern_tcon(head, new_args) + } + Type::Variable(n) if self.sacreds.contains(&n) => tp, + Type::Variable(n) => ctx.intern_tvar(Variable(n.0 + self.delta)), + } + } + /// Reify a [`TypeSchema`] for use under a new [`Source`]. + /// + /// # Examples + /// + /// ``` + /// # use polytype::{ptp, tp, with_ctx, Source, TypeContext, Variable}; + /// with_ctx(32, |ctx: TypeContext<'_>| { + /// let mut src_1 = Source::default(); + /// src_1.fresh(); + /// src_1.fresh(); + /// src_1.fresh(); + /// + /// let mut src_2 = Source::default(); + /// src_2.fresh(); + /// src_2.fresh(); + /// src_2.fresh(); + /// + /// let change = src_1.merge(src_2, vec![Variable(1)]); + /// assert_eq!(src_1.fresh(), 6); + /// + /// let s_original = ptp!(ctx, 0, @arrow[ + /// tp!(ctx, @arrow[tp!(ctx, 0), tp!(ctx, 1)]), + /// tp!(ctx, @arrow[tp!(ctx, 2), tp!(ctx, 1)]) + /// ]); + /// assert_eq!(s_original.to_string(), "∀t0. (t0 → t1) → t2 → t1"); + /// + /// let s_reified = change.reify_typeschema(s_original, &ctx); + /// assert_eq!(s_reified.to_string(), "∀t3. (t3 → t1) → t5 → t1"); + /// }); + /// ``` + /// + /// [`Schema`]: type.Schema.html + /// [`Source`]: struct.Source.html + pub fn reify_typeschema<'ctx, N: Name>( + &self, + schema: Schema<'ctx, N>, + ctx: &TypeContext<'ctx, N>, + ) -> Schema<'ctx, N> { + match schema { + TypeSchema::Monotype(inner) => ctx.intern_monotype(self.reify_type(inner, ctx)), + TypeSchema::Polytype(variable, body) => { + let t_var = Variable(variable.0 + self.delta); + let new_body = self.reify_typeschema(body, ctx); + ctx.intern_polytype(t_var, new_body) + } + } + } +} diff --git a/src/substitution.rs b/src/substitution.rs new file mode 100644 index 0000000..a81e3ee --- /dev/null +++ b/src/substitution.rs @@ -0,0 +1,274 @@ +use crate::{Name, Ty, TypeContext, Variable}; + +#[derive(Copy, Clone, Debug, PartialEq, Eq)] +/// A way to mark the current state of a [`Substitution`] such that it can be later restored. +/// +/// [`Substitution`]: struct.Substitution.html +pub struct Snapshot(usize); + +#[derive(Clone, Debug, PartialEq, Eq)] +/// A mapping from [`Variable`]s to [`Ty`]s indicating that each [`Variable`] +/// can be substituted for the corresponding [`Ty`]. +/// +/// [`Variable`]: struct.Variable.html +/// [`Ty`]: type.Ty.html +pub struct Substitution<'ctx, N: Name = &'static str> { + /// The `TypeContext` in which typing takes place. + pub(crate) ctx: TypeContext<'ctx, N>, + /// The `Variable` to `Ty` map. + pub(crate) sub: Vec<(Variable, Ty<'ctx, N>)>, +} + +pub struct SubIter<'a, 'ctx, N: Name = &'static str> { + it: std::slice::Iter<'a, (Variable, Ty<'ctx, N>)>, +} +pub struct SubIterMut<'a, 'ctx, N: Name = &'static str> { + it: std::slice::IterMut<'a, (Variable, Ty<'ctx, N>)>, +} + +impl<'ctx, N: Name> Substitution<'ctx, N> { + /// Construct an empty `Substitution` with at least capacity for `n` mappings. + /// + /// # Examples + /// + /// ``` + /// # use polytype::{tp, with_ctx, Substitution, TypeContext}; + /// with_ctx(32, |ctx: TypeContext<'_>| { + /// let mut sub = Substitution::with_capacity(ctx, 10); + /// assert_eq!(sub.len(), 0); + /// }); + /// ``` + pub fn with_capacity(ctx: TypeContext<'ctx, N>, n: usize) -> Self { + Substitution { + ctx, + sub: Vec::with_capacity(n), + } + } + /// Optionally retrieve the [`Ty`] associated with some variable. + /// + /// # Examples + /// + /// ``` + /// # use polytype::{tp, with_ctx, Substitution, Variable, Type}; + /// with_ctx(32, |ctx| { + /// let mut sub = Substitution::with_capacity(ctx, 10); + /// sub.add(Variable(0), tp!(ctx, int)); + /// assert_eq!( sub.get(Variable(0)), Some(tp!(ctx, int))); + /// assert_eq!(sub.get(Variable(1)), None) + /// }); + /// ``` + pub fn get(&self, q: Variable) -> Option> { + self.sub.iter().find(|(k, _)| *k == q).map(|(_, v)| *v) + } + /// Insert a new mapping into the `Substitution` unless it conflicts with an + /// existing mapping. + /// + /// The return value indicates whether the insertion was successful. + /// + /// # Examples + /// + /// ``` + /// # use polytype::{tp, with_ctx, Substitution, TypeContext, Variable}; + /// with_ctx(32, |ctx| { + /// let mut sub = Substitution::with_capacity(ctx, 10); + /// assert_eq!(sub.len(), 0); + /// let added = sub.add(Variable(0), tp!(ctx, int)); + /// assert!(added); + /// assert_eq!(sub.len(), 1); + /// let added = sub.add(Variable(0), tp!(ctx, bool)); + /// assert!(!added); + /// assert_eq!(sub.len(), 1); + /// }); + /// ``` + pub fn add(&mut self, k: Variable, v: Ty<'ctx, N>) -> bool { + if self.sub.iter().any(|(j, _)| k == *j) { + false + } else { + self.sub.push((k, v)); + true + } + } + /// The `Substitution` as a slice. + /// + /// # Examples + /// + /// ``` + /// # use polytype::{tp, with_ctx, Substitution, TypeContext, Variable}; + /// with_ctx(32, |ctx| { + /// let mut sub = Substitution::with_capacity(ctx, 10); + /// sub.add(Variable(0), tp!(ctx, int)); + /// sub.add(Variable(1), tp!(ctx, bool)); + /// let slice = sub.as_slice(); + /// assert_eq!(slice.len(), 2); + /// assert_eq!(slice[0], (Variable(0), tp!(ctx, int))); + /// assert_eq!(slice[1], (Variable(1), tp!(ctx, bool))); + /// }); + /// ``` + pub fn as_slice(&self) -> &[(Variable, Ty<'ctx, N>)] { + &self.sub + } + /// An Iterator over the `Substitution`. + /// + /// # Examples + /// + /// ``` + /// # use polytype::{tp, with_ctx, Substitution, TypeContext, Variable}; + /// with_ctx(32, |ctx| { + /// let mut sub = Substitution::with_capacity(ctx, 10); + /// sub.add(Variable(0), tp!(ctx, int)); + /// sub.add(Variable(1), tp!(ctx, bool)); + /// sub.add(Variable(2), tp!(ctx, bool)); + /// sub.add(Variable(3), tp!(ctx, char)); + /// sub.add(Variable(4), tp!(ctx, bool)); + /// assert_eq!(sub.iter().filter(|(v, t)| *t == tp!(ctx, bool)).count(), 3); + /// }); + /// ``` + pub fn iter<'a>(&'a self) -> SubIter<'a, 'ctx, N> { + SubIter { + it: self.sub.iter(), + } + } + /// A mutable Iterator over the `Substitution`. + /// + /// # Examples + /// + /// ``` + /// # use polytype::{tp, with_ctx, Substitution, TypeContext, Variable}; + /// with_ctx(32, |ctx| { + /// let mut sub = Substitution::with_capacity(ctx, 10); + /// sub.add(Variable(0), tp!(ctx, int)); + /// sub.add(Variable(1), tp!(ctx, bool)); + /// sub.add(Variable(2), tp!(ctx, bool)); + /// sub.add(Variable(3), tp!(ctx, char)); + /// sub.add(Variable(4), tp!(ctx, bool)); + /// assert_eq!(sub.iter().filter(|(v, t)| *t == tp!(ctx, bool)).count(), 3); + /// for (v, t) in sub.iter_mut() { + /// *t = tp!(ctx, bool); + /// } + /// assert_eq!(sub.iter().filter(|(v, t)| *t == tp!(ctx, bool)).count(), 5); + /// }); + /// ``` + pub fn iter_mut<'a>(&'a mut self) -> SubIterMut<'a, 'ctx, N> { + SubIterMut { + it: self.sub.iter_mut(), + } + } + /// The number of constraints in the `Substitution`. + /// + /// # Examples + /// + /// ``` + /// # use polytype::{tp, with_ctx, Substitution, TypeContext, Variable}; + /// with_ctx(32, |ctx| { + /// let mut sub = Substitution::with_capacity(ctx, 10); + /// sub.add(Variable(0), tp!(ctx, int)); + /// sub.add(Variable(1), tp!(ctx, bool)); + /// sub.add(Variable(2), tp!(ctx, float)); + /// sub.add(Variable(3), tp!(ctx, char)); + /// sub.add(Variable(4), tp!(ctx, string)); + /// assert_eq!(sub.len(), 5); + /// }); + /// ``` + pub fn len(&self) -> usize { + self.sub.len() + } + /// `true` if the `Substitution` has any constraints, else `false`. + /// + /// # Examples + /// + /// ``` + /// # use polytype::{tp, with_ctx, Substitution, TypeContext, Variable}; + /// with_ctx(32, |ctx| { + /// let mut sub = Substitution::with_capacity(ctx, 10); + /// assert!(sub.is_empty()); + /// sub.add(Variable(0), tp!(ctx, int)); + /// assert!(!sub.is_empty()); + /// }); + /// ``` + pub fn is_empty(&self) -> bool { + self.sub.is_empty() + } + /// Clears the substitution managed by the context. + /// + /// # Examples + /// + /// ``` + /// # use polytype::{tp, with_ctx, Substitution, TypeContext, Variable}; + /// with_ctx(10, |ctx: TypeContext<'_>| { + /// let mut sub = Substitution::with_capacity(ctx, 1); + /// + /// let clean = sub.clone(); + /// + /// sub.add(Variable(0), tp!(ctx, int)); + /// let dirty = sub.clone(); + /// + /// sub.clean(); + /// + /// assert_eq!(clean, sub); + /// assert_ne!(clean, dirty); + /// }) + /// ``` + pub fn clean(&mut self) { + self.sub.clear(); + } + /// Creates a `Snapshot` to which the `Substitution` can be rolled back. + /// + /// # Examples + /// + /// ``` + /// # use polytype::{tp, with_ctx, Snapshot, Substitution, TypeContext, Variable}; + /// with_ctx(10, |ctx: TypeContext<'_>| { + /// let mut sub = Substitution::with_capacity(ctx, 5); + /// sub.add(Variable(0), tp!(ctx, int)); + /// sub.add(Variable(1), tp!(ctx, bool)); + /// sub.add(Variable(2), tp!(ctx, char)); + /// let snapshot = sub.snapshot(); + /// assert_eq!(sub.len(), 3); + /// sub.add(Variable(3), tp!(ctx, bool)); + /// sub.add(Variable(4), tp!(ctx, char)); + /// assert_eq!(sub.len(), 5); + /// sub.rollback(snapshot); + /// assert_eq!(sub.len(), 3); + /// }) + /// ``` + pub fn snapshot(&self) -> Snapshot { + Snapshot(self.len()) + } + /// Removes all substitutions added to the `Substitution` since the supplied `Snapshot`. + /// + /// # Examples + /// + /// ``` + /// # use polytype::{tp, with_ctx, Snapshot, Substitution, TypeContext, Variable}; + /// with_ctx(10, |ctx: TypeContext<'_>| { + /// let mut sub = Substitution::with_capacity(ctx, 5); + /// sub.add(Variable(0), tp!(ctx, int)); + /// sub.add(Variable(1), tp!(ctx, bool)); + /// sub.add(Variable(2), tp!(ctx, char)); + /// let snapshot = sub.snapshot(); + /// assert_eq!(sub.len(), 3); + /// sub.add(Variable(3), tp!(ctx, bool)); + /// sub.add(Variable(4), tp!(ctx, char)); + /// assert_eq!(sub.len(), 5); + /// sub.rollback(snapshot); + /// assert_eq!(sub.len(), 3); + /// }) + /// ``` + pub fn rollback(&mut self, Snapshot(n): Snapshot) { + self.sub.truncate(n) + } +} + +impl<'a, 'ctx, N: Name> Iterator for SubIter<'a, 'ctx, N> { + type Item = &'a (Variable, Ty<'ctx, N>); + fn next(&mut self) -> Option { + self.it.next() + } +} + +impl<'a, 'ctx, N: Name> Iterator for SubIterMut<'a, 'ctx, N> { + type Item = &'a mut (Variable, Ty<'ctx, N>); + fn next(&mut self) -> Option { + self.it.next() + } +} diff --git a/src/types.rs b/src/types.rs index 97fb466..a38c5a4 100644 --- a/src/types.rs +++ b/src/types.rs @@ -1,284 +1,117 @@ +use crate::{ + parser::{parse_type, parse_typeschema, ParseError}, + Name, Source, Substitution, TypeContext, +}; use itertools::Itertools; -use std::collections::{HashMap, VecDeque}; -use std::fmt; +use smallvec::{smallvec, SmallVec}; +use std::{error::Error, fmt}; -use crate::{Context, Name}; - -/// Represents a [type variable][1] (an unknown type). -/// -/// [1]: https://en.wikipedia.org/wiki/Hindley–Milner_type_system#Free_type_variables -pub type Variable = usize; - -/// Represents [polytypes][1] (uninstantiated, universally quantified types). +/// The primary way [`Type`]s are handled. This is what a [`TypeContext`] returns when interning a [`Type`]. /// -/// The primary ways of creating a `TypeSchema` are with the [`ptp!`] macro or -/// with [`Type::generalize`]. +/// [`Type`]: enum.Type.html +/// [`TypeContext`]: struct.TypeContext.html +pub type Ty<'ctx, N = &'static str> = &'ctx Type<'ctx, N>; +/// The primary way [`TypeSchema`]s are handled. This is what a [`TypeContext`] returns when interning a [`TypeSchema`]. /// -/// [1]: https://en.wikipedia.org/wiki/Hindley–Milner_type_system#Polytype -/// [`ptp!`]: macro.ptp.html -/// [`Type::generalize`]: enum.Type.html#method.generalize -#[derive(Debug, Clone, Hash, PartialEq, Eq)] -pub enum TypeSchema { - /// Non-polymorphic types (e.g. `α → β`, `int → bool`) - Monotype(Type), - /// Polymorphic types (e.g. `∀α. α → α`, `∀α. ∀β. α → β`) - Polytype { - /// The [`Variable`] being bound - /// - /// [`Variable`]: type.Variable.html - variable: Variable, - /// The type in which `variable` is bound - body: Box>, - }, -} -impl TypeSchema { - /// Checks whether a variable is bound in the quantification of a polytype. - /// - /// # Examples - /// - /// ``` - /// # use polytype::{ptp, tp}; - /// let t = ptp!(0; @arrow[tp!(0), tp!(1)]); // ∀α. α → β - /// assert!(t.is_bound(0)); - /// assert!(!t.is_bound(1)); - /// ``` - pub fn is_bound(&self, v: Variable) -> bool { - match *self { - TypeSchema::Monotype(_) => false, - TypeSchema::Polytype { variable, .. } if variable == v => true, - TypeSchema::Polytype { ref body, .. } => body.is_bound(v), - } - } - /// Returns a set of each [`Variable`] bound by the [`TypeSchema`]. - /// - /// # Examples - /// - /// ``` - /// # use polytype::{ptp, tp}; - /// let t = ptp!(0, 1; @arrow[tp!(1), tp!(2), tp!(3)]); // ∀α. ∀β. β → ɣ → δ - /// assert_eq!(t.bound_vars(), vec![0, 1]); - /// ``` - /// - /// [`Variable`]: type.Variable.html - /// [`TypeSchema`]: enum.TypeSchema.html - pub fn bound_vars(&self) -> Vec { - let mut t = self; - let mut bvs = Vec::new(); - while let TypeSchema::Polytype { variable, ref body } = *t { - bvs.push(variable); - t = body - } - bvs - } - /// Returns a set of each free [`Variable`] in the [`TypeSchema`]. +/// [`TypeSchema`]: enum.TypeSchema.html +/// [`TypeContext`]: struct.TypeContext.html +pub type Schema<'ctx, N = &'static str> = &'ctx TypeSchema<'ctx, N>; + +#[derive(Debug, Copy, Clone, Hash, PartialEq, Eq, PartialOrd, Ord)] +/// A type variable representing a definite but unknown type (e.g. `t0`). +pub struct Variable(pub usize); + +/// Errors during unification. +#[derive(Debug, Clone, PartialEq)] +pub enum UnificationError<'ctx, N: Name = &'static str> { + /// `Occurs` happens when occurs checks fail (i.e. a type variable is + /// unified recursively). The id of the bad type variable is supplied. /// /// # Examples /// /// ``` - /// # use polytype::{ptp, tp}; - /// let t = ptp!(0, 1; @arrow[tp!(1), tp!(2), tp!(3)]); // ∀α. ∀β. β → ɣ → δ - /// let mut free = t.free_vars(); - /// free.sort(); - /// assert_eq!(free, vec![2, 3]); + /// # use polytype::{tp, ptp, with_ctx, Type, UnificationError, Variable}; + /// with_ctx(10, |ctx| { + /// let t_1 = tp!(ctx, 0); + /// let t_2 = tp!(ctx, list(tp!(ctx, 0))); + /// assert_eq!(Type::unify(&[(t_1, t_2)], &ctx), Err(UnificationError::Occurs(Variable(0)))); + /// }) /// ``` - /// [`Variable`]: type.Variable.html - /// [`TypeSchema`]: enum.TypeSchema.html - pub fn free_vars(&self) -> Vec { - let mut vars = vec![]; - self.free_vars_internal(&mut vars); - vars.sort_unstable(); - vars.dedup(); - vars - } - fn free_vars_internal(&self, vars: &mut Vec) { - match *self { - TypeSchema::Monotype(ref t) => t.vars_internal(vars), - TypeSchema::Polytype { variable, ref body } => { - body.free_vars_internal(vars); - *vars = vars.iter().filter(|&v| v != &variable).cloned().collect(); - } - } - } - /// Instantiate a [`TypeSchema`] in the context by removing quantifiers. - /// - /// All type variables will be replaced with fresh type variables. + Occurs(Variable), + /// `Mismatch` happens when symbols or type variants don't unify because of + /// structural differences. /// /// # Examples /// /// ``` - /// # use polytype::{ptp, tp, Context}; - /// let mut ctx = Context::default(); - /// - /// let t1 = ptp!(3; list(tp!(3))); - /// let t2 = ptp!(3; list(tp!(3))); - /// - /// let t1 = t1.instantiate(&mut ctx); - /// let t2 = t2.instantiate(&mut ctx); - /// assert_eq!(t1.to_string(), "list(t0)"); - /// assert_eq!(t2.to_string(), "list(t1)"); + /// # use polytype::{tp, ptp, with_ctx, Type, UnificationError}; + /// with_ctx(10, |ctx| { + /// let t_1 = tp!(ctx, set(tp!(ctx, 0))); + /// let t_2 = tp!(ctx, list(tp!(ctx, 0))); + /// assert_eq!(Type::unify(&[(t_1, t_2)], &ctx), Err(UnificationError::Mismatch(t_1, t_2))); + /// }) /// ``` - /// - /// [`TypeSchema`]: enum.TypeSchema.html - pub fn instantiate(&self, ctx: &mut Context) -> Type { - self.instantiate_internal(ctx, &mut HashMap::new()) - } - fn instantiate_internal( - &self, - ctx: &mut Context, - substitution: &mut HashMap>, - ) -> Type { + Mismatch(Ty<'ctx, N>, Ty<'ctx, N>), +} +impl<'ctx, N: Name> fmt::Display for UnificationError<'ctx, N> { + fn fmt(&self, f: &mut fmt::Formatter<'_>) -> Result<(), fmt::Error> { match *self { - TypeSchema::Monotype(ref t) => t.substitute(substitution), - TypeSchema::Polytype { variable, ref body } => { - substitution.insert(variable, ctx.new_variable()); - body.instantiate_internal(ctx, substitution) - } - } - } - /// Like [`instantiate`], but works in-place. - /// - /// [`instantiate`]: #method.instantiate - pub fn instantiate_owned(self, ctx: &mut Context) -> Type { - self.instantiate_owned_internal(ctx, &mut HashMap::new()) - } - fn instantiate_owned_internal( - self, - ctx: &mut Context, - substitution: &mut HashMap>, - ) -> Type { - match self { - TypeSchema::Monotype(mut t) => { - t.substitute_mut(substitution); - t - } - TypeSchema::Polytype { variable, body } => { - substitution.insert(variable, ctx.new_variable()); - body.instantiate_owned_internal(ctx, substitution) + UnificationError::Occurs(v) => write!(f, "Occurs({})", v.0), + UnificationError::Mismatch(ref t1, ref t2) => { + write!(f, "Mismatch({}, {})", t1.show(false), t2.show(false)) } } } } -impl fmt::Display for TypeSchema { - fn fmt(&self, f: &mut fmt::Formatter<'_>) -> Result<(), fmt::Error> { - match *self { - TypeSchema::Polytype { variable, ref body } => write!(f, "∀t{}. {}", variable, body), - TypeSchema::Monotype(ref t) => t.fmt(f), - } +impl<'ctx, N: Name + fmt::Debug> Error for UnificationError<'ctx, N> { + fn description(&self) -> &'static str { + "unification failed" } } -/// Represents [monotypes][1] (fully instantiated, unquantified types). -/// -/// The primary ways to create a `Type` are with either the [`tp!`] macro or -/// [`TypeSchema::instantiate`]. [`Type::arrow`] constructs function types (i.e. `α → β`), as does -/// conversion (`Type::from`) with `Vec` and `VecDeque` for curried arrows. -/// -/// [`tp!`]: macro.tp.html -/// [`TypeSchema::instantiate`]: enum.TypeSchema.html#method.instantiate -/// [`Type::arrow`]: enum.TypeSchema.html#method.instantiate -/// [1]: https://en.wikipedia.org/wiki/Hindley–Milner_type_system#Monotypes -#[derive(Debug, Clone, Hash, PartialEq, Eq)] -pub enum Type { +#[derive(Debug, Clone, PartialEq, Eq, Hash)] +/// A simple unquantified type. +pub enum Type<'ctx, N: Name = &'static str> { /// Primitive or composite types (e.g. `int`, `List(α)`, `α → β`) /// - /// # Examples - /// - /// Primitives have no associated types: - /// - /// ``` - /// # use polytype::Type; - /// let tint = Type::Constructed("int", vec![]); - /// assert_eq!(tint.to_string(), "int") - /// ``` - /// - /// Composites have associated types: - /// - /// ``` - /// # use polytype::Type; - /// let tint = Type::Constructed("int", vec![]); - /// let tlist_of_ints = Type::Constructed("list", vec![tint]); - /// assert_eq!(tlist_of_ints.to_string(), "list(int)"); - /// ``` - /// - /// With the macro: - /// - /// ``` - /// # use polytype::tp; - /// let t = tp!(list(tp!(int))); - /// assert_eq!(t.to_string(), "list(int)"); - /// ``` - /// - /// Function types, or "arrows", are constructed with either [`Type::arrow`], two - /// implementations of `Type::from` — one for [`Vec`] and one for [`VecDeque`] — or - /// the macro: - /// - /// ``` - /// # use polytype::{tp, Type}; - /// let t = Type::arrow(tp!(int), tp!(bool)); - /// assert_eq!(t.to_string(), "int → bool"); - /// - /// let t = Type::from(vec![tp!(int), tp!(int), tp!(bool)]); - /// assert_eq!(t.to_string(), "int → int → bool"); - /// - /// let t = tp!(@arrow[tp!(int), tp!(int), tp!(bool)]); // prefer this over Type::from - /// assert_eq!(t.to_string(), "int → int → bool"); - /// ``` - /// - /// [`Type::arrow`]: enum.Type.html#method.arrow - /// [`Vec`]: enum.Type.html#impl-From>> - /// [`VecDeque`]: enum.Type.html#impl-From>> - Constructed(N, Vec>), + /// For some `Type::Constructed(head, args)`: + /// - `head` is the type constructor. + /// - `args` are the arguments to `head`. + Constructed(&'ctx N, &'ctx [Ty<'ctx, N>]), /// Type variables (e.g. `α`, `β`). - /// - /// # Examples - /// - /// ``` - /// # use polytype::{tp, Type}; - /// // any function: α → β - /// let t = tp!(@arrow[Type::Variable(0), Type::Variable(1)]); - /// assert_eq!(t.to_string(), "t0 → t1"); - /// ``` - /// - /// With the macro: - /// - /// ``` - /// # use polytype::tp; - /// // map: (α → β) → [α] → [β] - /// let t = tp!(@arrow[ - /// tp!(@arrow[tp!(0), tp!(1)]), - /// tp!(list(tp!(0))), - /// tp!(list(tp!(1))), - /// ]); - /// assert_eq!(t.to_string(), "(t0 → t1) → list(t0) → list(t1)"); - /// ``` Variable(Variable), } -impl Type { - /// Construct a function type (i.e. `alpha` → `beta`). + +#[derive(Debug, Clone, PartialEq, Eq, Hash)] +/// A potentially quantified (i.e. parametrically polymorphic) type. +pub enum TypeSchema<'ctx, N: Name = &'static str> { + /// Non-polymorphic types (e.g. `α → β`, `int → bool`) + Monotype(Ty<'ctx, N>), + /// Polymorphic types (e.g. `∀α. α → α`, `∀α. ∀β. α → β`) /// - /// # Examples + /// For some `TypeSchema::Polytype(variable, body)`: + /// - `variable` is the [`Variable`] being bound. + /// - `body` is the type in which `variable` is bound. /// - /// ``` - /// # use polytype::{tp, Type}; - /// let t = Type::arrow(tp!(int), tp!(bool)); - /// assert_eq!(t.to_string(), "int → bool"); - /// ``` - pub fn arrow(alpha: Type, beta: Type) -> Type { - Type::Constructed(N::arrow(), vec![alpha, beta]) - } + /// [`Variable`]: type.Variable.html + Polytype(Variable, Schema<'ctx, N>), +} + +impl<'ctx, N: Name> Type<'ctx, N> { /// If the type is an arrow, get its associated argument and return types. /// /// # Examples /// /// ``` - /// # use polytype::{ptp, tp}; - /// let t = tp!(@arrow[tp!(int), tp!(int), tp!(bool)]); - /// if let Some((left, right)) = t.as_arrow() { - /// assert_eq!(left.to_string(), "int"); + /// # use polytype::{tp, with_ctx, TypeContext}; + /// with_ctx(10, |ctx| { + /// let t = tp!(ctx, @arrow[tp!(ctx, char), tp!(ctx, int), tp!(ctx, bool)]); + /// let (left, right) = t.as_arrow().expect("broken arrow"); + /// assert_eq!(left.to_string(), "char"); /// assert_eq!(right.to_string(), "int → bool"); - /// } else { unreachable!() } + /// }) /// ``` - pub fn as_arrow(&self) -> Option<(&Type, &Type)> { + pub fn as_arrow(&self) -> Option<(Ty<'ctx, N>, Ty<'ctx, N>)> { match *self { Type::Constructed(ref n, ref args) if n.is_arrow() => Some((&args[0], &args[1])), _ => None, @@ -286,15 +119,15 @@ impl Type { } pub(crate) fn occurs(&self, v: Variable) -> bool { match *self { - Type::Constructed(_, ref args) => args.iter().any(|t| t.occurs(v)), + Type::Constructed(_, args) => args.iter().any(|t| t.occurs(v)), Type::Variable(n) => n == v, } } /// Supplying `is_return` helps arrows look cleaner. pub(crate) fn show(&self, is_return: bool) -> String { match *self { - Type::Variable(v) => format!("t{}", v), - Type::Constructed(ref name, ref args) => { + Type::Variable(v) => format!("t{}", v.0), + Type::Constructed(name, args) => { if args.is_empty() { name.show() } else if name.is_arrow() { @@ -310,7 +143,7 @@ impl Type { } } /// Show specifically for arrow types - fn arrow_show(args: &[Type], is_return: bool) -> String { + fn arrow_show(args: &[Ty<'ctx, N>], is_return: bool) -> String { if is_return { format!("{} → {}", args[0].show(false), args[1].show(true)) } else { @@ -322,24 +155,27 @@ impl Type { /// # Examples /// /// ``` - /// # use polytype::tp; - /// let t = tp!(@arrow[tp!(int), tp!(int), tp!(bool)]); - /// if let Some(args) = t.args() { + /// # use polytype::{tp, with_ctx, TypeContext}; + /// with_ctx(10, |ctx: TypeContext<'_>| { + /// let t = tp!(ctx, @arrow[tp!(ctx, char), tp!(ctx, int), tp!(ctx, bool)]); + /// let args = t.args().expect("arguments"); /// assert_eq!(args.len(), 2); - /// assert_eq!(args[0].to_string(), "int"); + /// assert_eq!(args[0].to_string(), "char"); /// assert_eq!(args[1].to_string(), "int"); - /// } else { unreachable!() } + /// }) /// ``` - pub fn args(&self) -> Option>> { + // TODO: convert Type::args to an iterator + // TODO: convert TypeContext::intern_args to take an iterator + pub fn args(&self) -> Option>> { match *self { - Type::Constructed(ref n, ref args) if n.is_arrow() => { - let mut tps = VecDeque::with_capacity(1); - tps.push_back(&args[0]); + Type::Constructed(n, args) if n.is_arrow() => { + let mut tps: Vec> = Vec::with_capacity(10); + tps.push(&args[0]); let mut tp = &args[1]; loop { match *tp { - Type::Constructed(ref n, ref args) if n.is_arrow() => { - tps.push_back(&args[0]); + Type::Constructed(n, args) if n.is_arrow() => { + tps.push(&args[0]); tp = &args[1]; } _ => break, @@ -350,45 +186,25 @@ impl Type { _ => None, } } - /// If the type is an arrow, recursively get all curried function arguments. - pub fn args_destruct(self) -> Option>> { - match self { - Type::Constructed(n, mut args) if n.is_arrow() => { - let mut tps = Vec::with_capacity(1); - let mut tp = args.pop().unwrap(); - tps.push(args.pop().unwrap()); - loop { - match tp { - Type::Constructed(n, mut args) if n.is_arrow() => { - tp = args.pop().unwrap(); - tps.push(args.pop().unwrap()); - } - _ => break, - } - } - Some(tps) - } - _ => None, - } - } /// If the type is an arrow, get its ultimate return type. /// /// # Examples /// /// ``` - /// # use polytype::tp; - /// let t = tp!(@arrow[tp!(int), tp!(int), tp!(bool)]); - /// if let Some(ret) = t.returns() { + /// # use polytype::{tp, with_ctx, TypeContext}; + /// with_ctx(10, |ctx: TypeContext<'_>| { + /// let t = tp!(ctx, @arrow[tp!(ctx, char), tp!(ctx, int), tp!(ctx, bool)]); + /// let ret = t.returns().expect("return type"); /// assert_eq!(ret.to_string(), "bool"); - /// } else { unreachable!() } + /// }) /// ``` - pub fn returns(&self) -> Option<&Type> { + pub fn returns(&self) -> Option> { match *self { - Type::Constructed(ref n, ref args) if n.is_arrow() => { + Type::Constructed(n, args) if n.is_arrow() => { let mut tp = &args[1]; loop { match *tp { - Type::Constructed(ref n, ref args) if n.is_arrow() => { + Type::Constructed(n, args) if n.is_arrow() => { tp = &args[1]; } _ => break, @@ -407,71 +223,34 @@ impl Type { /// # Examples /// /// ``` - /// # use polytype::{tp, Context}; - /// let mut ctx = Context::default(); - /// ctx.unify(&tp!(0), &tp!(int)).expect("unifies"); + /// # use polytype::{tp, with_ctx, Substitution, TypeContext, Type, Variable}; + /// with_ctx(10, |ctx: TypeContext<'_>| { + /// let t_0 = tp!(ctx, 0); + /// let t_int = tp!(ctx, int); + /// let t_list_0 = tp!(ctx, list(t_0)); + /// + /// let sub = Type::unify(&[(t_0, t_int)], &ctx).expect("unifies"); /// - /// let t = tp!(list(tp!(0))); - /// assert_eq!(t.to_string(), "list(t0)"); - /// let t = t.apply(&ctx); - /// assert_eq!(t.to_string(), "list(int)"); + /// assert_eq!(t_list_0.to_string(), "list(t0)"); + /// + /// let t_list_int = t_list_0.apply(&sub); + /// assert_eq!(t_list_int.to_string(), "list(int)"); + /// }) /// ``` /// /// [`Context`]: struct.Context.html - pub fn apply(&self, ctx: &Context) -> Type { - match *self { - Type::Constructed(ref name, ref args) => { - let args = args.iter().map(|t| t.apply(ctx)).collect(); - Type::Constructed(name.clone(), args) - } - Type::Variable(v) => { - let maybe_tp = ctx - .path_compression_cache - .borrow() - .get(&v) - .or_else(|| ctx.substitution.get(&v)) - .cloned(); - maybe_tp - .map(|mut tp| { - tp.apply_mut(ctx); - if ctx.path_compression_cache.borrow().get(&v) != Some(&tp) { - ctx.path_compression_cache - .borrow_mut() - .insert(v, tp.clone()); - } - tp - }) - .unwrap_or_else(|| self.clone()) - } - } - } - /// Like [`apply_compress`], but works in-place. - /// - /// [`apply_compress`]: #method.apply_compress - pub fn apply_mut(&mut self, ctx: &Context) { + // TODO: not sure if it's okay to assume this lifetime. I think so. + pub fn apply(&'ctx self, sub: &Substitution<'ctx, N>) -> Ty<'ctx, N> { match *self { - Type::Constructed(_, ref mut args) => { - for t in args { - t.apply_mut(ctx) + Type::Constructed(name, args) => { + let naive_args = args.iter().map(|t| t.apply(sub)).collect_vec(); + if naive_args == args { + self + } else { + sub.ctx.intern_tcon(name, &naive_args) } } - Type::Variable(v) => { - let maybe_tp = ctx - .path_compression_cache - .borrow() - .get(&v) - .or_else(|| ctx.substitution.get(&v)) - .cloned(); - *self = maybe_tp - .map(|mut tp| { - tp.apply_mut(ctx); - ctx.path_compression_cache - .borrow_mut() - .insert(v, tp.clone()); - tp - }) - .unwrap_or_else(|| self.clone()); - } + Type::Variable(v) => sub.get(v).map(|tp| tp.apply(sub)).unwrap_or_else(|| self), } } /// Generalizes the type by quantifying over free variables in a [`TypeSchema`]. @@ -481,33 +260,34 @@ impl Type { /// # Examples /// /// ``` - /// # use polytype::{tp, Context}; - /// let t = tp!(@arrow[tp!(0), tp!(1)]); - /// assert_eq!(t.to_string(), "t0 → t1"); + /// # use polytype::{tp, with_ctx, Substitution, TypeContext, Type, Variable}; + /// with_ctx(10, |ctx: TypeContext<'_>| { + /// let t_int = tp!(ctx, int); + /// let t_0 = tp!(ctx, 0); + /// let t_1 = tp!(ctx, 1); + /// let t = tp!(ctx, @arrow[t_0, t_1]); /// - /// let mut ctx = Context::default(); - /// ctx.extend(0, tp!(int)); + /// let mut sub = Substitution::with_capacity(ctx, 1); + /// sub.add(Variable(0), t_int); /// - /// let t_gen = t.apply(&ctx).generalize(&[]); - /// assert_eq!(t_gen.to_string(), "∀t1. int → t1"); + /// let t_free = t.apply(&sub).generalize(&[], &ctx); + /// assert_eq!(t_free.to_string(), "∀t1. int → t1"); /// - /// let t_gen = t.apply(&ctx).generalize(&[1]); - /// assert_eq!(t_gen.to_string(), "int → t1"); + /// let t_bound = t.apply(&sub).generalize(&[Variable(1)], &ctx); + /// assert_eq!(t_bound.to_string(), "int → t1"); + /// }) /// ``` /// /// [`TypeSchema`]: enum.TypeSchema.html - pub fn generalize(&self, bound: &[Variable]) -> TypeSchema { - let fvs = self - .vars() - .into_iter() - .filter(|x| !bound.contains(x)) - .collect::>(); - let mut t = TypeSchema::Monotype(self.clone()); + pub fn generalize( + &'ctx self, + bound: &[Variable], + ctx: &TypeContext<'ctx, N>, + ) -> Schema<'ctx, N> { + let fvs = self.vars().into_iter().filter(|x| !bound.contains(x)); + let mut t: Schema<'ctx, N> = ctx.intern_monotype(self); for v in fvs { - t = TypeSchema::Polytype { - variable: v, - body: Box::new(t), - }; + t = ctx.intern_polytype(v, t); } t } @@ -516,24 +296,29 @@ impl Type { /// # Examples /// /// ``` - /// # use polytype::tp; - /// let t = tp!(@arrow[tp!(0), tp!(1)]); - /// assert_eq!(t.to_string(), "t0 → t1"); + /// # use polytype::{with_ctx, Substitution, TypeContext, Type, Variable}; + /// with_ctx(10, |ctx: TypeContext<'_>| { + /// let t_0 = ctx.intern_tvar(Variable(0)); + /// let t_1 = ctx.intern_tvar(Variable(1)); + /// let t = ctx.arrow(t_0, t_1); /// - /// let mut vars = t.vars(); - /// vars.sort(); - /// assert_eq!(vars, vec![0, 1]); + /// assert_eq!(t.to_string(), "t0 → t1"); + /// + /// let mut vars = t.vars(); + /// vars.sort(); + /// assert_eq!(vars, vec![Variable(0), Variable(1)]); + /// }) /// ``` pub fn vars(&self) -> Vec { let mut vars = vec![]; self.vars_internal(&mut vars); - vars.sort_unstable(); + vars.sort(); vars.dedup(); vars } fn vars_internal(&self, vars: &mut Vec) { match *self { - Type::Constructed(_, ref args) => { + Type::Constructed(_, args) => { for arg in args { arg.vars_internal(vars); } @@ -541,82 +326,386 @@ impl Type { Type::Variable(v) => vars.push(v), } } - /// Perform a substitution. This is analogous to [`apply`]. + /// Parse a type from a string. This round-trips with [`Display`]. /// /// # Examples /// /// ``` - /// # use polytype::tp; - /// # use std::collections::HashMap; - /// let t = tp!(@arrow[tp!(0), tp!(1)]); - /// assert_eq!(t.to_string(), "t0 → t1"); + /// # use polytype::{with_ctx, TypeContext, Type, Variable}; + /// with_ctx(10, |ctx: TypeContext<'_>| { + /// let t_parse = Type::parse(&ctx, "int -> HashMap(t0, List(bool))").expect("valid type"); + /// + /// let n_int = ctx.intern_name("int"); + /// let n_hash = ctx.intern_name("HashMap"); + /// let n_list = ctx.intern_name("List"); + /// let n_bool = ctx.intern_name("bool"); + /// let t_int = ctx.intern_tcon(n_int, &[]); + /// let t_0 = ctx.intern_tvar(Variable(0)); + /// let t_bool = ctx.intern_tcon(n_bool, &[]); + /// let t_list = ctx.intern_tcon(n_list, &[t_bool]); + /// let t_hash = ctx.intern_tcon(n_hash, &[t_0, t_list]); + /// let t_manual = ctx.arrow(t_int, t_hash); /// - /// let mut substitution = HashMap::new(); - /// substitution.insert(0, tp!(int)); - /// substitution.insert(1, tp!(bool)); + /// assert_eq!(t_parse, t_manual); /// - /// let t = t.substitute(&substitution); - /// assert_eq!(t.to_string(), "int → bool"); + /// let s = "(t1 → t0 → t1) → t1 → list(t0) → t1"; + /// let t = Type::parse(&ctx, s).expect("valid type"); + /// let round_trip = t.to_string(); + /// assert_eq!(s, round_trip); + /// }) /// ``` /// - /// [`apply`]: #method.apply - pub fn substitute(&self, substitution: &HashMap>) -> Type { - match *self { - Type::Constructed(ref name, ref args) => { - let args = args.iter().map(|t| t.substitute(substitution)).collect(); - Type::Constructed(name.clone(), args) - } - Type::Variable(v) => substitution.get(&v).cloned().unwrap_or(Type::Variable(v)), - } + /// [`Display`]: https://doc.rust-lang.org/std/fmt/trait.Display.html + pub fn parse(ctx: &TypeContext<'ctx, N>, s: &str) -> Result, ParseError> { + parse_type(ctx, s) } - /// Like [`substitute`], but works in-place. + /// Unify a set of constraints. /// - /// [`substitute`]: #method.substitute - pub fn substitute_mut(&mut self, substitution: &HashMap>) { - match *self { - Type::Constructed(_, ref mut args) => { - for t in args { - t.substitute_mut(substitution) + /// # Examples + /// + /// ``` + /// # use polytype::{with_ctx, TypeContext, Type}; + /// with_ctx(10, |ctx: TypeContext<'_>| { + /// let t1 = Type::parse(&ctx, "int -> t0").expect("t1"); + /// let t2 = Type::parse(&ctx, "t1 -> bool").expect("t2"); + /// let sub = Type::unify(&[(t1, t2)], &ctx).expect("sub"); + /// + /// let t1 = t1.apply(&sub); + /// let t2 = t2.apply(&sub); + /// assert_eq!(t1, t2); + /// assert_eq!(t1.to_string(), "int → bool"); + /// }) + /// ``` + /// + /// Unification errors leave the context unaffected. A + /// [`UnificationError::Mismatch`] error happens when symbols don't match: + /// + /// ``` + /// # use polytype::{with_ctx, TypeContext, Type, UnificationError}; + /// with_ctx(10, |ctx: TypeContext<'_>| { + /// let t1 = Type::parse(&ctx, "int -> t0").expect("t1"); + /// let t2 = Type::parse(&ctx, "bool -> t1").expect("t2"); + /// let res = Type::unify(&[(t1, t2)], &ctx); + /// + /// if let Err(UnificationError::Mismatch(left, right)) = res { + /// assert_eq!(left.to_string(), "int"); + /// assert_eq!(right.to_string(), "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. + /// + /// ``` + /// # use polytype::{with_ctx, TypeContext, Type, UnificationError, Variable}; + /// with_ctx(10, |ctx: TypeContext<'_>| { + /// let t1 = Type::parse(&ctx, "t0").expect("t1"); + /// let t2 = Type::parse(&ctx, "bool -> t0").expect("t2"); + /// let res = Type::unify(&[(t1, t2)], &ctx); + /// + /// if let Err(UnificationError::Occurs(v)) = res { + /// assert_eq!(v, Variable(0)); + /// } else { unreachable!() } + /// }) + /// ``` + /// + /// [`UnificationError::Mismatch`]: enum.UnificationError.html#variant.Mismatch + /// [`UnificationError::Occurs`]: enum.UnificationError.html#variant.Occurs + /// [`instantiate`]: enum.Type.html#method.instantiate + pub fn unify( + cs: &[(Ty<'ctx, N>, Ty<'ctx, N>)], + ctx: &TypeContext<'ctx, N>, + ) -> Result, UnificationError<'ctx, N>> { + let mut sub = Substitution::with_capacity(ctx.clone(), 32); + Type::unify_with_sub(cs, &mut sub).map(|_| sub) + } + /// Unify a set of constraints subject to an existing `Substitution`. + /// + /// # Examples + /// + /// ``` + /// # use polytype::{tp, with_ctx, Substitution, Type, TypeContext, Variable}; + /// with_ctx(10, |ctx: TypeContext<'_>| { + /// let t1 = Type::parse(&ctx, "t0 -> t1").expect("t1"); + /// let t2 = Type::parse(&ctx, "t2 -> bool").expect("t2"); + /// let tint = Type::parse(&ctx, "int").expect("tint"); + /// let mut sub = Substitution::with_capacity(ctx, 10); + /// sub.add(Variable(0), tint); + /// Type::unify_with_sub(&[(t1, t2)], &mut sub).expect("success"); + /// + /// let t1 = t1.apply(&sub); + /// let t2 = t2.apply(&sub); + /// assert_eq!(t1, t2); + /// assert_eq!(t1.to_string(), "int → bool"); + /// }) + /// ``` + pub fn unify_with_sub( + initial_cs: &[(Ty<'ctx, N>, Ty<'ctx, N>)], + sub: &mut Substitution<'ctx, N>, + ) -> Result<(), UnificationError<'ctx, N>> { + let mut cs: SmallVec<[(&Type, &Type); 32]> = smallvec![]; + for &(s, t) in initial_cs { + Type::unify_one(s, t, &mut cs, sub)?; + } + while let Some((s, t)) = cs.pop() { + Type::unify_one(s, t, &mut cs, sub)?; + } + Ok(()) + } + /// the internal implementation of a single unification. + #[inline] + fn unify_one( + mut s: Ty<'ctx, N>, + mut t: Ty<'ctx, N>, + cs: &mut SmallVec<[(Ty<'ctx, N>, Ty<'ctx, N>); 32]>, + subs: &mut Substitution<'ctx, N>, + ) -> Result<(), UnificationError<'ctx, N>> { + s = s.apply(subs); + t = t.apply(subs); + + // if they are equal, you're all done with them. + if s != t { + match (s, t) { + (Type::Variable(ref var), Type::Variable(_)) => { + subs.add(*var, t); } - } - Type::Variable(v) => { - if let Some(t) = substitution.get(&v) { - *self = t.clone() + (Type::Variable(ref var), t) => { + if t.occurs(*var) { + return Err(UnificationError::Occurs(*var)); + } else { + subs.add(*var, t); + } + } + (s, Type::Variable(ref var)) => { + if s.occurs(*var) { + return Err(UnificationError::Occurs(*var)); + } else { + subs.add(*var, s); + } + } + (Type::Constructed(n1, a1), Type::Constructed(n2, a2)) => { + if n1 != n2 { + return Err(UnificationError::Mismatch(s, t)); + } else { + for (&c1, &c2) in a1.iter().zip(a2.iter()) { + cs.push((c1, c2)); + } + } } } } + Ok(()) } } -impl fmt::Display for Type { + +impl<'ctx, N: Name> fmt::Display for Type<'ctx, N> { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> Result<(), fmt::Error> { write!(f, "{}", self.show(true)) } } -impl From>> for Type { - fn from(mut tps: VecDeque>) -> Type { - match tps.len() { - 0 => panic!("cannot create a type from nothing"), - 1 => tps.pop_front().unwrap(), - 2 => { - let alpha = tps.pop_front().unwrap(); - let beta = tps.pop_front().unwrap(); - Type::arrow(alpha, beta) + +impl<'ctx, N: Name> TypeSchema<'ctx, N> { + /// Checks whether a variable is bound in the quantification of a polytype. + /// + /// # Examples + /// + /// ``` + /// # use polytype::{with_ctx, TypeContext, TypeSchema, Variable}; + /// with_ctx(10, |ctx: TypeContext<'_>| { + /// let t = TypeSchema::parse(&ctx, "t0. t0 -> t1").expect("t"); + /// assert!(t.is_bound(Variable(0))); + /// assert!(!t.is_bound(Variable(1))); + /// }) + /// ``` + pub fn is_bound(&self, v: Variable) -> bool { + let mut t = self; + while let TypeSchema::Polytype(variable, body) = t { + if *variable == v { + return true; + } else { + t = body + } + } + false + } + /// Returns a set of each [`Variable`] bound by the [`TypeSchema`]. + /// + /// # Examples + /// + /// ``` + /// # use polytype::{with_ctx, TypeContext, TypeSchema, Variable}; + /// with_ctx(10, |ctx: TypeContext<'_>| { + /// let t = TypeSchema::parse(&ctx, "t0. t1. t1 -> t2 -> t3").expect("t"); + /// assert_eq!(t.bound_vars(), vec![Variable(0), Variable(1)]); + /// }) + /// ``` + /// + /// [`Variable`]: type.Variable.html + /// [`TypeSchema`]: enum.TypeSchema.html + pub fn bound_vars(&self) -> Vec { + let mut t = self; + let mut bvs = Vec::with_capacity(self.depth()); + while let TypeSchema::Polytype(variable, body) = *t { + bvs.push(variable); + t = body; + } + bvs + } + /// The number of [`Variable`]s bound by the `TypeSchema`. + /// + /// # Examples + /// + /// ``` + /// # use polytype::{with_ctx, TypeContext, TypeSchema, Variable}; + /// with_ctx(10, |ctx: TypeContext<'_>| { + /// let t = TypeSchema::parse(&ctx, "t0. t1. t1 -> t2 -> t3").expect("t"); + /// assert_eq!(t.depth(), 2); + /// }) + /// ``` + /// + /// [`Variable`]: type.Variable.html + pub fn depth(&self) -> usize { + let mut t = self; + let mut depth = 0; + while let TypeSchema::Polytype(_, body) = t { + depth += 1; + t = body; + } + depth + } + /// Returns a set of each free [`Variable`] in the [`TypeSchema`]. + /// + /// # Examples + /// + /// ``` + /// # use polytype::{with_ctx, TypeContext, TypeSchema, Variable}; + /// with_ctx(10, |ctx: TypeContext<'_>| { + /// let t = TypeSchema::parse(&ctx, "t0. t1. t1 -> t2 -> t3").expect("t"); + /// assert_eq!(t.free_vars(), vec![Variable(2), Variable(3)]); + /// }) + /// ``` + /// + /// [`Variable`]: type.Variable.html + /// [`TypeSchema`]: enum.TypeSchema.html + pub fn free_vars(&self) -> Vec { + let mut vars = vec![]; + self.free_vars_internal(&mut vars); + vars.sort(); + vars.dedup(); + vars + } + fn free_vars_internal(&self, vars: &mut Vec) { + match *self { + TypeSchema::Monotype(t) => t.vars_internal(vars), + TypeSchema::Polytype(variable, body) => { + body.free_vars_internal(vars); + *vars = vars.iter().filter(|&v| v != &variable).copied().collect(); } - _ => { - let alpha = tps.pop_front().unwrap(); - Type::arrow(alpha, tps.into()) + } + } + /// Instantiate a [`TypeSchema`] in the context by removing quantifiers. + /// + /// All type variables will be replaced with fresh type variables. + /// + /// # Examples + /// + /// ``` + /// # use polytype::{with_ctx, Source, TypeContext, TypeSchema, Variable}; + /// with_ctx(10, |ctx: TypeContext<'_>| { + /// let mut src = Source::default(); + /// src.fresh(); // Throw away a type variable to match parse. + /// let t = TypeSchema::parse(&ctx, "t1. t1 -> t0").expect("t"); + /// let t_in1 = t.instantiate(&ctx, &mut src); + /// let t_in2 = t.instantiate(&ctx, &mut src); + /// assert_eq!(t_in1.to_string(), "t1 → t0"); + /// assert_eq!(t_in2.to_string(), "t2 → t0"); + /// }) + /// ``` + /// + /// ``` + /// # use polytype::{with_ctx, Source, TypeContext, TypeSchema, Variable}; + /// with_ctx(10, |ctx: TypeContext<'_>| { + /// let mut src = Source::default(); + /// let t = TypeSchema::parse(&ctx, "t0. t1. (t0 -> t1) -> t0 -> t1").expect("t"); + /// let t_in1 = t.instantiate(&ctx, &mut src); + /// let t_in2 = t.instantiate(&ctx, &mut src); + /// assert_eq!(t_in1.to_string(), "(t0 → t1) → t0 → t1"); + /// assert_eq!(t_in2.to_string(), "(t2 → t3) → t2 → t3"); + /// }) + /// ``` + /// + /// [`TypeSchema`]: enum.TypeSchema.html + pub fn instantiate(&self, ctx: &TypeContext<'ctx, N>, src: &mut Source) -> Ty<'ctx, N> { + let mut sub = Substitution::with_capacity(ctx.clone(), self.depth()); + let mut tp = self; + loop { + match tp { + TypeSchema::Polytype(variable, body) => { + let t_var = Variable(src.fresh()); + let t = ctx.intern_tvar(t_var); + if *variable != t_var { + sub.add(*variable, t); + } + tp = body; + } + TypeSchema::Monotype(t) => return TypeSchema::substitute(t, &sub), + } + } + } + // A helper function used by `instantiate`. + fn substitute(tp: Ty<'ctx, N>, sub: &Substitution<'ctx, N>) -> Ty<'ctx, N> { + match *tp { + Type::Constructed(name, args) => { + let naive_args = args + .iter() + .map(|t| TypeSchema::substitute(t, sub)) + .collect_vec(); + sub.ctx.intern_tcon(name, &naive_args) } + // Major difference is here: we don't call substitute recursively. + Type::Variable(v) => sub.get(v).unwrap_or(tp), } } + /// Parse a [`TypeSchema`] from a string. This round-trips with [`Display`]. + /// + /// The "for-all" `∀` is optional. + /// + /// # Examples + /// + /// ``` + /// # use polytype::{with_ctx, TypeContext, TypeSchema, Variable}; + /// with_ctx(10, |ctx: TypeContext<'_>| { + /// let t_parse = TypeSchema::parse(&ctx, "∀t0. t0 -> t0").expect("t_parse"); + /// + /// let t_0 = ctx.intern_tvar(Variable(0)); + /// let t_arrow = ctx.arrow(t_0, t_0); + /// let t_mono = ctx.intern_monotype(t_arrow); + /// let t_manual = ctx.intern_polytype(Variable(0), t_mono); + /// + /// assert_eq!(t_parse, t_manual); + /// + /// let s = "∀t0. ∀t1. (t1 → t0 → t1) → t1 → list(t0) → t1"; + /// let t = TypeSchema::parse(&ctx, s).expect("t"); + /// let round_trip = t.to_string(); + /// assert_eq!(s, round_trip); + /// }) + /// ``` + /// + /// [`Display`]: https://doc.rust-lang.org/std/fmt/trait.Display.html + /// [`TypeSchema`]: enum.TypeSchema.html + pub fn parse(ctx: &TypeContext<'ctx, N>, s: &str) -> Result, ParseError> { + parse_typeschema(ctx, s) + } } -impl From>> for Type { - fn from(mut tps: Vec>) -> Type { - let mut beta = tps - .pop() - .unwrap_or_else(|| panic!("cannot create a type from nothing")); - while let Some(alpha) = tps.pop() { - beta = Type::arrow(alpha, beta) + +impl<'ctx, N: Name> fmt::Display for TypeSchema<'ctx, N> { + fn fmt(&self, f: &mut fmt::Formatter<'_>) -> Result<(), fmt::Error> { + match *self { + TypeSchema::Polytype(variable, body) => write!(f, "∀t{}. {}", variable.0, body), + TypeSchema::Monotype(ref t) => t.fmt(f), } - beta } } From 8d7bf4cecceea4fb48d73973cb29f3d1d8dce6f1 Mon Sep 17 00:00:00 2001 From: Josh Rule Date: Thu, 15 Jul 2021 13:20:51 -0700 Subject: [PATCH 2/3] enhancement: add SourceChange::reify_substitution --- src/source.rs | 52 ++++++++++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 51 insertions(+), 1 deletion(-) diff --git a/src/source.rs b/src/source.rs index 776acbf..850b002 100644 --- a/src/source.rs +++ b/src/source.rs @@ -1,4 +1,4 @@ -use crate::{Name, Schema, Ty, Type, TypeContext, TypeSchema, Variable}; +use crate::{Name, Schema, Substitution, Ty, Type, TypeContext, TypeSchema, Variable}; /// A way to generate fresh [`Variable`]s. /// @@ -171,4 +171,54 @@ impl SourceChange { } } } + /// Reify a [`Substitution`] for use under a new [`Source`]. + /// + /// # Examples + /// ``` + /// # use polytype::{ptp, tp, with_ctx, Source, Substitution, Type, TypeContext, Variable}; + /// with_ctx(1024, |ctx| { + /// let mut src = Source::default(); + /// let a = src.fresh(); + /// let b = src.fresh(); + /// let _ = src.fresh(); + /// let ta = ctx.intern_tvar(Variable(a)); + /// let tb = ctx.intern_tvar(Variable(b)); + /// let t1 = ctx.arrow(ta, tb); + /// let t2 = tp!(ctx, @arrow[tp!(ctx, int), tp!(ctx, bool)]); + /// let sub1 = Type::unify(&[(t1, t2)], &ctx).unwrap(); + /// + /// let mut src2 = Source::default(); + /// let _ = src2.fresh(); + /// let pt = ptp!(ctx, 0, 1; @arrow[tp!(ctx, 0), tp!(ctx, 1)]); + /// let t = pt.instantiate(&ctx, &mut src2); + /// let last = ctx.intern_tvar(Variable(src2.fresh())); + /// let mut sub2 = Substitution::with_capacity(ctx, 32); + /// sub2.add(Variable(2), tp!(ctx, bool)); + /// + /// let src_change = src.merge(src2, vec![Variable(0), Variable(1)]); + /// let t_reified = src_change.reify_type(t, &ctx); + /// assert_eq!(t_reified.to_string(), "t1 → t5"); + /// src_change.reify_substitution(&mut sub2, &ctx); + /// assert_eq!( + /// t_reified.apply(&sub2).apply(&sub1).to_string(), + /// "bool → bool" + /// ); + /// }) + ///``` + /// + /// [`Substitution`]: struct.Substitution.html + /// [`Source`]: struct.Source.html + pub fn reify_substitution<'ctx, N: Name>( + &self, + sub: &mut Substitution<'ctx, N>, + ctx: &TypeContext<'ctx, N>, + ) { + for (var, tp) in sub.sub.iter_mut() { + let contains_var = self.sacreds.contains(var); + if !contains_var { + *var = Variable(var.0 + self.delta) + } + *tp = self.reify_type(tp, ctx); + } + } } From f061073dfc4fefe5232cc6278968cabfe2e15729 Mon Sep 17 00:00:00 2001 From: Josh Rule Date: Thu, 15 Jul 2021 13:21:08 -0700 Subject: [PATCH 3/3] tests: update tests.rs to use interning --- tests/tests.rs | 603 ++++++++++++++++++++++++------------------------- 1 file changed, 301 insertions(+), 302 deletions(-) diff --git a/tests/tests.rs b/tests/tests.rs index 5b48181..01b0815 100644 --- a/tests/tests.rs +++ b/tests/tests.rs @@ -1,370 +1,369 @@ -use std::collections::VecDeque; - use polytype::*; #[test] fn test_tp_macro() { - assert_eq!(tp!(bool), Type::Constructed("bool", vec![])); - assert_eq!( - tp!(list(tp!(bool))), - Type::Constructed("list", vec![Type::Constructed("bool", vec![])]), - ); - assert_eq!( - tp!(list(tp!(tuple(tp!(bool), tp!(int))))), - Type::Constructed( - "list", - vec![Type::Constructed( - "tuple", - vec![ - Type::Constructed("bool", vec![]), - Type::Constructed("int", vec![]), + with_ctx(1024, |ctx: TypeContext<'_>| { + assert_eq!(tp!(ctx, bool), &Type::Constructed(&"bool", &[])); + assert_eq!( + tp!(ctx, list(tp!(ctx, bool))), + &Type::Constructed(&"list", &[&Type::Constructed(&"bool", &[])]), + ); + assert_eq!( + tp!(ctx, list(tp!(ctx, tuple(tp!(ctx, bool), tp!(ctx, int))))), + &Type::Constructed( + &"list", + &[&Type::Constructed( + &"tuple", + &[ + &Type::Constructed(&"bool", &[]), + &Type::Constructed(&"int", &[]), + ], + )], + ), + ); + assert_eq!( + tp!( + ctx, + list( + tp!(ctx, unusually_large_identifier_requiring_wrap), + tp!(ctx, unusually_large_identifier_requiring_wrap), + ) + ), + &Type::Constructed( + &"list", + &[ + &Type::Constructed(&"unusually_large_identifier_requiring_wrap", &[]), + &Type::Constructed(&"unusually_large_identifier_requiring_wrap", &[]), ], - )], - ), - ); - assert_eq!( - tp!(list( - tp!(unusually_large_identifier_requiring_wrap), - tp!(unusually_large_identifier_requiring_wrap), - )), - Type::Constructed( - "list", - vec![ - Type::Constructed("unusually_large_identifier_requiring_wrap", vec![]), - Type::Constructed("unusually_large_identifier_requiring_wrap", vec![]), - ], - ), - ); - assert_eq!(tp!(0), Type::Variable(0)); - assert_eq!( - tp!(hashmap(tp!(str), tp!(@arrow[tp!(int), tp!(0), tp!(bool)]))), - Type::Constructed( - "hashmap", - vec![ - Type::Constructed("str", vec![]), - Type::arrow( - Type::Constructed("int", vec![]), - Type::arrow(Type::Variable(0), Type::Constructed("bool", vec![])), - ), - ], - ) - ); - // arrows - assert_eq!(tp!(@arrow[Type::Variable(0)]), Type::Variable(0)); - let arg = Type::Variable(0); - let ret = Type::Variable(1); - let t = tp!(@arrow[arg, ret]); - assert_eq!(t, tp!(@arrow[Type::Variable(0), Type::Variable(1)])); - assert_eq!( - tp!(@arrow[Type::Variable(0), Type::Variable(1), Type::Variable(2)]), - Type::arrow( - Type::Variable(0), - Type::arrow(Type::Variable(1), Type::Variable(2)), - ) - ); - assert_eq!( - tp!(@arrow[ - Type::Variable(0), - Type::Variable(1), - Type::Variable(2), - Type::Variable(3), - ]), - Type::arrow( - Type::Variable(0), - Type::arrow( - Type::Variable(1), - Type::arrow(Type::Variable(2), Type::Variable(3)), ), - ) - ); + ); + assert_eq!(tp!(ctx, 0), &Type::Variable(Variable(0))); + assert_eq!( + tp!( + ctx, + hashmap( + tp!(ctx, str), + tp!(ctx, @arrow[tp!(ctx, int), tp!(ctx, 0), tp!(ctx, bool)]) + ) + ), + &Type::Constructed( + &"hashmap", + &[ + &Type::Constructed(&"str", &[]), + ctx.arrow( + &Type::Constructed(&"int", &[]), + ctx.arrow( + &Type::Variable(Variable(0)), + &Type::Constructed(&"bool", &[]) + ), + ), + ], + ) + ); + // arrows + assert_eq!(tp!(ctx, @arrow[tp!(ctx, 0)]), &Type::Variable(Variable(0))); + let arg = &Type::Variable(Variable(0)); + let ret = &Type::Variable(Variable(1)); + let t = tp!(ctx, @arrow[arg, ret]); + assert_eq!( + t, + tp!(ctx, @arrow[&Type::Variable(Variable(0)), &Type::Variable(Variable(1))]) + ); + assert_eq!( + tp!(ctx, @arrow[tp!(ctx, 0), tp!(ctx, 1), tp!(ctx, 2)]), + ctx.arrow( + &Type::Variable(Variable(0)), + ctx.arrow(&Type::Variable(Variable(1)), &Type::Variable(Variable(2))), + ) + ); + assert_eq!( + tp!(ctx, @arrow[ + tp!(ctx, 0), + tp!(ctx, 1), + tp!(ctx, 2), + tp!(ctx, 3), + ]), + ctx.arrow( + &Type::Variable(Variable(0)), + ctx.arrow( + &Type::Variable(Variable(1)), + ctx.arrow(&Type::Variable(Variable(2)), &Type::Variable(Variable(3))), + ), + ) + ); + }) } #[test] fn test_ptp_macro() { - assert_eq!( - ptp!(bool), - TypeSchema::Monotype(Type::Constructed("bool", vec![])) - ); - assert_eq!( - ptp!(list(tp!(bool))), - TypeSchema::Monotype(Type::Constructed( - "list", - vec![Type::Constructed("bool", vec![])], - )) - ); - assert_eq!( - ptp!(0; 0), - TypeSchema::Polytype { - variable: 0, - body: Box::new(TypeSchema::Monotype(Type::Variable(0))), - } - ); - assert_eq!( - ptp!(0; @arrow[tp!(0), tp!(0)]), - TypeSchema::Polytype { - variable: 0, - body: Box::new(TypeSchema::Monotype(Type::Constructed( - "→", - vec![Type::Variable(0), Type::Variable(0)], - ))), - } - ); -} - -#[test] -fn test_arrow_methods() { - let t0 = Type::Variable(0); - let t1 = Type::Constructed("int", vec![]); - let t2 = Type::arrow(t0.clone(), t1.clone()); - let ta1 = Type::arrow(t2.clone(), Type::arrow(t1.clone(), t0.clone())); - let ta2 = tp!(@arrow[t2.clone(), t1.clone(), t0.clone()]); - let ta3 = tp!(@arrow[tp!(@arrow[tp!(0), tp!(int)]), tp!(int), tp!(0)]); - assert_eq!(ta3, ta1); - assert_eq!(ta3, ta2); - let t = tp!(@arrow[tp!(@arrow[tp!(0), tp!(int)]), tp!(int), tp!(0)]); - assert_eq!( - t.args(), - Some(VecDeque::from(vec![ - &tp!(@arrow[tp!(0), tp!(int)]), - &tp!(int), - ])), - ); - assert_eq!(t.returns(), Some(&tp!(0))); -} - -#[test] -fn test_tp_from_vecdeque() { - let mut tps = VecDeque::new(); - tps.push_back(Type::Variable(0)); - let tp: Type = tps.clone().into(); - assert_eq!(tp, Type::Variable(0)); - - tps.push_back(Type::Variable(1)); - let tp: Type = tps.clone().into(); - assert_eq!(tp, Type::arrow(Type::Variable(0), Type::Variable(1))); - - tps.push_back(Type::Variable(2)); - let tp: Type = tps.clone().into(); - assert_eq!( - tp, - Type::arrow( - Type::Variable(0), - Type::arrow(Type::Variable(1), Type::Variable(2)) - ) - ); - tps.push_back(Type::Variable(3)); - let tp: Type = tps.clone().into(); - assert_eq!( - tp, - Type::arrow( - Type::Variable(0), - Type::arrow( - Type::Variable(1), - Type::arrow(Type::Variable(2), Type::Variable(3)) + with_ctx(1024, |ctx| { + assert_eq!( + ptp!(ctx, bool), + &TypeSchema::Monotype(&Type::Constructed(&"bool", &[])) + ); + assert_eq!( + ptp!(ctx, list(tp!(ctx, bool))), + &TypeSchema::Monotype(&Type::Constructed( + &"list", + &[&Type::Constructed(&"bool", &[])], + )) + ); + assert_eq!( + ptp!(ctx, 0; 0), + &TypeSchema::Polytype( + Variable(0), + &TypeSchema::Monotype(&Type::Variable(Variable(0))), ) - ) - ); + ); + assert_eq!( + ptp!(ctx, 0; @arrow[tp!(ctx, 0), tp!(ctx, 0)]), + &TypeSchema::Polytype( + Variable(0), + &TypeSchema::Monotype(&Type::Constructed( + &"→", + &[&Type::Variable(Variable(0)), &Type::Variable(Variable(0))], + )), + ) + ); + }) } #[test] -fn test_tp_from_vec() { - let mut tps = Vec::new(); - tps.push(Type::Variable(0)); - let tp: Type = tps.clone().into(); - assert_eq!(tp, Type::Variable(0)); - - tps.push(Type::Variable(1)); - let tp: Type = tps.clone().into(); - assert_eq!(tp, Type::arrow(Type::Variable(0), Type::Variable(1))); - - tps.push(Type::Variable(2)); - let tp: Type = tps.clone().into(); - assert_eq!( - tp, - Type::arrow( - Type::Variable(0), - Type::arrow(Type::Variable(1), Type::Variable(2)) - ) - ); - tps.push(Type::Variable(3)); - let tp: Type = tps.clone().into(); - assert_eq!( - tp, - Type::arrow( - Type::Variable(0), - Type::arrow( - Type::Variable(1), - Type::arrow(Type::Variable(2), Type::Variable(3)) - ) - ) - ); +fn test_arrow_methods() { + with_ctx(1024, |ctx| { + let t0 = &Type::Variable(Variable(0)); + let t1 = &Type::Constructed(&"int", &[]); + let t2 = ctx.arrow(t0, t1); + let ta1 = ctx.arrow(t2, ctx.arrow(t1, t0)); + let ta2 = tp!(ctx, @arrow[t2, t1, t0]); + let ta3 = tp!(ctx, @arrow[tp!(ctx, @arrow[tp!(ctx, 0), tp!(ctx, int)]), tp!(ctx, int), tp!(ctx, 0)]); + assert_eq!(ta3, ta1); + assert_eq!(ta3, ta2); + let t = tp!(ctx, @arrow[tp!(ctx, @arrow[tp!(ctx, 0), tp!(ctx, int)]), tp!(ctx, int), tp!(ctx, 0)]); + assert_eq!( + t.args(), + Some(Vec::from(vec![ + tp!(ctx, @arrow[tp!(ctx, 0), tp!(ctx, int)]), + tp!(ctx, int), + ])), + ); + assert_eq!(t.returns(), Some(tp!(ctx, 0))); + }) } #[test] fn test_unify_one_side_polymorphic() { - let mut ctx = Context::default(); - ctx.unify( - &tp!(list(tp!(@arrow[tp!(int), tp!(bool)]))), - &tp!(list(tp!(0))), - ) - .expect("one side polymorphic"); + with_ctx(1024, |ctx| { + Type::unify( + &[( + tp!(ctx, list(tp!(ctx, @arrow[tp!(ctx, int), tp!(ctx, bool)]))), + tp!(ctx, list(tp!(ctx, 0))), + )], + &ctx, + ) + .expect("one side polymorphic"); + }) } #[test] fn test_unify_one_side_polymorphic_fail() { - let mut ctx = Context::default(); - ctx.unify(&tp!(@arrow[tp!(int), tp!(bool)]), &tp!(list(tp!(0)))) + with_ctx(1024, |ctx| { + Type::unify( + &[( + tp!(ctx, @arrow[tp!(ctx, int), tp!(ctx, bool)]), + tp!(ctx, list(tp!(ctx, 0))), + )], + &ctx, + ) .expect_err("incompatible types"); + }) } #[test] fn test_unify_both_sides_polymorphic() { - let mut ctx = Context::default(); - ctx.unify( - &tp!(list(tp!(@arrow[tp!(int), tp!(0)]))), - &tp!(list(tp!(@arrow[tp!(1), tp!(bool)]))), - ) - .expect("both sides polymorphic"); + with_ctx(1024, |ctx| { + Type::unify( + &[( + tp!(ctx, list(tp!(ctx, @arrow[tp!(ctx, int), tp!(ctx, 0)]))), + tp!(ctx, list(tp!(ctx, @arrow[tp!(ctx, 1), tp!(ctx, bool)]))), + )], + &ctx, + ) + .expect("both sides polymorphic"); + }) } #[test] fn test_unify_both_sides_polymorphic_occurs() { - let mut ctx = Context::default(); - ctx.unify(&tp!(0), &tp!(list(tp!(@arrow[tp!(0), tp!(bool)])))) + with_ctx(1024, |ctx| { + Type::unify( + &[( + tp!(ctx, 0), + tp!(ctx, list(tp!(ctx, @arrow[tp!(ctx, 0), tp!(ctx, bool)]))), + )], + &ctx, + ) .expect_err("circular polymorphic types"); + }) } #[test] fn test_unify_nonstring_name() { - #[derive(Debug, Clone, PartialEq, Eq)] + #[derive(Debug, Clone, PartialEq, Eq, Hash)] struct N(u32); + struct ParseError; impl Name for N { + type ParseError = ParseError; fn arrow() -> Self { N(0) } + fn parse(s: &str) -> Result { + match s.parse::() { + Ok(n) => Ok(N(n)), + Err(_) => Err(ParseError), + } + } } - let ts = TypeSchema::Polytype { - variable: 0, - body: Box::new(TypeSchema::Monotype(Type::Constructed( - N(3), - vec![Type::Variable(0)], - ))), - }; + with_ctx(1024, |ctx| { + let mut src = Source::default(); - let mut ctx = Context::default(); - let t = ts.instantiate(&mut ctx); - ctx.unify( - &Type::Constructed( - N(3), - vec![Type::arrow( - Type::Constructed(N(1), vec![]), - Type::Constructed(N(2), vec![]), - )], - ), - &t, - ) - .expect("nonstring one side polymorphic"); + let ts = TypeSchema::Polytype( + Variable(0), + &TypeSchema::Monotype(&Type::Constructed(&N(3), &[&Type::Variable(Variable(0))])), + ); - let mut ctx = Context::default(); - let t = ts.instantiate(&mut ctx); - ctx.unify( - &Type::arrow( - Type::Constructed(N(1), vec![]), - Type::Constructed(N(2), vec![]), - ), - &t, - ) - .expect_err("nonstring incompatible types"); + let t = ts.instantiate(&ctx, &mut src); + let t_n1 = ctx.intern_name(N(1)); + let t_n2 = ctx.intern_name(N(2)); + let t_n3 = ctx.intern_name(N(3)); + let t_con1 = ctx.intern_tcon(t_n1, &[]); + let t_con2 = ctx.intern_tcon(t_n2, &[]); + let t_arrow = ctx.arrow(t_con1, t_con2); + let t_test = ctx.intern_tcon(t_n3, &[t_arrow]); + Type::unify(&[(t_test, t)], &ctx).expect("nonstring one side polymorphic"); + + let t = ts.instantiate(&ctx, &mut src); + let t_test = ctx.arrow( + &Type::Constructed(&N(1), &[]), + &Type::Constructed(&N(2), &[]), + ); + Type::unify(&[(t, t_test)], &ctx).expect_err("nonstring incompatible types"); + }) } #[test] fn test_merge_no_sacreds() { - let mut ctx = Context::default(); - let a = ctx.new_variable(); - let b = ctx.new_variable(); - let _ = ctx.new_variable(); - ctx.unify(&Type::arrow(a, b), &tp!(@arrow[tp!(int), tp!(bool)])) - .unwrap(); + with_ctx(1024, |ctx| { + let mut src = Source::default(); + let a = src.fresh(); + let b = src.fresh(); + let _ = src.fresh(); + let ta = ctx.intern_tvar(Variable(a)); + let tb = ctx.intern_tvar(Variable(b)); + let t1 = ctx.arrow(ta, tb); + let t2 = tp!(ctx, @arrow[tp!(ctx, int), tp!(ctx, bool)]); + let sub1 = Type::unify(&[(t1, t2)], &ctx).unwrap(); - let mut ctx2 = Context::default(); - let _ = ctx2.new_variable(); - let pt = ptp!(0, 1; @arrow[tp!(0), tp!(1)]); - let mut t = pt.instantiate(&mut ctx2); - ctx2.extend(1, tp!(bool)); - let mut last = ctx2.new_variable(); - assert_eq!(t.apply(&ctx2).to_string(), "bool → t2"); + let mut src2 = Source::default(); + let _ = src2.fresh(); + let pt = ptp!(ctx, 0, 1; @arrow[tp!(ctx, 0), tp!(ctx, 1)]); + let t = pt.instantiate(&ctx, &mut src2); + let last = ctx.intern_tvar(Variable(src2.fresh())); + let mut sub2 = Substitution::with_capacity(ctx, 32); + sub2.add(Variable(2), tp!(ctx, bool)); + assert_eq!(t.apply(&sub2).to_string(), "t1 → bool"); - let ctx_change = ctx.merge(ctx2, vec![]); - ctx_change.reify_type(&mut t); - assert_eq!(t.to_string(), "t4 → t5"); - assert_eq!(t.apply(&ctx).to_string(), "bool → t5"); - ctx_change.reify_type(&mut last); - assert_eq!(last, tp!(6)); - assert_eq!(ctx.new_variable(), tp!(7)); + let src_change = src.merge(src2, vec![]); + let t_reified = src_change.reify_type(t, &ctx); + assert_eq!(t_reified.to_string(), "t4 → t5"); + src_change.reify_substitution(&mut sub2, &ctx); + assert_eq!(t_reified.apply(&sub2).apply(&sub1).to_string(), "t4 → bool"); + let last_reified = src_change.reify_type(last, &ctx); + assert_eq!(last_reified, tp!(ctx, 6)); + assert_eq!(src.fresh(), 7); + }) } #[test] fn test_merge_with_sacreds() { - let mut ctx = Context::default(); - let a = ctx.new_variable(); - let b = ctx.new_variable(); - let _ = ctx.new_variable(); - ctx.unify(&Type::arrow(a, b), &tp!(@arrow[tp!(int), tp!(bool)])) - .unwrap(); + with_ctx(1024, |ctx| { + let mut src = Source::default(); + let a = src.fresh(); + let b = src.fresh(); + let _ = src.fresh(); + let ta = ctx.intern_tvar(Variable(a)); + let tb = ctx.intern_tvar(Variable(b)); + let t1 = ctx.arrow(ta, tb); + let t2 = tp!(ctx, @arrow[tp!(ctx, int), tp!(ctx, bool)]); + let sub1 = Type::unify(&[(t1, t2)], &ctx).unwrap(); - let mut ctx2 = Context::default(); - let _ = ctx2.new_variable(); - let pt = ptp!(0, 1; @arrow[tp!(0), tp!(1)]); - let mut t = pt.instantiate(&mut ctx2); - ctx2.extend(2, tp!(bool)); - let mut last = ctx2.new_variable(); - assert_eq!(t.apply(&ctx2).to_string(), "t1 → bool"); + let mut src2 = Source::default(); + let _ = src2.fresh(); + let pt = ptp!(ctx, 0, 1; @arrow[tp!(ctx, 0), tp!(ctx, 1)]); + let t = pt.instantiate(&ctx, &mut src2); + let last = ctx.intern_tvar(Variable(src2.fresh())); + let mut sub2 = Substitution::with_capacity(ctx, 32); + sub2.add(Variable(2), tp!(ctx, bool)); + assert_eq!(t.apply(&sub2).to_string(), "t1 → bool"); - let ctx_change = ctx.merge(ctx2, vec![0, 1]); - ctx_change.reify_type(&mut t); - assert_eq!(t.to_string(), "t1 → t5"); - assert_eq!(t.apply(&ctx).to_string(), "bool → bool"); - ctx_change.reify_type(&mut last); - assert_eq!(last, tp!(6)); - assert_eq!(ctx.new_variable(), tp!(7)); + let src_change = src.merge(src2, vec![Variable(0), Variable(1)]); + let t_reified = src_change.reify_type(t, &ctx); + assert_eq!(t_reified.to_string(), "t1 → t5"); + src_change.reify_substitution(&mut sub2, &ctx); + assert_eq!( + t_reified.apply(&sub2).apply(&sub1).to_string(), + "bool → bool" + ); + let last_reified = src_change.reify_type(last, &ctx); + assert_eq!(last_reified, tp!(ctx, 6)); + assert_eq!(src.fresh(), 7); + }) } #[cfg(feature = "parser")] #[test] fn test_parse() { - let t = tp!(int); - assert_eq!(&t, &Type::parse("int").expect("parse 1")); - assert_eq!(t, Type::parse(&t.to_string()).expect("parse 2")); + with_ctx(1024, |ctx| { + let t = tp!(ctx, int); + assert_eq!(&t, &Type::parse(&ctx, "int").expect("parse 1")); + assert_eq!(t, Type::parse(&ctx, &t.to_string()).expect("parse 2")); - let t = tp!(0); - assert_eq!(&t, &Type::parse("t0").expect("parse 3")); - assert_eq!(t, Type::parse(&t.to_string()).expect("parse 4")); + let t = tp!(ctx, 0); + assert_eq!(&t, &Type::parse(&ctx, "t0").expect("parse 3")); + assert_eq!(t, Type::parse(&ctx, &t.to_string()).expect("parse 4")); - let t = tp!(@arrow[tp!(int), tp!(int)]); - assert_eq!(&t, &Type::parse("int -> int").expect("parse 5")); - assert_eq!(t, Type::parse(&t.to_string()).expect("parse 6")); + let t = tp!(ctx, @arrow[tp!(ctx, int), tp!(ctx, int)]); + assert_eq!(&t, &Type::parse(&ctx, "int -> int").expect("parse 5")); + assert_eq!(t, Type::parse(&ctx, &t.to_string()).expect("parse 6")); - let t = tp!(list(tp!(@arrow[tp!(int), tp!(2)]))); - assert_eq!(&t, &Type::parse("list(int -> t2)").expect("parse 7")); - assert_eq!(t, Type::parse(&t.to_string()).expect("parse 8")); + let t = tp!(ctx, list(tp!(ctx, @arrow[tp!(ctx, int), tp!(ctx, 2)]))); + assert_eq!(&t, &Type::parse(&ctx, "list(int -> t2)").expect("parse 7")); + assert_eq!(t, Type::parse(&ctx, &t.to_string()).expect("parse 8")); - let t = tp!(hashmap(tp!(str), tp!(@arrow[tp!(int), tp!(0), tp!(bool)]))); - assert_eq!( - &t, - &Type::parse("hashmap(str, int -> t0 -> bool)").expect("parse 9") - ); - assert_eq!(t, Type::parse(&t.to_string()).expect("parse 10")); + let t = tp!( + ctx, + hashmap( + tp!(ctx, str), + tp!(ctx, @arrow[tp!(ctx, int), tp!(ctx, 0), tp!(ctx, bool)]) + ) + ); + assert_eq!( + &t, + &Type::parse(&ctx, "hashmap(str, int -> t0 -> bool)").expect("parse 9") + ); + assert_eq!(t, Type::parse(&ctx, &t.to_string()).expect("parse 10")); - let t = tp!(@arrow[ - tp!(@arrow[tp!(1), tp!(0), tp!(1)]), - tp!(1), - tp!(list(tp!(0))), - tp!(1), - ]); - assert_eq!( - &t, - &Type::parse("(t1 → t0 → t1) → t1 → list(t0) → t1").expect("parse 11") - ); - assert_eq!(t, Type::parse(&t.to_string()).expect("parse 12")); + let t = tp!(ctx, @arrow[ + tp!(ctx, @arrow[tp!(ctx, 1), tp!(ctx, 0), tp!(ctx, 1)]), + tp!(ctx, 1), + tp!(ctx, list(tp!(ctx, 0))), + tp!(ctx, 1), + ]); + assert_eq!( + &t, + &Type::parse(&ctx, "(t1 → t0 → t1) → t1 → list(t0) → t1").expect("parse 11") + ); + assert_eq!(t, Type::parse(&ctx, &t.to_string()).expect("parse 12")); + }) }