4.10.1 Type Definitions

A type definition is of one of the forms (with the second being a type macro)

def type-name ::= type-expression

def type-name == type-expression

type-name is either an alphanumeric atom or a compound term whose arguments are distinct variables (each representing any type). A type definition with such a type name defines a parameterised type where the type variables stand for any type. Those type variables then appears in one or more of a disjunction of compound terms with other arguments that are type names. We give examples below.

4.10.1.1 Integer range type expression

This is an expression of the form M..N where M < N and both are integers.

Examples:

def digit ::= 0..9
def small_int ::= -10..10

As in the examples different range types may overlap but only when one is completely contained inside the other. To have overlapping sets of integers corresponding to different types, type union must be used (see below).

4.10.1.2 Enumeration of constants type expression

This is an expression of the form C1 | C2 | ... | Ck where each Ci is the same kind of constant, except that we can mix different types of numbers.

Examples:

def gender ::= male | female 
def threeNums ::= 20 | 6.7 | -50
def article ::= "a" | "an" | "one" | "the" | "that" | "those"

Different type definitions using overlapping disjunctions of constants are allowed providing one is completely contained inside the other. So, as well as the article type we could define

def indef_article::= "a" | "an" | "one"

It is possible to have an enumerated type with just one element as in

def def_article::= "the" 

A disjunction of integers can also overlap with a range type providing it either comprises a subset or a superset of the integers of the range type. These constraints ensure that each constant belongs to a unique minimal type. For example "a" would belong to the types indef_article, article, string, atomic, term.

To have partially overlapping disjunctions of constants corresponding to different types, type union expressions must be used to define each partially overlapping type (see below).

4.10.1.3 Enumeration of constructor type expression

This is an expression of the form CT1 | CT2 | ... | CTk where each CTi is a compound term with arguments that are type names, or type variables, or a parameterised type name. Such a type expression can only appear as the right hand side of a parameterised type definition with left hand side a compound term containing exactly the same type variables as appears on the right hand side.

Examples:

def tree(T) ::= empty() | tr(tree(T),T,tree(T))
def tree2(N,L) ::=  leaf(L) | node(tree2(N,L), N, tree2(N,L))
def an_indexed(T)::= rec(int,T)
def noun_exp_tree::= ne(adjective,noun_exp_tree) | n(noun)

Unlike type enumerations of atomics we do not allow type constructors to appear in multiple declarations and the functors of these constructors are not allowed to appear in any enumeration of atomics.

4.10.1.4 Type union expression

This is an expression of the form Ty1 || Ty2 || ... || Tyk where each Tyi a simple type name or a ground parameterised type name or a code type expression.

Examples:

def int_atom == int || atom

4.10.1.5 Code type expressions

There are four code type expressions in QuLog/TeleoR. These are: a function type, a relation type, and action type and a TeleoR procedure type.

4.10.1.6 Function type expression

This has the form fun(TE1,TE2,...,TEk) -> TE where each TEi and TE is any simple, or compound type name, or type union expression, or a code type expression. Functions must be called by giving ground arguments of the required types and will return a ground value of the specified value type.

Examples:

fun(set(T), set(T)) -> set(T)
fun(string) -> nat

The first example declares the type of a function that takes a pair of sets of some type and returns a set of the same type. The function union has this type.

The second example takes a string and returns a nat. The function # (when applied to a string) has this type.

4.10.1.7 Relation type expression

This has the form rel(MTE1,MTE2,...,MTEk) where each MTEi is a moded type where the type is any simple, or compound type name, or type union expression, or a code type expression.

The possible modes of a moded type are the prefixes !, ?, ?? and @.

The moded type !Type used as an argument of a relation means, when called, the supplied argument must be ground and of type Type.

The moded type ?Type used as an argument of a relation means, when called, the supplied argument may be variable or a partial or ground and of type Type. If not ground in the call it will be ground to a term of type Type by the call.

The moded type ??Type used as an argument of a relation means, when called, the supplied argument may be variable or a partial or ground and of type Type. It might not be ground on success of the call.

The moded type @term used as an argument of a relation means, when called, the supplied argument may be variable or a partial or ground term. It will be left unchanged by the call.

For relations and actions, if no (outer) mode is given it is taken to be !.

As we discuss in more detail in Modes and Moded Types, modes can be used multiple times in structured types as long as outer modes are more restrictive than inner modes. For example, the moded type

!list(?int)

means that the top-level list structure must be given (i.e. the number or elements are known at call time) but the elements of the list can be a mixture of integers and variables with the variables instantiated to integers by the call.

Examples:

rel(!list(T), !list(T), ?list(T))
rel(!string, ??term)

which can also be be given as

rel(list(T), list(T), ?list(T))
rel(string, ??term)

as ! is the default mode for static relation arguments.

The first example is the type of a relation whose first two arguments must be given as ground lists of values of the same type T and whose third argument can either be a variable or partial or ground list of values of type T that will be a ground list of T values if the relation call succeeds. This is one of the types of the append primitive. The second example is the type of a relation that takes a string as its first argument and whose second argument might be instantiated to a possibly non-ground term. This is the type of the string2term primitive.

If a mode is not given for an inner type it is taken to be the same as the outer mode - for example !list(T) is the same as !list(!T).

4.10.1.8 Action type expression

This has the form act(MTE1,MTE2,...,MTEk) where each MTEi is a moded type where the type is any simple, or compound type name, or type union expression, or a code type expression.

The modes are as for a relation type.

Examples:

act(??term, !handle)
act()

The first example is the type of an action that takes a term that may be a variable or contains variables and a ground handle. It is the type of the message send action to. The second example is the type of an action that takes no arguments. It is the type of kill_agent.

4.10.1.9 TeleoR procedure type expression

This has the form tel(TE1,TE2,...,TEk) where each TEi is any simple, or compound type name, or type union expression, or a code type expression. The types are implicitly ! ground input moded.

Example:

tel(list(block), slot)

This is the type of a TeleoR procedure that takes a list of blocks and a slot. This is the type of makeTower in one of the tower building programs in the examples directory where block and slot are user defined types.


On This Site