Trait rusttyc::types::Variant

pub trait Variant: Sized + Clone + Debug + Eq {
    type Err: Debug;
    fn top() -> Self;
    fn meet(
        lhs: Partial<Self>, 
        rhs: Partial<Self>
    ) -> Result<Partial<Self>, Self::Err>;
    fn arity(&self) -> Arity;
}

A variant that will be inferred during the type checking procedure.

Requirements

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

Refinement

The top value needs to be provided by the Variant::top() function. Types will be refined successively using the fallible Variant::meet() function. If the types are incompatible, i.e., would result in a contradictory type, the meet needs to return a Variant::Err. Note that Variant::meet() needs to follow the rules of abstract meets. Intuitively, these are:

• The result of a meet needs to be more or equally concrete than either argument.
• Meeting two variants returns the greatest upper bound, i.e., the type variant 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. The arguments of the meet functions are Partial, i.e., the combination of a variant and the least number of children the respective type has. This is of particular interest for types that are not fully resolved and thus do not have a fixed arity, yet. An unconstained type variant could have a sub-type because it will be later determined to be an "Option" or "Tuple" type. More details in the next section.

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, tuples might have an arbitrary arity. 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. Hence, its least arity is initially 0 and potentially increases when more information was collected.

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

The meet of two variants must not reduce its arity. For example, meeting a pair with fixed arity 2 and a triple with fixed arity 3 may not result in a variant with fixed arity 1. It may, however, result in a variant with variable arity.

Example

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

Context

If the variant requires a context for the meet and/or equality operation, refer to ContextSensitiveVariant. Each Variant automatically implements ContextSensitiveVariant.

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. The error will be wrapped into a crate::TcErr providing contextual information.

Loading content...

Required methods

fn top() -> Self

Returns the unconstrained, most abstract type.

fn meet(
    lhs: Partial<Self>,
    rhs: Partial<Self>
) -> Result<Partial<Self>, Self::Err>

Attempts to meet two variants respecting their currently-determined potentially variable arity. Refer to Variant for the responsibilities of this function. In particular: usize::max(lhs.least_arity, rhs.least_arity) <= result.least_arity In the successful case, the variant and arity of the partial have to match, i.e., if the Arity is fixed with value n, then Partial::least_arity needs to be n as well.

fn arity(&self) -> Arity

Indicates whether the variant has a fixed arity. Note that this values does not have to be constant over all instances of the variant. A tuple, for example, might have a variable arity until the inferrence reaches a point where it is determined to be a pair or a triple. The pair and triple are both represented by the same type variant and have a fixed, non-specific arity. Before obtaining this information, the tuple has a variable arity and potentially a different variant.

Loading content...

Implementors

Loading content...