© Jørgen Steensgaard-Madsen, 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 [T1, T2,...,Tn] is short for
T1 T2 Tuple T3 Tuple ... Tn 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 non-zero arity.
An intuitive understanding of the nature of values of the various kinds is important, so here is a brief help
values can be thought of as fixed-size tables: elements are numbered sequentially upwards from 0 and on equal footing with respect to access time.
values are fixed-length sequences: the first element is the easiest to access, but elements can be accessed like entries in an array.
values can be thought of as pairs. Notation makes it possible to hide the pairing and describe for instance tripples and quadrouples.
values distinguish between presence and absence and has a component value only in the case of presence.
values can be thought of as hierarchies, i.e. pairs of node values and a list of (sub-)hierarchies.


Three categories of operators requesting operand values can be singled out: one consisting of 3-way 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 3-way comparison for as many types as possible. The operator symbol must be the same, and ?? has been chosen. So the first category amounts to The second category supports two special notations
  1. [ E1,E2,...,En ] is short for  E1::E2::...::En

  2. (E1,E2,...,En) is short for  E1 `,' E2 `,' ... `,' En
    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:
The final category consists of regular operators motivated by the type operator's properties.

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.


[ split_list OF U,W
     (L:U List)
     [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.


[ 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.


[ split OF A,W(X:A Option)
     [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.


[ 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


·Demo language
Implementation tool

General properties

Somefix operators
·Predefined type operators
Mutable variables
Functions for mathematics
File operations
Processes and connections
Misc. utilities
New type operators
Top-level entities

File translated from TEX by TTH, version 3.33.
On 18 Oct 2006, 16:47.
SourceForge.net Logo