The Correctness of Type Specialisation

  • John Hughes
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1782)


Type specialisation, like partial evaluation, is an approach to specialising programs. But type specialisation works in a very different way, using a form of type inference. Previous articles have described the method and demonstrated its power as a program transformation, but its correctness has not previously been addressed. Indeed, it is not even clear what correctness should mean: type specialisation transforms programs to others with different types, so clearly cannot preserve semantics in the usual sense.

In this paper we explain why finding a correctness proof was difficult, we motivate a correctness condition, and we prove that type specialisation satisfies it. Perhaps unsurprisingly, type-theoretic methods turned out to crack the nut


Residual Program Specialisation Rule Partial Evaluation Logical Relation Residual Term 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


  1. 1.
    Zena Ariola, Matthias Felleisen, John Maraist, Martin Odersky, and Philip Wadler. A call-by-need lambda calculus. In 22’nd Symposium on Principles of Programming Languages, San Francisco, California, January 1995. ACM Press.Google Scholar
  2. 2.
    A. Bondorf. Automatic autoprojection of higher order recursive equations. Science of Computer Programming, 17(1–3):3–34, December 1991. Selected papers of ESOP’ 90, the 3rd European Symposium on ProgrammingzbMATHCrossRefGoogle Scholar
  3. 3.
    O. Danvy. Type-directed partial evaluation. In Symposium on Principles of Programming Languages. ACM, jan 1996.Google Scholar
  4. 4.
    D. Dussart, J. Hughes, and P. Thiemann. Type Specialisation for Imperative Languages. In International Conference on Functional Programming, pages 204–216, Amsterdam, June 1997. ACM.Google Scholar
  5. 5.
    Andrzej Filinski. A Semantic Account of Type-Directed Partial Evaluation. In Principles and Practice of Declarative Programming: International Conference PPDP’99, volume 1702 of Lecture Notes in Computer Science, pages 378–395, Paris, France, September 1999. Springer-Verlag.Google Scholar
  6. 6.
    C.K. Gomard. A self-applicable partial evaluator for the lambda calculus: Correctness and pragmatics. ACM Transactions on Programming Languages and Systems, 14(2):147–172, April 1992.CrossRefGoogle Scholar
  7. 7.
    John Hannan and Patrick Hicks. Higher-Order Arity Raising. In Proceedings of 3rd ACM SIGPLAN International Conference on Functional Programming, pages 27–38, Baltimore, Maryland, September 1998.Google Scholar
  8. 8.
    John Hannan and Patrick Hicks. Higher-Order UnCurrying. In Proceedings of the 25th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 1–10, San Diego, January 1998.Google Scholar
  9. 9.
    J. Hughes. An Introduction to Program Specialisation by Type Inference. In Functional Programming. Glasgow University, July 1996. published electronically.Google Scholar
  10. 10.
    J. Hughes. Type Specialisation for the Lambda-calculus; or, A New Paradigm for Partial Evaluation based on Type Inference. In O. Danvy, R. Glück, and P. Thiemann, editors, Partial Evaluation, volume 1110 of LNCS, pages 183–215. Springer-Verlag, February 1996.Google Scholar
  11. 11.
    J. Hughes. A Type Specialisation Tutorial. In DIKU Summer School on Partial Evaluation, 1998.Google Scholar
  12. 12.
    J. Hughes. Type Specialisation. In Olivier Danvy, Robert Glück, and Peter Thiemann, editors, 1998 Symposium on Partial Evaluation, volume 30 of Computing Surveys, September 1998.Google Scholar
  13. 13.
    N. D. Jones, C. K. Gomard, and P. Sestoft. Partial Evaluation and Automatic Program Generation. Prentice-Hall, 1993.Google Scholar
  14. 14.
    David MacQueen, Gordon Plotkin, and Ravi Sethi. An ideal model for recursive polymorphic types. Information and Control, 71(1/2):95–130, October/November 1986.zbMATHCrossRefMathSciNetGoogle Scholar
  15. 15.
    Eugenio Moggi. Functor categories and two-level languages. In FOSSACS, volume 1378 of Lecture Notes in Computer Science, pages 211–225. Springer-Verlag, 1998.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2000

Authors and Affiliations

  • John Hughes
    • 1
  1. 1.Chalmers University of TechnologyGöteborg

Personalised recommendations