
© Jørgen SteensgaardMadsen, Copenhagen, 2006

New type operators



The following type operators are defined internally for all
Howard languages:
void int real string Text Output void NONE
Other type operators are globally bound, with predefined support
in some contributions. 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.
Input complex 1 Array 1 List 2 Tuple 1 Option 1 Tree
Additional type operators can be supported by operations that can be
seen as classes that packages introduction of one or more type
operators and a small number of related operations that form a
sufficient basis for further work.
Some operations of this kind are described below. Beware that some
have an experimental character.
Operation overview
Semantics of sets
Finite sets of firstorder values (excluding computations as elements)
is a useful notion, although it should be used with caution in
practice because of inherent implementation difficulties. It is
especially useful for experimentation and prototyping.
[ sets OF W[Support OF 1 Set ... : W] : W ]
Clause Support of sets

[ empty OF A : A Set ]
[ :: OF A {A??A}(A,A Set) : A Set ]
[ @ OF A {A??A}(A Set,A) : int ]
[ ?? OF A {A??A}(A Set,A Set) : int ]
[ << OF A {Output<<A}(Output,A Set) : Output ]
[ set OF A[Body ... : A Set] : A Set ]
[ __ OF A[Body ... : A Set] : A Set ]
[ setind OF A,T(S:A Set,Base:T)
[Step ... : T] : T ]
Sets can be constructed from the empty set by inclusion of
elements one at a time using the :: operator.
The @ operator supports test for membership of a set, and
?? is the conventional 3way comparison for sets  which
of course requires a similar comparison operator for element values.
The << operator displays a value as set([...])
which can be used later as a constant in another expression.
The setind operation supports computations in close analogy
with induction over finite sets.
Operations set and __ in the Support
clause of sets:
The default meaning of a label of support is the same as that of
operation set.
Clause Body of operation set and __
The special notation [...] can be used for sets here

( nil : A Set )
the empty set, which causes the expanded version of [...] to
use the setmeaning of ::  admittedly fairly tricky.
Operation setind in the Support clause of sets:
[ setind OF A,T(S:A Set,Base:T)[Step ...: T ] : T ]
Induction over a finite sets is a specialised version of mathematical
induction over natural numbers: if an assumption based on sets of size
n1 generalises can be proved to imply the assumption for sets of
size n, and the assumption is valid for the empty set, then the
assumption is valid for all sets. This pattern can be used for
computations to make correctness almost obvious: Base
provides a value for an empty set and the Step generalises
from sets of size n1 to size n.
Clause Step of operation setind
Based on an assumed result for a set s and an element e not in
s, find a result for set sÈ{e}.

( e : A )
[ rest : T ]
rest is the (assumed) result for a set s Î S not
containing e.
Semantics of rings
[ rings OF w[Members OF 1 Ring ... : w] : w ]
Clause Members of operation rings
A ring value can be considered a doublylinked, circular list that can
be manipulated by the means described below:

[ @ OF T (T Ring,int) : T ]
[ :: OF T (T,T Ring) : T Ring ]
[ << OF T {Output<<T}(Output,T Ring) : Output ]
[ ?? OF T {T??T}(T Ring,T Ring) : int ]
[ ring OF T[Body ... : T Ring] : T Ring ]
[ hd OF T(X:T Ring) : T ]
[ tl OF T(X:T Ring) : T Ring ]
[ length OF T(X:T Ring) : int ]
[ next OF T(X:T Ring) : T Ring ]
[ prev OF T(X:T Ring) : T Ring ]
[ rev OF T(X:T Ring) : T Ring ]
The design is closely related to that of sets described
above, but some operators differ by modifying a ring value given as
operand.
The @ operator allows an element value to be retrieved by
indexing as in a list. The :: operator modifies its right
operand by inserting the left operand as new element 0.
Operators << and ?? are used for output and 3way
comparison in conventional manner.
Operation ring allows a ring value to be computed as
ring([...]) using the same trick as for sets.
Properties:
hd(x) == x@0
{with(length(y)) n; length(ring(x::y)) == 1+n}
{with(hd(x)) h; h::tl(x) == x}
{with(x) y; next(x)@i == y@(i+1)}
next(prev(x)) == x
{with(x) y; rev(x)@i == y@(length(y)1i)}
Note that the modifying operators leads to cumbersome statement of
properties.
Clause Body of operation ring

[ nil : T Ring ]
Denotes an empty ring and implies :: to be disambiguated as a
ring operator in the Body clause.
Semantics of union
The union of two sets contain both as subsets, but its number of
elements may be smaller than the sum of elements in the original two.
A disjoint sum, or discriminated union, likewise contains subsets that
match the sets used to build it, but these are disjoint. Typically a
tag is used with a unique value for each subset in a representation.
[ union OF W[Usage OF SUM ... : W] : W ]
Clause Usage of operation union
Provides a context in which a new, unique type is defined in addition
to the operation add illustrated above. Further computation
should occur in a Members clause of add, probably
the innermost one in a nest of applications of add.
Clause Members of operation add
Computes a final result of application of add. Usually
Members clauses nest and the result obtained in the innermost
clause tricles out to the outermost.
Each Members clause provides its own means to inject into and
extract from SUM.
Clause Match of operation prj :
Of course the clause should provide access to the value injected into
type SUM. In this case the design has opted to encourage use
of a clause label  i.e.c and p above.
Semantics
As mentioned above, sumtype is an alternative design for
disjoint sums.
[ sumtype OF T[Members OF SUM ... : T] : T ]
Clause Members of operation sumtype
Operation switch in the Members clause of sumtype:
Application of switch is designed to be similar to the
switchstatement found in the programming language C. Technically, a
tag associated with the actual value of X is extracted
internally, but not disclosed externally.
Clause Branching of operation switch
Note that a case operation is not introduced by
switch.

[ break ]
Terminates computation of switch.
Operation add in the Members clause of sumtype:
Clause Operations of operation add
Operation add provides operations to generate values of type
SUM and to check if a given SUM value was generated in
this way.

[ __(X:A) : SUM ]
The meaning of a label of an Operations clause is a mapping
of A values into SUM values.

[ prj OF W
(X:SUM)
[Hit ... : W]
[Miss:W] : W ]
Tests if a value of type A corresponds to X and if
so evaluates the Hit clause; otherwise the Miss
clause is evaluated.

[ case OF W[Hit ... : W] : W ]
Tests if the tag extracted by switch matches that for type
A. An example should clarify the rôle of type A:
{ sumtype;
add cartesian;
add polar;
with (cartesian((1.,1.))) u;
switch (u) {
cartesian.case c{ stdout << ~"Cartesian: " << c << nl };
polar.case p{ stdout << ~"Polar:" ... }
}
};
Operation prj in the Operations clause of add:
Clause Hit of operation prj

( __ : A )
The meaning of a label of a Hit clause is the A
value used to generate the inspected SUM value.
Operation case in the Operations clause of add:
Clause Hit of operation case

( __ : A )
The meaning of a label of a Hit clause is the A
value used to generate the inspected SUM value.
Contents
File translated from
T_{E}X
by
T_{T}H,
version 3.33.
 On 18 Oct 2006, 16:47.

 