© Jrgen Steensgaard-Madsen, 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 first-order 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
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
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 n-1 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 n-1 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}.

Semantics of rings

[ rings OF w[Members OF 1 Ring ... : w] : w ]

Clause   Members of operation rings
A ring value can be considered a doubly-linked, circular list that can be manipulated by the means described below:
Clause   Body of operation ring

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.


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 switch-statement 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.
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.
Operation prj in the Operations clause of add:
Clause   Hit of operation prj
Operation case in the Operations clause of add:
Clause   Hit of operation case


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