A Framework for User-friendly Declarative Typing Systems

Wolfram Kahl

Technical Report Nr. 9704, 15 pages
Fakultät für Informatik
Universität der Bundeswehr München
December 1997
(superseded by [Kahl-1998d])

Abstract

Advanced type systems frequently pose problems to the user, as can already be observed with the still rather simple type systems currently in use e.g. in Haskell or ML: error messages signaling type errors frequently give complex types and little clue where the real source of the error is.

We present a class of typing systems that are designed for online use, preventing input of untypeable constructs and guiding the user through the construction of programs with complex types. Since this implies making explicit the relation between programs and their types, the choice formalism for this purpose is that of term graphs, where much more program structure can usefully be made explicit than in linear notations.

After presenting a framework for the definition of typing systems in term graphs, we discuss the advantages of this approach and sketch applications to e.g. polytypic programming.


Wolfram Kahl --- 24 February 1999