type_lang/ty.rs
1//! The type term: variables, constructors, and their application.
2
3use alloc::vec::Vec;
4use core::fmt;
5
6/// An inference variable — a placeholder for a type not yet known.
7///
8/// A `TyVar` is a 32-bit handle minted by [`Unifier::fresh`](crate::Unifier::fresh)
9/// and stable for the life of that unifier. It is deliberately opaque: there is no
10/// public constructor, so a variable can only be obtained from a unifier. Mint and
11/// use variables in the same unifier — a handle is an index into that unifier's id
12/// space, and a unifier treats an id it has not minted as an unbound variable, so a
13/// handle is only meaningful against the unifier that produced it.
14///
15/// A variable starts life unbound — it stands for "some type" — and unification
16/// may bind it to a concrete type or to another variable. Use
17/// [`Unifier::resolve`](crate::Unifier::resolve) to read back what a variable has
18/// become; a variable that is still unbound resolves to itself.
19///
20/// # Examples
21///
22/// ```
23/// use type_lang::Unifier;
24///
25/// let mut unifier = Unifier::new();
26/// let a = unifier.fresh();
27/// let b = unifier.fresh();
28///
29/// // Variables are minted in order and stay distinct.
30/// assert_eq!(a.to_u32(), 0);
31/// assert_eq!(b.to_u32(), 1);
32/// assert_ne!(a, b);
33/// ```
34#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
35#[derive(Clone, Copy, Debug, PartialEq, Eq, PartialOrd, Ord, Hash)]
36pub struct TyVar(u32);
37
38impl TyVar {
39 /// Wraps a raw index. Internal: only a [`Unifier`](crate::Unifier) mints
40 /// variables, so that every variable in circulation belongs to a unifier that
41 /// can resolve it.
42 #[inline]
43 pub(crate) const fn from_index(index: u32) -> Self {
44 Self(index)
45 }
46
47 /// Returns the raw index this variable wraps.
48 ///
49 /// The value is the variable's creation order, starting at `0`. It is useful as
50 /// a dense key into a side table of per-variable data; prefer passing the
51 /// opaque `TyVar` itself wherever a handle will do.
52 ///
53 /// # Examples
54 ///
55 /// ```
56 /// use type_lang::Unifier;
57 ///
58 /// let mut unifier = Unifier::new();
59 /// let v = unifier.fresh();
60 /// assert_eq!(v.to_u32(), 0);
61 /// ```
62 #[inline]
63 #[must_use]
64 pub const fn to_u32(self) -> u32 {
65 self.0
66 }
67}
68
69/// A type constructor — the name a concrete type is built from.
70///
71/// A `TyCon` is an opaque 32-bit tag that the *consumer* assigns meaning to. This
72/// crate stores and compares constructors but never interprets them, so a language
73/// front-end is free to map its own primitives and type formers onto whatever tags
74/// it likes:
75///
76/// ```
77/// use type_lang::TyCon;
78///
79/// const INT: TyCon = TyCon::new(0);
80/// const BOOL: TyCon = TyCon::new(1);
81/// const FUNCTION: TyCon = TyCon::new(2);
82/// const LIST: TyCon = TyCon::new(3);
83/// ```
84///
85/// Two constructors are the same type former when their tags are equal, so keeping
86/// the tag assignment stable across a compilation is the caller's responsibility —
87/// a `const` table, as above, is the usual way.
88#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
89#[derive(Clone, Copy, Debug, PartialEq, Eq, PartialOrd, Ord, Hash)]
90pub struct TyCon(u32);
91
92impl TyCon {
93 /// Creates a constructor from a tag.
94 ///
95 /// The tag identifies the type former; the caller chooses the numbering and is
96 /// responsible for keeping it consistent. Equal tags are treated as the same
97 /// constructor during unification.
98 ///
99 /// # Examples
100 ///
101 /// ```
102 /// use type_lang::TyCon;
103 ///
104 /// let int = TyCon::new(0);
105 /// assert_eq!(int.to_u32(), 0);
106 /// ```
107 #[inline]
108 #[must_use]
109 pub const fn new(tag: u32) -> Self {
110 Self(tag)
111 }
112
113 /// Returns the raw tag this constructor wraps.
114 #[inline]
115 #[must_use]
116 pub const fn to_u32(self) -> u32 {
117 self.0
118 }
119}
120
121/// A type term: either an inference variable or a constructor applied to arguments.
122///
123/// This is the structural core every concrete type is expressed in. A type is one
124/// of two shapes:
125///
126/// - [`Var`](Self::Var) — an inference [`TyVar`], possibly still unbound.
127/// - [`App`](Self::App) — a [`TyCon`] applied to zero or more argument types. A
128/// primitive like `int` is the zero-argument case; a `List<int>` is `List`
129/// applied to `int`; a function `(A) -> B` is some `->` constructor applied to
130/// `A` and `B`.
131///
132/// The same two shapes describe primitives, generics, functions, tuples, and any
133/// other first-order type former — the meaning of each constructor is the
134/// consumer's to define. Build terms with the [`var`](Self::var),
135/// [`con`](Self::con), and [`app`](Self::app) constructors.
136///
137/// # Examples
138///
139/// ```
140/// use type_lang::{TyCon, Type, Unifier};
141///
142/// const INT: TyCon = TyCon::new(0);
143/// const LIST: TyCon = TyCon::new(1);
144///
145/// let mut unifier = Unifier::new();
146/// let element = unifier.fresh();
147///
148/// // List<?element>
149/// let list_of = Type::app(LIST, [Type::var(element)]);
150/// // List<int>
151/// let list_int = Type::app(LIST, [Type::con(INT)]);
152///
153/// unifier.unify(&list_of, &list_int).expect("same constructor");
154/// assert_eq!(unifier.resolve(&Type::var(element)), Type::con(INT));
155/// ```
156#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
157#[derive(Clone, Debug, PartialEq, Eq, Hash)]
158pub enum Type {
159 /// An inference variable.
160 Var(TyVar),
161 /// A constructor applied to its arguments. The argument list is empty for a
162 /// nullary constructor such as a primitive.
163 App(TyCon, Vec<Type>),
164}
165
166impl Type {
167 /// Builds a variable type from a [`TyVar`].
168 ///
169 /// # Examples
170 ///
171 /// ```
172 /// use type_lang::{Type, Unifier};
173 ///
174 /// let mut unifier = Unifier::new();
175 /// let v = unifier.fresh();
176 /// let ty = Type::var(v);
177 /// assert_eq!(ty.as_var(), Some(v));
178 /// ```
179 #[inline]
180 #[must_use]
181 pub const fn var(var: TyVar) -> Self {
182 Self::Var(var)
183 }
184
185 /// Builds a nullary constructor type, such as a primitive.
186 ///
187 /// This is the zero-argument case of [`app`](Self::app); `Type::con(c)` and
188 /// `Type::app(c, [])` are the same term.
189 ///
190 /// # Examples
191 ///
192 /// ```
193 /// use type_lang::{TyCon, Type};
194 ///
195 /// const UNIT: TyCon = TyCon::new(0);
196 /// let ty = Type::con(UNIT);
197 /// assert_eq!(ty.head(), Some(UNIT));
198 /// assert!(ty.args().is_empty());
199 /// ```
200 #[inline]
201 #[must_use]
202 pub const fn con(head: TyCon) -> Self {
203 Self::App(head, Vec::new())
204 }
205
206 /// Builds a constructor applied to a list of argument types.
207 ///
208 /// Accepts anything that turns into a `Vec<Type>` — an array, a `Vec`, or any
209 /// iterator's `collect()` — so a fixed-arity type reads naturally:
210 ///
211 /// ```
212 /// use type_lang::{TyCon, Type, Unifier};
213 ///
214 /// const FUNCTION: TyCon = TyCon::new(0);
215 /// const INT: TyCon = TyCon::new(1);
216 ///
217 /// let mut unifier = Unifier::new();
218 /// let result = unifier.fresh();
219 ///
220 /// // (int) -> ?result
221 /// let signature = Type::app(FUNCTION, [Type::con(INT), Type::var(result)]);
222 /// assert_eq!(signature.head(), Some(FUNCTION));
223 /// assert_eq!(signature.args().len(), 2);
224 /// ```
225 #[inline]
226 #[must_use]
227 pub fn app(head: TyCon, args: impl Into<Vec<Type>>) -> Self {
228 Self::App(head, args.into())
229 }
230
231 /// Returns the variable if this is a [`Var`](Self::Var), otherwise `None`.
232 ///
233 /// # Examples
234 ///
235 /// ```
236 /// use type_lang::{TyCon, Type, Unifier};
237 ///
238 /// let mut unifier = Unifier::new();
239 /// let v = unifier.fresh();
240 /// assert_eq!(Type::var(v).as_var(), Some(v));
241 /// assert_eq!(Type::con(TyCon::new(0)).as_var(), None);
242 /// ```
243 #[inline]
244 #[must_use]
245 pub const fn as_var(&self) -> Option<TyVar> {
246 match self {
247 Self::Var(v) => Some(*v),
248 Self::App(..) => None,
249 }
250 }
251
252 /// Returns the head constructor if this is an [`App`](Self::App), otherwise
253 /// `None` (a variable has no constructor).
254 ///
255 /// # Examples
256 ///
257 /// ```
258 /// use type_lang::{TyCon, Type, Unifier};
259 ///
260 /// const INT: TyCon = TyCon::new(0);
261 /// let mut unifier = Unifier::new();
262 ///
263 /// assert_eq!(Type::con(INT).head(), Some(INT));
264 /// assert_eq!(Type::var(unifier.fresh()).head(), None);
265 /// ```
266 #[inline]
267 #[must_use]
268 pub const fn head(&self) -> Option<TyCon> {
269 match self {
270 Self::App(head, _) => Some(*head),
271 Self::Var(_) => None,
272 }
273 }
274
275 /// Returns the argument types of an [`App`](Self::App), or an empty slice for a
276 /// variable or a nullary constructor.
277 ///
278 /// # Examples
279 ///
280 /// ```
281 /// use type_lang::{TyCon, Type};
282 ///
283 /// const PAIR: TyCon = TyCon::new(0);
284 /// const INT: TyCon = TyCon::new(1);
285 ///
286 /// let pair = Type::app(PAIR, [Type::con(INT), Type::con(INT)]);
287 /// assert_eq!(pair.args().len(), 2);
288 /// assert!(Type::con(INT).args().is_empty());
289 /// ```
290 #[inline]
291 #[must_use]
292 pub fn args(&self) -> &[Type] {
293 match self {
294 Self::App(_, args) => args,
295 Self::Var(_) => &[],
296 }
297 }
298
299 /// Returns `true` if this term is an inference variable.
300 #[inline]
301 #[must_use]
302 pub const fn is_var(&self) -> bool {
303 matches!(self, Self::Var(_))
304 }
305}
306
307impl fmt::Display for Type {
308 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
309 match self {
310 Self::Var(v) => write!(f, "?{}", v.to_u32()),
311 Self::App(head, args) => {
312 write!(f, "#{}", head.to_u32())?;
313 if let [first, rest @ ..] = args.as_slice() {
314 write!(f, "({first}")?;
315 for arg in rest {
316 write!(f, ", {arg}")?;
317 }
318 write!(f, ")")?;
319 }
320 Ok(())
321 }
322 }
323 }
324}
325
326#[cfg(test)]
327mod tests {
328 extern crate alloc;
329 use alloc::string::ToString;
330 use alloc::vec;
331
332 use super::*;
333
334 const INT: TyCon = TyCon::new(0);
335 const PAIR: TyCon = TyCon::new(5);
336
337 #[test]
338 fn test_con_is_app_with_no_arguments() {
339 assert_eq!(Type::con(INT), Type::app(INT, vec![]));
340 }
341
342 #[test]
343 fn test_accessors_split_var_from_app() {
344 let v = TyVar::from_index(2);
345 assert_eq!(Type::var(v).as_var(), Some(v));
346 assert_eq!(Type::var(v).head(), None);
347 assert!(Type::var(v).is_var());
348
349 let pair = Type::app(PAIR, vec![Type::con(INT), Type::var(v)]);
350 assert_eq!(pair.as_var(), None);
351 assert_eq!(pair.head(), Some(PAIR));
352 assert_eq!(pair.args().len(), 2);
353 assert!(!pair.is_var());
354 }
355
356 #[test]
357 fn test_display_renders_structure() {
358 assert_eq!(Type::var(TyVar::from_index(4)).to_string(), "?4");
359 assert_eq!(Type::con(INT).to_string(), "#0");
360 let nested = Type::app(PAIR, vec![Type::con(INT), Type::var(TyVar::from_index(1))]);
361 assert_eq!(nested.to_string(), "#5(#0, ?1)");
362 }
363
364 #[test]
365 fn test_handles_work_as_map_keys() {
366 use alloc::collections::BTreeMap;
367
368 // TyVar and TyCon derive Ord + Hash, so they key ordered and hashed maps.
369 let mut cons: BTreeMap<TyCon, u32> = BTreeMap::new();
370 let _ = cons.insert(INT, 0);
371 let _ = cons.insert(PAIR, 1);
372 assert_eq!(cons.get(&PAIR), Some(&1));
373
374 let mut vars: BTreeMap<TyVar, &str> = BTreeMap::new();
375 let _ = vars.insert(TyVar::from_index(0), "a");
376 let _ = vars.insert(TyVar::from_index(1), "b");
377 assert_eq!(vars.get(&TyVar::from_index(1)), Some(&"b"));
378 }
379}