
© Jørgen SteensgaardMadsen, Copenhagen, 2006

Predefined type operators



Some globally bound type operators are described below. A number before a
type operator name tells how many types are needed to form a type of
the named kind  e.g. one type (the element type) is required to
determine a list type. The number is called the arity of the
type operator. No preceding number means zero, and such type
operators are often just called types.
int real complex string Text Output void NONE
1 Array 1 List 2 Tuple 1 Option 1 Tree
Usually some operations are strongly related to a type operator: those
necessary to build values of types derived from it, and those required
to recover components of such values.
Most types are given by type expressions in which a sequence of
operands precedes a type operator. The length of the sequence must be
equal to the arity of the type operator. Such expressions are said to
adhere to reverse Polish notation. Tuple types may also be
given by a special kind of expression:
Type [T_{1}, T_{2},...,T_{n}]
is short for
T_{1} T_{2} Tuple T_{3} Tuple
... T_{n} Tuple
It is frequently convenient to talk about a value of array type
without full information about the element type. We acknowledge that
it is somewhat sloppy, since an Array is a type operator, but
let convenience win sometimes. Likewise for other type operators of
nonzero arity.
An intuitive understanding of the nature of values of the various
kinds is important, so here is a brief help
 Array
 values can be thought of as fixedsize tables: elements
are numbered sequentially upwards from 0 and on equal footing with
respect to access time.
 List
 values are fixedlength sequences: the first element is
the easiest to access, but elements can be accessed like entries
in an array.
 Tuple
 values can be thought of as pairs. Notation makes it
possible to hide the pairing and describe for instance tripples and
quadrouples.
 Option
 values distinguish between presence and absence and
has a component value only in the case of presence.
 Tree
 values can be thought of as hierarchies, i.e. pairs of
node values and a list of (sub)hierarchies.
Operators
Three categories of operators requesting operand values can be singled
out: one consisting of 3way comparison, in terms of which binary
comparisons are defined generically, one that is motivated by giving
semantics of special notations in terms of operators, and one that is
just a convenient way of constructing or decomposing values.
An attempt has been made to define 3way comparison for as many types
as possible. The operator symbol must be the same, and ??
has been chosen. So the first category amounts to

[ ?? OF A {A??A}(A Option,A Option) : int ]
[ ?? OF A,B {A??A,B??B}([A,B],[A,B]) : int ]
[ ?? OF A {A??A}(A Array,A Array) : int ]
[ ?? OF aa {aa??aa}(aa List,aa List) : int ]
[ ?? OF A {A??A}(A Tree,A Tree) : int ]
The second category supports two special notations
 [ E_{1},E_{2},...,E_{n} ]
is short for
E_{1}::E_{2}::...::E_{n}

(E_{1},E_{2},...,E_{n})
is short for
E_{1} `,' E_{2} `,' ... `,' E_{n}
The comma is not by itself recognised as an operator, but
special operator symbols can be defined as quoted.
It should be noted that these meanings are purely syntactic. These
operator symbols may be overloaded, so for instance the actual meaning
of a bracketed list of expressions depends on the identified meaning
of the :: operator. Thus we just need the signatures of the
operators:

[ :: OF aa (aa,aa List) : aa List ]
[ `,' OF A,B (A,B) : [A,B] ]
The final category consists of regular operators motivated by the
type operator's properties.

[ ~ OF A,B {A~string,B~string}([A,B],string) : Text ]
Generalises Text formatting from single values to tuples.

[ > OF W (int,W List) : W Array ]
Constructs an Array value from a length and a list.
e.g. 4>[1,2,3] is equal to 4>[1,2,3,1]
which is also the output format

[ @ OF W (W Array,int) : W ]
Evaluation of a@i finds the ith element of a

[ @ OF aa (aa List,int) : aa ]
Likewise: the ith element of list a

[ ::= OF lval,rval {lval:=rval List}(lval,rval) : rval List ]
x ::= y is short for x := y :: x 
which is unsystematic, but the only reasonable analogy to e.g. +=
Operation overview
An operation signature associates a name with a list of
clause descriptions
and possibly a result type. An application of an operation is
called
a command.
Function arguments are simple examples of clauses, as are the
branches of a conditional command. In more complex cases a
clause may be the scope of some
descendants
of the command operation. Different clauses will usually have
different descendants.
A clause description is a signature itself: it associates a name
of the clause with a list of signatures of descendants.
Detailed information about the language of signatures and commands
will have to be found elsewhere.

[ array_length OF u(l:u Array) : int ]
array_length(x) returns the number of entries in x

[ list_length OF u(l:u List) : int ]

[ hd OF U(l:U List) : U ]

[ tl OF U(l:U List) : U List ]
For all nonempty list values: x == hd(x) :: tl(x)

[ nil OF a : a List ]
nil is an empty list, which can also written [ ]

[ split_list OF U,W
(L:U List)
[Nil:W]
[Cons ... : W] : W ]
For all list values: L==split_list(L,[ ],hd::tl)
L is the list value to inspect
NIL is a computation of result when L is empty
Cons is a computation of result when L is nonempty

[ list OF U(Composition ... : U List) : U List ]
Alternative notation for lists:
list([E_{0},E_{1},... ])

[ fst OF A,B(x:[A,B]) : A ]
[ snd OF A,B(x:[A,B]) : B ]
For all tuple values: P == (fst(P),snd(P))

[ none OF A : A Option ]
[ some OF A(X:A) : A Option ]
[ split OF A,W (X:A Option)
[None:W]
[Some ... : W] : W ]
For all option values: X == split(X,none,some(x))

[ tree OF A(X:A, D:A Tree List) : A Tree ]
[ node OF A,W
(N:A Tree)
(Split ... : W) : W ]
For all tree values: X == node(X,tree(data,children))
Semantics
[ split_list OF U,W
(L:U List)
[Nil:W]
[Cons ... : W] : W ]
Application of split_list combines case distinction and avoids
recomputation of list components, which can be convenient in many
cases, e.g.
induction (L) P(split_list(P,1,hd*result(tl)))
which may be compared to
induction (L) P(if(P==[],1,hd(P)*result(tl(P))));
Clause: Cons of operation split_list
Should compute a result for L == hd::tl where hd and
tl have signatures as follows. Note that the names are the
same as the function names for decomposition  which may be disturbing.
Semantics
[ list OF U(Composition ... : U List) : U List ]
Since the [...] notation depends on the meaning of operator
:: it can be necessary to temporarily redefine it to build a
list, if some other current meaning is defined in the context.
Clause: Composition of operation list
Forms a context where nil denotes a list, which suffices to
make operator :: denote a list operation.
Semantics
[ split OF A,W(X:A Option)
[None:W]
[Some ... : W] : W ]
Remember the characterisation: X == split(X,none,some(x)) .
Clause: Some of operation split
Should compute a result for values that are present.

( x : A )
Identifies the present value.

( __ : A )
Default value of a label, same as x
Semantics
[ node OF A,W
(N:A Tree)
(Split ... : W) : W ]
Find a result for a tree by utilising the tree value property:
t == node(t,tree(data,children))
The Split clause
gives access to the components by the signatures
Contents
File translated from
T_{E}X
by
T_{T}H,
version 3.33.
 On 18 Oct 2006, 16:47.

 