Trait rusttyc::types::Abstract

pub trait Abstract: Eq + Sized + Clone + Debug {
    type Err: Debug;
    fn unconstrained() -> Self;
    fn meet(&self, other: &Self) -> Result<Self, Self::Err>;
    fn arity(&self) -> Option<usize>;
    fn nth_child(&self, n: usize) -> &Self;
    fn with_children<I>(&self, children: I) -> Self
    where
        I: IntoIterator<Item = Self>;

    fn is_unconstrained(&self) -> bool { ... }
}

An abstract type that will be inferred during the type checking procedure.

This trait that needs to be implemented by all (rust-) types that represent a type in the type checking procedure.

Requirements

The abstract types need to follow a lattice structure where the top element is the least constrained, most abstract type possible.

Refinement

This value needs to be provided by the Abstract::unconstrained function. Types will be refined successively using the fallible meet function. If the types are incompatible, i.e., would result in a contradictory type, the meet needs to return a Result::Err. Otherwise, it returns a Result::Ok containing the resulting type. The function needs to follow the rules for abstract meets. Intuitively, these are:

• The result of a meet needs to be more or equally concrete than either argument.
• Meeting two types returns the greatest upper bound, i.e., the type that is more or equally concrete to either argument and there is no other, less concrete type meeting this requirement. This especially entails that meeting any type T with an unconstrained type returns T.

Arity

Type can be recursive, i.e., they have a number of subtypes, their "children". An integer, for example, has no children and is thus 0-ary. An optional type on the other hand is 1-ary, i.e., it has one sub-type. During the inference process, the arity might be undetermined: the unconstrained type will resolve to something with an arity, but the value is not clear, yet.

The type checking procedure keeps track of types and their potential children.
For this, it requires some guarantees when it comes to the arity:

Arity Stability

• If a type has a defined arity, it may not change when turning more concrete. Thus, abstract types with ambiguous arity must not return an arity.
• A leaf type, i.e., a fully resolved non-contradictory type must provide an arity. A consequence is that the meet of two types with different, defined arity will result in an error.

Example

For a full example of an abstract type system, refer to the crate documentation and the examples. TODO: link!

Associated Types

type Err: Debug

Result of a meet of two incompatible type, i.e., it represents a type contradiction. May contain information regarding why the meet failed.

Loading content...

Required methods

fn unconstrained() -> Self

Returns the unconstrained, most abstract type.

fn meet(&self, other: &Self) -> Result<Self, Self::Err>

Attempts to meet two abstract types. Refer to the documentation of Abstract for the responsibilities of this function.

fn arity(&self) -> Option<usize>

Provides the arity of the self if the type is sufficiently resolved to determine it.

fn nth_child(&self, n: usize) -> &Self

Provide access to the nth child.

Guarantee

The arity of self is defined and greater or equal to n: assert!(self.arity.map(|a| *a >= n).unwrap_or(false)

fn with_children<I>(&self, children: I) -> Self where
    I: IntoIterator<Item = Self>, 

Generate an instance of Self that is equivalent to self except that the children of the newly generated type will be children.

Guarantee

The arity of self is defined and corresponds to the number of element in children: assert!(self.arity.map(|a| a == children.collect::<Vec>().len()).unwrap_or(false))`

Loading content...

Provided methods

fn is_unconstrained(&self) -> bool

Determines whether or not self is the unconstrained type.

Loading content...

Implementors

Loading content...