5.2 Built In Types

Below we list the builtin term types giving the subtype relation (<) between the types.

nat < int < num < atomic < term
string < atomic
list(Type) < term
set(Type) < term
atom_naming(CodeType) < atom < atomic
atom_naming(CodeType) < term_naming(CodeType) < term
(Type1, ..., Typen) < term
typeE(Type) < term

The type term is the top type - all QuLog terms have type term.

The natural numbers have type nat, the integers have type int and the integers together with the floats have type num.

QuLog strings (which are like C strings as opposed to lists of ASCII codes) are of type string.

The QuLog atoms (the same as Prolog atoms) are of type atom.

The numbers, atoms and strings together are of type atomic.

The type list(Type) is the type of a list whose elements are of type Type.

The type set(Type) is the type of a set whose elements are of type Type.

In QuLog sets and lists are different data structures.

The types atom_naming and term_naming are respectively the types of atoms and terms that name code. For example, in examples/introduction/qlexamples.qlg we define the function curry and so in the interpreter with the file consulted we get

| ?? X = curry.

X = curry : atom_naming(fun(fun(Ty1, Ty2) -> Ty3) ->
                        fun(Ty1) -> fun(Ty2) -> Ty3)

| ?? X = curry(+)(1.3).

X = curry(+)(1.3) : term_naming(fun(num) -> num)

A tuple in QuLog is a term of the form (Term1,..., Termn) and has type (Type1,..., Typen) where Termi has type Typei

The special type typeE(Type) is used for giving the type of a type. For example, in the interpreter,

| ?? X = nat.

X = nat : typeE(nat)

QuLog variables can be used in type declarations to represent a polymorphic type (as is reflected in the curry example above).

The code types form another collection of types as listed below.

• function type: fun(Type1, ..., Typen) -> Type
• relation type: rel(ModedType1, ..., ModedTypen)
• action type: act(ModedType1, ..., ModedTypen)
• TR procedure type: tel(Type1, ..., Typen)

Because we can give multiple types to code we get, on giving the types, an intersection type with each type separated by && as in the following variation of the earlier example involving curry.

| ?? X = curry(+)(1).

X = curry(+)(1) : term_naming(fun(int) -> int &&
                              fun(num) -> num &&
                              fun(nat) -> nat)

From the programmers point of view giving multiple declarations is declaring an intersection type - the programmmer doesn’t use && in declarations.

Note that for functions we use the fun wrapper rather than as is done in functional languages where we might write something like

((Ty1, Ty2) -> Ty3) -> Ty1 -> Ty2 -> Ty3

We do this for pragmatic reasons - in our context using the functional approach makes it difficult for us to distinguish between a function with multiple arguments and a function with a single argument that is a tuple - instead we simply have, for example

fun(int, int) -> int
fun((int, int)) -> int