A type is a class of objects that a diagram works with. In the set-theory example, Set is a type. The syntax for a type declaration is as follows:
For example, statement
type Set declares a type with name
Set. We can then use the name
Set to later refer to this type.
Conceptually, a type might be a subtype of another type. As an example, in a chemistry domain, types Hydrogen and Oxygen might both be subtypes of the type Atom. Penrose allows us to simultaneously declare a type and declare subtyping relations as follows:
type subtype_name <: supertype_name
Take the example of types Hydrogen, Oxygen, and Atom:
type Hydrogen <: Atom
type Oxygen <: Atom
If the types are already declared beforehand, just omit the
Hydrogen <: Atom
Oxygen <: Atom
Subtyping describes "is-a" relationships between types: a Hydrogen "is-a[n]" Atom; an Oxygen "is-a[n]" Atom. Using the "is-a" interpretation, since an Atom "is-a[n]" Atom, inherently, for all type
A, we have that
A is a subtype of
A. This interpretation of subtyping is consistent with "inheritance" in many object-oriented programming languages.
Penrose adopts this interpretation: if Penrose expects to see an object with type
A, then it will also accept an object of type
B, as long as
B is a subtype of
A. We say that "
The domain schema provides two built-in literal types,
Number, which represent string and numerical literals. These types can be inferred from literal expressions in substance and style.
These literal types can be referred to in other parts of the domain schema without declaration as arguments to predicates, functions, and constructors. For example, a domain schema about sets containing numbers can be described with
predicate Has(Set s, Number n)
Number is built-in so does not need to be declared.
Restrictions on Literal Types
Since these types are built-in, other type names cannot conflict with these literal types. That is, type declarations like
Since these literal types have special properties, they cannot be supertyped or subtyped. That is, we disallow declarations like
Set <: Number
String <: Set
Finally, literal types cannot be outputs of functions or constructors since they cannot be explicitly constructed, only inferred from literal expressions in substance and style. Hence we disallow declarations like
function addOne (Number n) -> Number