Enum Type 

pub enum Type {
    Any,
    MaybeZero(Box<Type>),
    Named(String, Vec<Type>),
    And(Vec<Type>),
    Arrow(Box<Type>, Box<Type>),
    Tuple(Vec<Type>),
    HTuple(Box<Type>, Constant),
    Product(Vec<Type>),
    Ratio(Box<Type>, Box<Type>),
    Constant(Constant),
}

Each Term has at least one Type.

Types are composed of Atomic parts like Nameds. An Named type has a name and possibly some parameters. Atomic parts can be combined to form Compound parts like Arrows. Compound parts are formed by some combination of Arrows, Tuples, Products, and Ratios. At the Highest level a Compound type can be pluralized with an And to join it to other Compounds.

And types are represented in Conjunctive-Normal-Form which requires the Ands to only occupy the highest level of a type. Some basic typing algorithms may not work correctly if a type is not in Conjunctive-Normal-Form.

Subtyping is implemented with And types. An implication, A + A => B, may be rewritten as just A + B.

Variants

Any

MaybeZero(Box<Type>)

Named(String, Vec<Type>)

And(Vec<Type>)

Arrow(Box<Type>, Box<Type>)

Tuple(Vec<Type>)

HTuple(Box<Type>, Constant)

Product(Vec<Type>)

Ratio(Box<Type>, Box<Type>)

Constant(Constant)

Implementations

impl Type

pub fn datatype(&self) -> String

pub fn project_ratio(&self) -> (Vec<Type>, Vec<Type>)

pub fn is_ctuple(&self) -> bool

pub fn is_open(&self) -> bool

pub fn is_constant(&self) -> bool

pub fn all_named(&self) -> Vec<Type>

pub fn and(&self, other: &Type) -> Type

pub fn is_var(&self) -> bool

pub fn domain(&self) -> Type

pub fn range(&self) -> Type

pub fn vars(&self) -> Vec<String>

pub fn simplify_ratio(&self) -> Type

pub fn normalize(&self) -> Type

pub fn remove(&self, x: &Type) -> Type

pub fn substitute(&self, subs: &HashMap<Type, Type>) -> Type

pub fn is_concrete(&self) -> bool

pub fn kind(&self, kinds: &HashMap<Type, Kind>) -> Kind

pub fn narrow(&self, kinds: &HashMap<Type, Kind>, k: &Kind) -> Type

pub fn is_bottom(&self) -> bool

pub fn compile_subs(subs: &Vec<(Type, Type)>) -> Result<HashMap<Type, Type>, ()>

pub fn implies(tlc: &TLC, lt: &Type, rt: &Type) -> Type

pub fn arrow_implies( tlc: &TLC, lt: &mut Type, rt: &mut Type, inarrow: InArrow, ) -> Type

pub fn subs_implies( tlc: &TLC, subs: &mut Vec<(Type, Type)>, lt: &Type, rt: &Type, ) -> Type

pub fn nored_implies( tlc: &TLC, subs: &mut Vec<(Type, Type)>, lt: &Type, rt: &Type, ) -> Type

pub fn implication_unifier(&self, other: &Type) -> Type

pub fn subs_implication_unifier( &self, subs: &mut Vec<(Type, Type)>, other: &Type, ) -> Type

pub fn most_general_unifier(&self, other: &Type) -> Type

Trait Implementations

impl Clone for Type

fn clone(&self) -> Type

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for Type

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl Hash for Type

fn hash<__H: Hasher>(&self, state: &mut __H)

Feeds this value into the given Hasher.

fn hash_slice<H>(data: &[Self], state: &mut H)

where H: Hasher, Self: Sized,

Feeds a slice of this type into the given Hasher.

impl Ord for Type

fn cmp(&self, other: &Type) -> Ordering

This method returns an Ordering between self and other.

fn max(self, other: Self) -> Self

where Self: Sized,

Compares and returns the maximum of two values.

fn min(self, other: Self) -> Self

where Self: Sized,

Compares and returns the minimum of two values.

fn clamp(self, min: Self, max: Self) -> Self

where Self: Sized,

Restrict a value to a certain interval.

impl PartialEq for Type

fn eq(&self, other: &Type) -> bool

Tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl PartialOrd for Type

fn partial_cmp(&self, other: &Type) -> Option<Ordering>

This method returns an ordering between self and other values if one exists.

fn lt(&self, other: &Rhs) -> bool

Tests less than (for self and other) and is used by the < operator.

fn le(&self, other: &Rhs) -> bool

Tests less than or equal to (for self and other) and is used by the <= operator.

fn gt(&self, other: &Rhs) -> bool

Tests greater than (for self and other) and is used by the > operator.

fn ge(&self, other: &Rhs) -> bool

Tests greater than or equal to (for self and other) and is used by the >= operator.

impl Eq for Type

impl StructuralPartialEq for Type