Typing Declarations

Appeared in Volume 8/2, May 1995

thomasl@arnold.csd.uu.se
Thomas Lindgren
25th November 1994

One of the pains of Goedel is that you must write type declarations for every procedure, which is the same as type declaring each case statement or while-loop in an imperative language.

Goedel programs, from what I have seen and my few own programming examples, seem to consist of equal parts of type declarations and program. A language such as the recently proposed Mercury have even more declarations: in the paper I read, a toy example had 14 lines of declarations and 4 lines of program code.

While the information is used for a worthy purpose, I personally find this excessive, and would much prefer type inference or soft typing to reduce the amount of declarations to just declaring type definitions (not predicate types) and/or typing selected predicates. This has been done for Scheme (e.g., Andrew Wright's thesis) and for the object-oriented Cecil (Craig Chambers and students).

Finally, maybe the Mycroft-O'Keefe type checker can be useful to those who want strong typing for their Prolog programs. I also seem to recall a Typed Prolog, but cannot remember where either of the above two may be found. Doesn't NU-Prolog provide various forms of typing as well? The advantage is again that you can mix statically and dynamically typed program development to your own taste.

winikoff@munta.cs.mu.oz.au
Michael David Winikoff
6th December 1994

Thomas Lindgren) writes:
One of the pains of Goedel is that you must write type declarations for every procedure, which is the same as type declaring each case statement or while-loop in an imperative language.

One of the worthy purposes is documentation.

Functional languages such as Haskell/Gofer/Miranda/SML do type inference so in theory you never have to declare types. It is, however, good practice to include the types explicitly - it doesn't take any extra thinking (if you don't know what the types of your functions are odds are they don't have consistant types).

Types also make good documentation and can help the type inferencer pinpoint errors.

conway@munta.cs.mu.oz.au
Thomas Charles Conway
6th December 1994

Thomas Lindgren writes:
A language such as the recently proposed Mercury had even more declarations

The following figures were produced from the current compiler sources.

Predicate declaration lines: 	2884
Mode declaration lines:	2278
Type declaration lines:	1069
Inst declaration lines: 	45
Module declaration lines:	895
				----
Total declaration lines:	7171

Code lines:	23353

Well, you get what you pay for. You choose - either pay the cost once and spend an extra ten seconds for each predicate typing the declaration (if you're writing the predicate, you usually know what types you want it to operate on, and in which modes you want it to operate) and let the compiler find the errors, or spend an extra ten to 100 minutes in the debugger sweating blood to find the errors yourself.

fjh@munta.cs.mu.oz.au
Fergus Henderson
10th December 1994

I've heard several people make the point that type declarations supposedly make maintenance more difficult, because you may need to change the type declarations too. But my experience is very much the opposite - type declarations make maintenance much easier.

In Prolog, modifications such as adding a new argument to a predicate, changing the order of arguments to a predicate, or changing the way data is represented all require careful and painstaking searches through the entire source code to find every place where that predicate is called or where that data structure is used. The process is slow, tedious and very error-prone.

In Mercury I regularly make program modifications that would be extremely difficult without the compiler's help. The type-checker can quickly pinpoint all the parts of the program that need modifying as a result of a change. I often still use "grep" to help locate those parts before running the program through the compiler, but I can do it much more quickly and easily since I know that if I make a mistake, the compiler will find it for me anyway.