Typechecking ABC Programs

Steven Pemberton, CWI, Amsterdam

Contents

The Programming Language ABC

• Simple
• Interactive
• Structured (data and program)
• Powerful
• Compact
• User-oriented
• No declarations, strongly typed

Environment

Dedicated environment:

• User defined commands and locations exist in a Workspace
• ABC is the command language
• Locations (variables) are used instead of files

Dedicated Editor:

• Knows the syntax and semantics of ABC
• Warns the user on the spot when an error is made

The Type System of ABC

Five kinds of type:

1. Numbers

   Unbounded, exact & approximate

2. Texts

   Unbounded length strings

3. Compounds

   Records without field names.

4. Lists

   Sorted bags, with elements of any one type.

5. Tables

   Finite mapping of keys of any one type onto items of any one type.

Compounds

PUT 0, -1 IN z

z is a compound with two numeric fields.

PUT 0, "zero" IN z

is a type error.

User Defined Commands

These are polymorphic:

HOW TO SWAP a WITH b:
    PUT a, b IN b, a

Functions

HOW TO RETURN cosh x:
    PUT exp x IN ex
    RETURN (ex+1/ex)/2

Global variables

HOW TO PUSH v:
   SHARE stack
   PUT v IN stack[#stack+1]

Example: a telephone list

>>> PUT {} IN tel
>>> PUT 4141 IN tel["Lambert"] 
>>> PUT 4071 IN tel["Leo"] 
>>> PUT 4138 IN tel["Frank"]
>>> WRITE tel["Leo"]
4071
>>> WRITE tel
{["Frank"]: 4138; ["Lambert"]: 4141; ["Leo"]: 4071}
>>> FOR name IN keys tel:
        WRITE name, ": ", tel[name]/
Frank: 4138 
Lambert: 4141 
Leo: 4071

(Telephone list, continued)

>>> PUT {} IN user
>>> FOR name IN keys tel:
        PUT name IN user[tel[name]]
>>> WRITE user[4141]
Lambert
>>> WRITE user
{[4071]: "Leo"; [4138]: "Frank"; [4141]: "Lambert"}

Representing Types

Consider the following commands:

PUT 0 IN a

a must therefore be a number

PUT a IN b

a and b are therefore the same type

WRITE t[b]

t is a table, whose keys have the same type as b

The (possibly incomplete) information about a type is represented by a polytype

Polytypes

A polytype can be

1. A name (ie otherwise unknown)
2. A text
3. A number
4. A list of some polytype
5. A table with keys of some polytype and associates of some polytype
6. A compound of some length, with that many polytypes as fields

Thus

a= Number
b= B (say)
t= Table(B,T)

The Algorithm

Each variable is given a polytype, initially just a name (ie unknown).

Whenever a line of source is processed it is analysed and new polytypes are created and unified with the existing ones.

Unification

Two polytypes are unified as follows:

• If one is a name all occurrences of that name in all existing polytypes is replaced by the other polytype.
• If neither is a name both must be of the same type (both text, or list etc)
• If both compounds, they must be of the same length.
• If both a list, table, or compound the algorithm is applied to the corresponding pairs of sub-polytypes.
• Otherwise, a type error has occurred.

An Example

Unify (Number, A, Number)
with (B, Table(C, D), C) from

PUT d IN t[c]
PUT 0, a, 0 IN b, t, c

They are both compounds of the same length so unify

1. Number, B
2. A, Table(C, D)
3. Number, C

From this,

1. gives
   (Number, A, Number)
   (Number, Table(C, D), C)
2. gives
   (Number, Table(C, D), Number)
   (Number, Table(C, D), C)
3. gives
   (Number, Table(Number, D), Number)
   (Number, Table(Number, D), Number)

And this is the unification, with the additional information that
A = T= Table(Number, D)
B = Number
C = Number

User Defined Commands

The algorithm as presented so far can be used to calculate the 'local' type requirements of a user defined command.

These are then 'projected' on to its parameters. Thus with

HOW TO SHOW s AT k: 
    WRITE s[k]

the polytype of SHOW is (Table(K, X), K).

When nothing is known about a command, its polytypes are all names.

Expressions and Functions

A function like

HOW TO RETURN cosh x: 
    PUT exp x IN ex
    RETURN (ex+1/ex)/2

can be treated as if it was

HOW TO COSH x GIVING y: 
    PUT exp x IN ex 
    PUT (ex+1/ex)/2 IN y

Similarly the use of an expression like

WRITE a**(i+1)

can be treated as

ADD i AND 1 GIVING tmp1 
RAISE a TO tmp1 GIVING tmp2 
WRITE tmp2

Special Features for ABC

Generic texts, lists and tables, e.g.

WRITE #t

FOR x IN t: WRITE x

PUT {} IN t

WRITE {a..b}

Adds new kinds of polytypes:

• text, list or table of T
• list or table of T
• number or text

Adds new rules to unification.

Implementation

Types are checked incrementally

• after each how-to definition
• when a how-to is loaded for execution.

The 'source' and code of an ABC program are represented by a single (threaded), largely abstract, tree.

Each node in the tree has an identifier, and a number of sub-nodes.

For instance, for a PUT command, you have

[ PUT | . | . ]
       /     \
     expr   address

Mini-Interpreters

Mini-interpreters for tasks not performed frequently, e.g.

• displaying the text of a how-to
• static checks, including the type check.

Code for mini-interpreters held as strings.

For instance, for displaying the put command:

PUT: "PUT 1 IN 2" 

The 1 and 2 refer to the corresponding sub-nodes.

Type Check Interpreter

Stack of polytypes kept.

Tree is processed by

• taking the identifier of the node
• indexing the interpreter's code table with this identifier
• executing the code it finds there.

This results usually in recursive analysis of the subtrees.

Example

For instance, for PUT we have:

PUT: "eeU"

e -- analyse and push the next subnode

U -- pop(x); pop(y); unify(x, y);

For the command

INSERT item IN list 

we have

INSERT: "e}eU"

} -- pop(x); push(listof(x))

List Displays

For the list display in

WRITE {1; 2; 3}

we have

List display: "e<eu>}"

< > -- loop over all sub-nodes

u -- pop(x); pop(y); push(unify(x, y));

For ranges in list displays, like

WRITE {a..b}

we have

range bounds: "e.ueu"

. -- push(text-or-number);

Table Displays

WRITE {[a]: b; ... }

has

table: "ee<~eu~eu>]"

~ -- swap top two elements on stack

]-- pop(a); pop(k); push(table(k, a));

For instance:

Op Stack
e: K 
e: KA 
~: AK 
e: AKE 
u: AK' 
~: K'A 
e: K'AE 
u: K'A'
   etc. 
]: Table(K', A') 

Conclusion

Incremental, interactive type checking

No declarations

Uses unification

Simple small interpreter for type checker