orbital.logic.sign.type
Interface TypeSystem

public interface TypeSystem

Provides type constructors, and factories for types of a type system. Type constructors create new types depending on some existing types. Factories, instead, create completely new types. For example, there are type constructors for map types.

 [A type system is a] tractable syntactic method for proving the
 absence of certain program behaviors by classifying phrases
 according to the kinds of values they compute.

 (Types and Programming Languages, MIT Press, 2002)
 

Author:

André Platzer

See Also:

Types.getDefault(), Type.typeSystem(), Type, Meta-Object Facility

Note:

Type constructors with list or set parameters usually also accept them as generalized iteratable objects, including but not limited to List, Set.

Method Summary

Type	ABSURD() The absurd type ⊥ = ⋃∅.
Function	bag() bag: * → *; τ ↦ 〔τ〕.
Type	bag(Type element) The bag/multiset type 〔τ〕.
Function	collection() collection: * → *; τ ↦ collection(τ).
Type	collection(Type element) The general collection type collection(τ).
boolean	equals(java.lang.Object o) Checks whether two type systems are equal.
int	hashCode()
Function	inf() inf: {*} → *; (τi) ↦ ⋂iτi = τ1∩…∩τn.
Type	inf(Type[] components) Get the infimum type ⋂iτi = τ1∩…∩τn.
Function	list() list: * → *; τ ↦ ⟨τ⟩.
Type	list(Type element) The list type ⟨τ⟩.
BinaryFunction	map() map: *×* → *; (σ,τ) ↦ σ→τ.
Type	map(Type domain, Type codomain) Get the map type σ→τ.
Type	NOTYPE() Not a type.
Type	objectType(java.lang.Class type) Get the object type described by a class.
Type	objectType(java.lang.Class type, java.lang.String signifier) Get the object type described by a class.
Function	predicate() predicate: * → *; σ ↦ (σ).
Type	predicate(Type domain) Get the predicate type (σ) = σ→ο.
Function	product() product: ⟨*⟩ → *; (τi) ↦ ∏iτi = τ1×…×τn.
Type	product(Type[] components) Get the product type ∏iτi = τ1×…×τn.
Function	set() set: * → *; τ ↦ {τ}.
Type	set(Type element) The set type {τ}.
Function	sup() sup: {*} → *; (τi) ↦ ⋃iτi = τ1∪…∪τn.
Type	sup(Type[] components) Get the supremum type ⋃iτi = τ1∪…∪τn.
Type	TYPE() The meta-type (kind) of types *:□.
Type	UNIVERSAL() The universal type ⊤ = ⋂∅.

Method Detail

equals

boolean equals(java.lang.Object o)

Checks whether two type systems are equal. Two type systems are equal if they produce completely compatible types on all operations.

Type system equality will often only depend on the implementation's classes.

Overrides:

equals in class java.lang.Object

hashCode

int hashCode()

Overrides:

hashCode in class java.lang.Object

TYPE

Type TYPE()

The meta-type (kind) of types *:□. The type * and every type containing * is a kind, with the latter being types for type constructors. Types containing meta-types as well as ordinary types are currently not defined.

Postconditions:

RES == OLD(RES)

UNIVERSAL

Type UNIVERSAL()

The universal type ⊤ = ⋂_∅. It is the top element of the lattice Τ of types, has no differentiae and is characterized by

• (∃x) ⊤(x)
• (∀x) ⊤(x)
• (∀τ:Type) τ≤⊤

This would be the only type of uniform type systems.

See Also:

ABSURD()

Postconditions:

RES == OLD(RES)

ABSURD

Type ABSURD()

The absurd type ⊥ = ⋃_∅. It is the bottom element of the lattice Τ of types, it cannot be the type of anything that exists, and it is characterized by

• ¬(∃x) ⊥(x)
• (∀τ:Type) ⊥≤τ

See Also:

UNIVERSAL()

Postconditions:

RES == OLD(RES)

NOTYPE

Type NOTYPE()

Not a type. The type of expressions that do not have any type at all. This type has extension ∅.

See Also:

ABSURD()

Postconditions:

RES == OLD(RES)

objectType

Type objectType(java.lang.Class type)

Get the object type described by a class. Converts a native Java class object to a type. These types are called object types since they directly are types of objects, described by their classes.

Parameters:

type - the type τ represented as a class object.

Returns:

τ = void→τ.

objectType

Type objectType(java.lang.Class type,
                java.lang.String signifier)

Get the object type described by a class. Converts a native Java class object to a type. These types are called object types since they directly are types of objects, described by their classes.

Still unspecified: type alias'

