Enum Type

Source

pub enum Type {
    Var(TyVar),
    App(TyCon, Vec<Type>),
}

Expand description

A type term: either an inference variable or a constructor applied to arguments.

This is the structural core every concrete type is expressed in. A type is one of two shapes:

Var — an inference TyVar, possibly still unbound.
App — a TyCon applied to zero or more argument types. A primitive like int is the zero-argument case; a List<int> is List applied to int; a function (A) -> B is some -> constructor applied to A and B.

The same two shapes describe primitives, generics, functions, tuples, and any other first-order type former — the meaning of each constructor is the consumer’s to define. Build terms with the var, con, and app constructors.

§Examples

use type_lang::{TyCon, Type, Unifier};

const INT: TyCon = TyCon::new(0);
const LIST: TyCon = TyCon::new(1);

let mut unifier = Unifier::new();
let element = unifier.fresh();

// List<?element>
let list_of = Type::app(LIST, [Type::var(element)]);
// List<int>
let list_int = Type::app(LIST, [Type::con(INT)]);

unifier.unify(&list_of, &list_int).expect("same constructor");
assert_eq!(unifier.resolve(&Type::var(element)), Type::con(INT));

Variants§

§

Var(TyVar)

An inference variable.

§

App(TyCon, Vec<Type>)

A constructor applied to its arguments. The argument list is empty for a nullary constructor such as a primitive.

Implementations§

Source §

impl Type

Source

pub const fn var(var: TyVar) -> Self

Builds a variable type from a TyVar.

§Examples

use type_lang::{Type, Unifier};

let mut unifier = Unifier::new();
let v = unifier.fresh();
let ty = Type::var(v);
assert_eq!(ty.as_var(), Some(v));

Source

pub const fn con(head: TyCon) -> Self

Builds a nullary constructor type, such as a primitive.

This is the zero-argument case of app; Type::con(c) and Type::app(c, []) are the same term.

§Examples

use type_lang::{TyCon, Type};

const UNIT: TyCon = TyCon::new(0);
let ty = Type::con(UNIT);
assert_eq!(ty.head(), Some(UNIT));
assert!(ty.args().is_empty());

Source

pub fn app(head: TyCon, args: impl Into<Vec<Type>>) -> Self

Builds a constructor applied to a list of argument types.

Accepts anything that turns into a Vec<Type> — an array, a Vec, or any iterator’s collect() — so a fixed-arity type reads naturally:

use type_lang::{TyCon, Type, Unifier};

const FUNCTION: TyCon = TyCon::new(0);
const INT: TyCon = TyCon::new(1);

let mut unifier = Unifier::new();
let result = unifier.fresh();

// (int) -> ?result
let signature = Type::app(FUNCTION, [Type::con(INT), Type::var(result)]);
assert_eq!(signature.head(), Some(FUNCTION));
assert_eq!(signature.args().len(), 2);

Source

pub const fn as_var(&self) -> Option<TyVar>

Returns the variable if this is a Var, otherwise None.

§Examples

use type_lang::{TyCon, Type, Unifier};

let mut unifier = Unifier::new();
let v = unifier.fresh();
assert_eq!(Type::var(v).as_var(), Some(v));
assert_eq!(Type::con(TyCon::new(0)).as_var(), None);

Source

pub const fn head(&self) -> Option<TyCon>

Returns the head constructor if this is an App, otherwise None (a variable has no constructor).

§Examples

use type_lang::{TyCon, Type, Unifier};

const INT: TyCon = TyCon::new(0);
let mut unifier = Unifier::new();

assert_eq!(Type::con(INT).head(), Some(INT));
assert_eq!(Type::var(unifier.fresh()).head(), None);

Source

pub fn args(&self) -> &[Type]

Returns the argument types of an App, or an empty slice for a variable or a nullary constructor.

§Examples

use type_lang::{TyCon, Type};

const PAIR: TyCon = TyCon::new(0);
const INT: TyCon = TyCon::new(1);

let pair = Type::app(PAIR, [Type::con(INT), Type::con(INT)]);
assert_eq!(pair.args().len(), 2);
assert!(Type::con(INT).args().is_empty());

Source