orbital.logic.sign.type
Interface Type

All Superinterfaces:

java.lang.Comparable, Functor, Predicate

All Known Subinterfaces:

Type.Composite

public interface Type
extends java.lang.Comparable, Predicate

Representation of a type.

The types form a free algebra of terms Τ over {ι,→,()} plus perhaps {×,∩,∪,{},⟨⟩,〔〕}. Intuitively, ι is the type for individuals, σ→τ the type for maps from σ to τ, and (σ) = σ→ο the type for predicates of σ, likewise ο = () is the type of truth-values. A type denotes the set of possible values for a quantity. But there is also a precise semantics.

Need for this class

Unfortunately, without creating classes for every combination of types, Java class objects cannot represent types like (σ→σ')→(τ→τ') even though they occur quite naturally in unifying approaches of expressions. Additionally, the Java language specification disallows covariant return-types, such that natural subtypes cannot be modelled with class inheritance. Also, the Java Generics do not yet provide access to template parameter types at runtime. Therefore, this class needed being introduced as a supplement for strict typing information at runtime.

Author:

André Platzer

See Also:

TypeSystem, Typed.getType(), Class

Nested Class Summary

static interface

Type.Composite The base interface for all composite types that are composed of other types.

Nested classes/interfaces inherited from interface orbital.logic.functor.Functor

Functor.Specification

Field Summary

Fields inherited from interface orbital.logic.functor.Predicate

callTypeDeclaration

Method Summary

boolean	apply(java.lang.Object x) Checks whether an object x is an instance of this type.
Type	codomain() Get the co-domain τ of a type σ→τ.
int	compareTo(java.lang.Object tau) Compares two types for subtype inclusions.
Type	domain() Get the domain σ of a type σ→τ.
boolean	equals(java.lang.Object o) Checks two types for equality.
int	hashCode()
Type	on(Type sigma) Applies this type on sigma returning the resulting type.
boolean	subtypeOf(Type tau) Checks whether this type is a subtype of tau.
java.lang.String	toString() Returns a string representation of this type.
TypeSystem	typeSystem() Get the type system that this type stems from.

Method Detail

equals

boolean equals(java.lang.Object o)

Checks two types for equality. By antisymmetry, two types are equal if they are mutual subtypes of each other.

σ→τ equals σ'→τ' :⇔ σ = σ' ∧ τ = τ'.

Specified by:

equals in interface Functor

Overrides:

equals in class java.lang.Object

hashCode

int hashCode()

Specified by:

hashCode in interface Functor

Overrides:

hashCode in class java.lang.Object

toString

java.lang.String toString()

Returns a string representation of this type.

Specified by:

toString in interface Functor

Overrides:

toString in class java.lang.Object

Returns:

a nice name for the functor.

domain

Type domain()

Get the domain σ of a type σ→τ.

Returns:

the type of the parameter domain. TypeSystem.NOTYPE() if this type does not take parameters.

codomain

Type codomain()

Get the co-domain τ of a type σ→τ.

Returns:

the type of the result value co-domain.

typeSystem

TypeSystem typeSystem()

Get the type system that this type stems from.

Returns:

the type system that created this type.

compareTo

int compareTo(java.lang.Object tau)

Compares two types for subtype inclusions. Defines the subtype relation on types. Note that this only is a partial order, but it is still consistent with equals (thus not only a quasi-order).

Specified by:

compareTo in interface java.lang.Comparable

Parameters:

tau - the type τ to check for being a supertype, subtype of us, or equals.

Returns:

Returns a value < 0 if this < τ (this is a proper subtype of τ).
Returns a value > 0 if this > τ (this is a proper supertype of τ).
Returns 0 if this = τ (which is the case if and only if this ≤ τ and this ≥ τ).

Throws:

IncomparableException - if the types are incomparable.

See Also:

subtypeOf(Type), TypeSystem.inf(), TypeSystem.sup()

Preconditions:

tau instanceof Type

subtypeOf

boolean subtypeOf(Type tau)

Checks whether this type is a subtype of tau. σ is a subtype of τ, written σ ≤ τ, if in every context using values of type τ, any value of type σ would be permitted as well. Convenience method.

Returns:

whether this ≤ τ. Especially returns false in case of incomparable types.

See Also:

Convenience method, compareTo(Object), Class.isAssignableFrom(java.lang.Class)

on

Type on(Type sigma)

Applies this type on sigma returning the resulting type.

Applying objects of type τ∈Τ on objects of type σ∈Τ gives objects of type τ∘σ∈Τ. For example,

(σ→τ)∘σ = τ

Parameters:

sigma - the type σ that this type is applied on.

Returns:

this type applied on sigma, i.e. the type τ∘σ all objects f(x) will have if f:τ and x:σ.

Throws:

TypeException - if τ∘σ is undefined, i.e. objects of this type τ cannot be applied to objects of type σ.

apply

boolean apply(java.lang.Object x)

Checks whether an object x is an instance of this type. Applies the type identifier predicate belonging to this type.

The type identifier predicate belonging to the type τ, is:

τ(x) ⇔ x is an instance of τ

The extension, δτ, of this predicate is the set of all actually existing elements of type τ.

Specified by:

apply in interface Predicate

Parameters:

x - single Object argument

Returns:

whether τ(x), i.e. x is an instance of this type τ.

See Also:

Class.isInstance(Object)