A Rewriting Logic Approach to Type Inference

This work has been published as an extended abstract and as a selected paper in a workshop proceedings (WADT'08) and in a technical report. These papers explain how one can use K to define and prove properties about type systems and inferencers.

A Rewriting Logic Approach to Type Inference
Chucky Ellison, Traian Florin Serbanuta and Grigore Rosu
WADT'08, LNCS 5486, pp 135-151. 2009
Abstract. Meseguer and Roșu proposed rewriting logic semantics (RLS) as a programing language definitional framework that unifies operational and algebraic denotational semantics. RLS has already been used to define a series of didactic and real languages, but its benefits in connection with defining and reasoning about type systems have not been fully investigated. This paper shows how the same RLS style employed for giving formal definitions of languages can be used to define type systems. The same term-rewriting mechanism used to execute RLS language definitions can now be used to execute type systems, giving type checkers or type inferencers. The proposed approach is exemplified by defining the Hindley-Milner polymorphic type inferencer $\mathcal{W}$ as a rewrite logic theory and using this definition to obtain a type inferencer by executing it in a rewriting logic engine. The inferencer obtained this way compares favorably with other definitions or implementations of $\mathcal{W}$. The performance of the executable definition is within an order of magnitude of that of highly optimized implementations of type inferencers, such as that of OCaml.

Technical Report

A Rewriting Logic Approach to Type Inference
Chucky Ellison, Traian Florin Serbanuta and Grigore Rosu
Technical report UIUCDCS-R-2008-2934, March 2008

Abstract. Meseguer and Rosu proposed rewriting logic semantics (RLS) as a programming language definitional framework that unifies operational and algebraic denotational semantics. Once a language is defined as an RLS theory, many generic tools are immediately available for use with no additional cost to the designer. These include a formal inductive theorem proving environment, an efficient interpreter, a state space explorer, and even a model checker. RLS has already been used to define a series of didactic and real languages, but its benefits in connection with defining and reasoning about type systems have not been fully investigated yet.

This paper shows how the same RLS style employed for giving formal definitions of languages can be used to define type systems. The same term-rewriting mechanism used to execute RLS language definitions can now be used to execute type systems, giving type checkers or type inferencers. Since both the language and its type system are defined uniformly as theories in the same logic, one can use the standard RLS proof theory to prove properties about languages and type systems for those languages.

The proposed approach is exemplified by defining Milner's polymorphic type inferencer W as a rewrite logic theory and using the definition: (1) to prove its soundness using Wright and Felleisen's standard preservation and progress methodology, and (2) to obtain a type inferencer by executing the definition in the Maude rewrite engine. The inferencer obtained "for free" was tested against implementations used in some current functional languages. It was found to be quite competitive---for example, it outperformed SML's type inferencer in all experiments.

To show that the proposed rewriting approach and the resulting type inferencers scale, Milner's simple language is extended with multiple-binding let and letrec, with lists, and with references and side effects. The resulting type inferencer, able to detect weak polymorphism, is only slightly slower than the one for Milner's simpler language. No proofs are given for the extended type system.

PDF, TR@UIUC, BIB