**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.