Type Declarations
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:
type typename
This statement declares a type with name typename
. After declaration, a type can be referred to in other parts of the Domain schema, as well as the Style and Substance schemas.
For example, statement type Set
declares a type with name Set
. We can then use the name Set
to later refer to this type.
Subtypes
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 Atom
type Hydrogen <: Atom
type Oxygen <: Atom
If the types are already declared beforehand, just omit the type
keyword:
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 "B
matches A
."
Literal Types
The domain schema provides two built-in literal types, String
and 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
type Set
predicate Has(Set s, Number n)
Notice that 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
type Number
type String
are disallowed.
Since these literal types have special properties, they cannot be supertyped or subtyped. That is, we disallow declarations like
type Set
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