Type Inference and Equational Theories
Andrew Kennedy. Technical report LIX/RR/96/09, École Polytechnique, September 1996.
The ML type system and inference algorithm are extended to incorporate equational theories of types. These are useful in formalising record type systems, numeric types with units of measure or dimensions, and type abbreviations or isomorphisms. Equational theories also have potential applications in type-based static analysis.
We build a general framework using many-sorted signatures and illustrate it with two concrete examples: a dimension type system and a novel approach to typing record operations based on the theory of Boolean rings. We prove that principal type schemes exist if (1) unification in the theory is unitary (all possible unifiers are instances of a single most general one) and (2) inferred types can be generalised to yield principal type schemes, a non-trivial procedure for many equational theories. The type inference algorithm therefore assumes the existence of a generalisation procedure with suitable properties; given this, we prove the soundness and completeness of the algorithm with respect to the typing rules. We also study in detail two formulations of the typing rule for let expressions, one based on expansion and the other on quantifier introduction.
CodeBricks: Code Fragments as Building Blocks
Guiseppe Attardi, Antonio Cisternino and Andrew Kennedy. In ACM SIGPLAN Workshop Partial Evaluation and Semantics-Based Program Manipulation, San Diego, California, June 2003. Published in SIGPLAN Notices, Vol. 38, No. 10, 306-314, October 2003.
We present a framework for code generation that allows programs to manipulate and generate code at the source level while the joining and splicing of executable code is carried out automatically at the intermediate code/VM level. The framework introduces a data type Code to represent code fragments: methods/operators from this class are used to reify a method from a class, producing its representation as an object of type Code. Code objects can be combined by partial application to other Code objects. Code combinators, corresponding to higher-order methods, allow splicing the code of a functional actual parameter into the resulting Code object. CodeBricks is a library implementing the framework for the .NET Common Language Runtime. The framework can be exploited by language designers to implement metaprogramming, multistage programming and other language features. We illustrate the use of the technique in the implementation of a fully featured regular expression compiler that generates code emulating a finite state automaton. We present benchmarks comparing the performance of the RE matcher built with CodeBricks with the hand written one present in .NET
Also see Antonio's CodeBricks project home page.