Extensions to unification grammar for the description of programming languages.

Abstract

In the study of language, the notion of agreement plays a central part. For example, in English a noun phrase and a verb phrase that comprise a clause must agree in number and person; so we do not say "The rocks weighs too much." Likewise, in programming languages such as Pascal, we can not write "x: = f(y, z)" unless the identifiers x, f, y, and z have types that agree in the obvious way. That is, the importance of agreement in the study of language is not confined to natural language. In particular, there is an apparent similarity between agreement problems in natural languages and type problems in programming languages. This similarity raises a question of whether formal accounts of natural language agreement can be adapted to account for programming language type constraints as well. In this dissertation, we show, using ideas from unification grammar formalisms in computational linguistics, that this is indeed possible. Thereby we can explain, for example, the use of unification in polymorphic type inference, showing that such type inference is an instance of a pervasive linguistic phenomenon. In order to underst and how linguistic treatments of agreement can be adapted to programming languages, we investigate along three lines. First, we investigate mathematical properties of certain mathematical structures, called feature structures, that are used in unification grammars to model agreement between linguistic objects. Second, we develop formal languages (logics) EKR1 and EKR2 for describing feature structures. Third, we consider examples of how feature structures can be used to enforce type constraints seen as agreement constraints. We give an extended example of how the type constraints of a polymorphic programming language can be defined in the logic EKR2. The language is Milner's Exp. The example demonstrates the use of feature structures for describing complicated agreement constraints, and illustrates an affinity between programming language research and computational linguistics research.