Type specialisation is an approach to program specialisation that works
with both a program and its type to produce specialised versions of
them. Its main contribution is the ability to express optimal
specialisation for interpreters written in typed languages -- a problem
that was open for almost ten years --, but it also provides a
combination of other powerful features, making type specialisation a
good framework for automatic program production.
The original specification of type specialisation by John Hughes used a
system of rules expressing it as a generalised type system, rather than
the usual view of specialisation as generalised evaluation. That system,
while powerful, has some drawbacks -- the most important being the
inability to express principal type specialisations. A principal
specialisation is one that is ``more general'' than any other for a
given term, and from which those can be obtained by a suitable notion of
instantiation.
In this talk I will present my work on type specialisation. I will
discuss a different formulation of the system specifying type
specialisation, extended to fix some of those problems, and to capture
the notion of principality. I will give a precise definition of the
notion of ``more general'', and of the notion of instantiation needed. I
will sketch a proof of the existance of principal specialisations.