Orbital library

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)

Orbital library
1.3.0: 11 Apr 2009

Copyright © 1996-2009 André Platzer
All Rights Reserved.