[TYPES] Type inference and principal typings for record concatenation and mixin modules

[Henning Makholm]

We would like to announce a technical report and a web-accessible
software demonstration.

The technical report is:

   Type Inference and Principal Typings for
   Symmetric Record Concatenation and Mixin Modules

   by Henning Makholm and J. B. Wells

   http://www.macs.hw.ac.uk/~makholm/papers/bowtini-long.pdf

In this report we present a new type system, Bowtie, for a lambda
calculus with records and a symmetric record concatenation operation.
The system has been designed to allow feasible _type inference_
with a complexity of O(nm*alpha(n)) where n is the input size and m
the number of different field labels in the program, as well as
_compositional type inference_ and a notion of _principal typings_.

(Because alpha(n) <= 4 for n < 10^(10^100) (a googolplex), one can
think of this factor as a constant for practical purposes.)

Most previous type systems for record concatenation have relied on
subtyping polymorphism.  Bowtie does not, and because subtyping is
absent, we have been able to straightforwardly extend Bowtie to a type
system, Martini, for _mixin modules_.

Bowtie and Martini are both non-polymorphic type systems, but because
both have principal typings it is straightforward to extend either
with Milner's let-polymorphism, and we do so.

Apart from the definition of Bowtie and Martini we also present some
negative results ("things that don't work").  Most notable among these
is a series of proofs that the straightforward typing rule for a
record concatenation operator in an SML-like type system leads to an
NP-hard typability problem --- *even for the let-free (non-polymorphic)
fragment*, and *no matter whether the concatenation operator is
symmetric or asymmetric/overwriting*.

We have also made available a web-accessible type inference demo for
Bowtie/Martini; it can be found at

  http://www.macs.hw.ac.uk/DART/software/Bowtini/

We hope you enjoy our paper and web demo and we welcome any feedback.

-- 
Henning Makholm
Joe Wells