This method allows specifying unusual signifiers for types. ☡ But be aware that this only changes the displayed name of the type, not the type itself. So it is

 objectType(java.lang.Number,"number").equals(objectType(java.lang.Number,"numericQuantity")
 

Parameters:

type - the type τ represented as a class object.

signifier - the representing the type.

Returns:

τ = void→τ.

See Also:

objectType(Class)

map

Type map(Type domain,
         Type codomain)

Get the map type σ→τ. In terms of Π-abstraction, it is σ→τ := τ^σ := Πx:σ.τ.

The subtype relation of types extends to map types as follows

σ→τ ≤ σ'→τ' :⇔ σ' ≤ σ ∧ τ ≤ τ' ⇔ σ ≥ σ' ∧ τ ≤ τ'.

This means that map subtypes have contravariant parameters and covariant return-types. With the exception of absurd types:

σ→⊥ = ⊥.

⊥→σ = not defined.

Parameters:

domain - the domain σ.

codomain - the co-domain τ.

map

BinaryFunction map()

map: *×* → *; (σ,τ) ↦ σ→τ.

The map type constructor.

See Also:

map(Type,Type)

Postconditions:

RES == OLD(RES)

predicate

Type predicate(Type domain)

Get the predicate type (σ) = σ→ο.

☡ Note that this type depends on the specific truth values.

Parameters:

domain - the co-domain σ.

See Also:

map(Type,Type)

predicate

Function predicate()

predicate: * → *; σ ↦ (σ).

The predicate type constructor.

See Also:

predicate(Type)

Postconditions:

RES == OLD(RES)

product

Type product(Type[] components)

Get the product type ∏_iτ_i = τ₁×…×τ_n.

Also called tuple type.

The subtype relation of types extends to product types as follows

∏_i∈Iσ_i ≤ ∏_j∈Jτ_j :⇔ I=J ∧ ∀i∈I σ_i ≤ τ_i

Parameters:

components - the components τ_i of the product type.

See Also:

list(Type)

product

Function product()

product: ⟨*⟩ → *; (τ_i) ↦ ∏_iτ_i = τ₁×…×τ_n.

The product type constructor.

See Also:

product(Type[])

Postconditions:

RES == OLD(RES)

inf

Type inf(Type[] components)

Get the infimum type ⋂_iτ_i = τ₁∩…∩τ_n. inf is the most general common subtype in the type lattice, also called intersection. Especially, it is ∀i ⋂_iτ_i ≤ τ_i.

The subtype relation of types extends to infimum types as follows

⋂_i∈Iσ_i ≤ τ :⇔ ∃i∈I σ_i ≤ τ

τ ≤ ⋂_i∈Iσ_i :⇔ ∀i∈I τ ≤ σ_i

provided that τ is not again an infimum type nor contains one.

See Also:

Type.compareTo(Object)

Postconditions:

RES is infimum of components with respect to ≤

Attributes:

associative, neutral ⊤, commutative, distributive sup(Type[]), idempotent, σ ≤ τ ⇔ σ∩τ = σ

inf

Function inf()

inf: {*} → *; (τ_i) ↦ ⋂_iτ_i = τ₁∩…∩τ_n.

The infimum type constructor.

See Also:

inf(Type[]), Type.compareTo(Object)

Postconditions:

RES == OLD(RES)

sup

Type sup(Type[] components)

Get the supremum type ⋃_iτ_i = τ₁∪…∪τ_n. sup is the most special common supertype in the type lattice, also called union. Especially, it is ∀i τ_i ≤ ⋃_iτ_i.

The subtype relation of types extends to supremum types as follows

⋃_i∈Iσ_i ≤ τ :⇔ ∀i∈I σ_i ≤ τ

⋃_i∈Iσ_i ≥ τ :⇔ ∃i∈I σ_i ≥ τ

provided that τ is not again a supremum type nor contains one.

See Also:

Type.compareTo(Object)

Postconditions:

RES is supremum of components with respect to ≤

Attributes:

associative, neutral ⊥, commutative, distributive inf(Type[]), idempotent, σ ≤ τ ⇔ σ∪τ = τ

sup

Function sup()

sup: {*} → *; (τ_i) ↦ ⋃_iτ_i = τ₁∪…∪τ_n.

The supremum type constructor.

See Also:

sup(Type[]), Type.compareTo(Object)

Postconditions:

RES == OLD(RES)

collection

Type collection(Type element)

The general collection type collection(τ). This is the supertype for all collections in the sense of mereology. The subtype relation extends to collection types as follows

c(τ) ≤ c'(τ') :⇔ c ≤ c' ∧ τ ≤ τ'
where for c the subtype relations are
collection ≤ list, collection ≤ set, collection ≤ bag

See Also:

list(Type), set(Type), bag(Type)

collection

Function collection()

collection: * → *; τ ↦ collection(τ).

The collection type constructor.

See Also:

collection(Type)

Postconditions:

RES == OLD(RES)

set

Type set(Type element)

The set type {τ}. Sets are orderless and contain unique elements.

Sets and predicates are different, i.e. {τ} ≠ (σ), because even though extensionally predicates correspond bijectively to sets, they may differ intensionally.

δ	predicate	→̃	set
	ρ	↦	{x ¦ ρ(x)}
	_∈M	↤	M

Also see identification with characteristic function.

See Also:

collection(Type), Set

set

Function set()

set: * → *; τ ↦ {τ}.

The set type constructor.

See Also:

set(Type)

Postconditions:

RES == OLD(RES)

list

Type list(Type element)

The list type ⟨τ⟩. Lists are ordered (but not sorted) and not limited to containing unique elements.

See Also:

collection(Type), List, product(Type[])

list

Function list()

list: * → *; τ ↦ ⟨τ⟩.

The list type constructor.

See Also:

list(Type)

Postconditions:

RES == OLD(RES)

bag

Type bag(Type element)

The bag/multiset type 〔τ〕. Bags are orderless and not limited to containing unique elements. So each element of a bag has a certain multiplicity.

See Also:

collection(Type)

bag

Function bag()

bag: * → *; τ ↦ 〔τ〕.

The bag type constructor.

See Also:

bag(Type)