next up previous contents index
Next: Statements and Definitions Up: Introduction to Type Previous: Relationship to Set

Relationship to Programming Languages

In many ways the formalism presented here will resemble a functional  programming language with a rich type structure. The functions of are denoted by lambda  expressions, written x.t, and correspond to programs. The function terms do not carry any type information, and they are evaluated without regard to types. This is the evaluation style of ML [Gordon, Milner, & Wadsworth 79],  and it contrasts with a style in which some type correctness is checked at runtime (as in PL/I).  The programs of are rather simple in comparison to those of modern production languages; there is no concurrency,  and there are few mechanisms to optimize the evaluation (such as alternative parameter passing mechanisms, pointer allocation schemes, etc.).

The type structure of is much richer than that of any programming language; for example, no such language offers dependent products, sets, quotients and universes. On the other hand, many of the types and type constructors familiar from languages such as Algol 68,  Simula 67,  Pascal  and Ada  are available in some form in

. We discuss this briefly below.

A typical programming language will have among its primitive types the integers, int, booleans, bool, characters, char, and real numbers (of finite precision), real. In the type of integers, int, is provided; the booleans  can be defined using the set type as {x:int | x=0 in int or x=1 in int}, the characters are given by atom, and various kinds of real numbers can be defined (including infinite precision), although no built--in finite  precision real type is as yet provided.

Many programming languages provide ways to build tuples of values. In Algol the constructor is the structure;  in Pascal  and Ada  it is the record  and has the form for the product of types A and B. In such a product would be written A#B just as it would be in ML. 

In Pascal the variant  record has the following form.

        CASE kind:(RECT,TRI,CIRC) of
            TRI :(x,y,a:real)
The elements of this type are either pairs, triples or quadruples, depending on the first entry. If the first entry is RECT then there are two more components, both reals. If the first entry is CIRC then there is only one other which is a real; if it is TRI then there are three real components. One might consider this type a discriminated  union rather than a variant record. In any case, in it is defined as an extension of the product operator which we call a dependent product.  If real denotes the type of finite precision reals, and if the Pascal type (RECT,CIRC,TRI) is represented by the type consisting of the three atoms "RECT","CIRC" and "TRI", and if the function F is defined as
        F("RECT") = real#real
        F("CIRC") = real
        F("TRI")  = real#real#real
then the following type represents the variant record.

In , as in Algol 68 , it is possible to form directly the disjoint union , written A|B, of two types A and B. This constructor could also be used to define the variant record above as real#real|(real|real#real#real).

One of the major differences between types and those of most programming languages is that the type of functions from A to B, written A->B, denotes exactly the total   functions. That is, for every input a of type A, a function in A->B must produce a value in B. In Algol the type of functions from A to B, say PROC(x:A)B, includes those procedures which may not be well--defined on all inputs of A; that is, they may diverge on some inputs.

In contrast to the usual state of affairs with programming languages the semantics of ``programs'' is completely formal. There are rules to settle such issues as when two types of programs are equal, when one type is a subtype of another, when a ``program'' is correctly typed, etc. There are also rules for showing that ``programs'' meet their specifications. Thus is related to programming languages in many of the ways that a programming  logic or program  verification system is.

next up previous contents index
Next: Statements and Definitions Up: Introduction to Type Previous: Relationship to Set

Richard Eaton
Thu Sep 14 08:45:18 EDT 1995