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