page 1  (22 pages)
2to next section

Partial Type Assignment
Left Linear Applicative Term Rewriting Systems?

Theory, Applications and Implementation.

Steffen van Bakel1y Sjaak Smetsers1 Simon Brock2

1) Department of Informatics, Faculty of Mathematics and Informatics, University of Nijmegen, Toernooiveld 1, 6525 ED Nijmegen, The Netherlands.
2) School of Information Systems, University of East Anglia, Norwich NR4 7TJ, United Kingdom.


This paper introduces a notion of partial type assignment on left linear applicative term rewriting systems that is based on the extension defined by Mycroft of Curry's type assignment system. The left linear applicative TRS we consider are extensions to those suggested by most functional programming languages in that they do not discriminate against the varieties of function symbols that can be used in patterns. As such there is no distinction between function symbols (such as append and plus) and constructor symbols (such as cons and succ). Terms and rewrite rules will be written as trees, and type assignment will consist of assigning types to function symbols, nodes and edges between nodes. The only constraints on this system are imposed by the relation between the type assigned to a node and those assigned to its incoming and out-going edges. We will show that every typeable term has a principal type, and formulate a needed and sufficient condition typeable rewrite rules should satisfy in order to gain preservance of types under rewriting. As an example we will show that the optimisation function performed after bracket abstraction is typeable. Finally we will present a type check algorithm that checks if rewrite rules are correctly typed, and finds the principal pair for typeable terms.


In the recent years several paradigms have been investigated for the implementation of functional programming languages. Not only the lambda calculus [Barendregt '84], but also term rewriting systems [Klop '92] and graph rewriting systems [Barendregt et al. '87] are topics of research. Lambda calculus (or rather combinator systems) forms the underlying model for the functional programming language Miranda [Turner '85], term rewriting systems are used in the underlying model for the language OBJ [Futatsugi et al. '85], and graph rewriting systems is the model for the language Clean [Brus et al. '87, N?ocker et al. '91].

There exists a well understood and well defined notion of type assignment on lambda terms, known as the Curry type assignment system [Curry & Feys '58]. This type assignment system is the basis for many type checkers and inferers used in functional programming languages. For example the type assignment system for the language ML [Milner '78], as defined by R. Milner forms in fact an extension of Curry's system. The type inference algorithm for the functional programming language Miranda works in roughly the same way as the one for ML. A real difference between ?Supported by the Esprit Basic Research Action 3074 ?Semagraph?.
yPartially supported by the Netherlands Organisation for the advancement of pure research (N.W.O.).