Type classes and overloading in higher-order logic

  • Markus Wenzel
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1275)


Type classes and overloading are shown to be independent concepts that can both be added to simple higher-order logics in the tradition of Church and Gordon, without demanding more logical expressiveness. In particular, model-theoretic issues are not affected. Our metalogical results may serve as a foundation of systems like Isabelle/Pure that offer the user Haskell-style order-sorted polymorphism as an extended syntactic feature. The latter can be used to describe simple abstract theories with a single carrier type and a fixed signature of operations.


Type Class Deductive System Class Definition Type Definition Type Constructor 
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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    P. B. Andrews. An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof. Academic Press, 1986.Google Scholar
  2. 2.
    A. Church. A formulation of the simple theory of types. Journal of Symbolic Logic, pages 56–68, 1940.Google Scholar
  3. 3.
    M. J. C. Gordon. Set theory, higher order logic or both? In Proc. 9th TPHOLs, volume 1125 of Lecture Notes in Computer Science, pages 191–201. Springer-Verlag, 1996.Google Scholar
  4. 4.
    M. J. C. Gordon and T. F. Melham (editors). Introduction to HOL: A theorem proving environment for higher order logic. Cambridge University Press, 1993.Google Scholar
  5. 5.
    L. Henkin. Completeness in the theory of types. Journal of Symbolic Logic, 15(2):81–91, 1950.Google Scholar
  6. 6.
    P. Hudak, S. L. P. Jones, and P. Wadler (editors). Report on the programming language Haskell, a non-strict purely functional language (Version 1.2). SIGPLAN Notices, March, 1992.Google Scholar
  7. 7.
    The Isabelle library. Scholar
  8. 8.
    M. P. Jones. Qualified Types: Theory and Practice. PhD thesis, University of Oxford, 1992.Google Scholar
  9. 9.
    T. Nipkow. Order-sorted polymorphism in Isabelle. In G. Huet and G. Plotkin, editors, Logical Environments, pages 164–188. Cambridge University Press, 1993.Google Scholar
  10. 10.
    T. Nipkow and C. Prehofer. Type checking type classes. In 20th ACM Symp. Principles of Programming Languages, 1993.Google Scholar
  11. 11.
    L. C. Paulson. The foundation of a generic theorem prover. Journal of Automated Reasoning, 5(3):363–397, 1989.Google Scholar
  12. 12.
    L. C. Paulson. Isabelle: A Generic Theorem Prover, volume 828 of Lecture Notes in Computer Science. Springer-Verlag, 1994.Google Scholar
  13. 13.
    A. Pitts. The HOL logic. In Gordon and Melham [4], pages 191–232.Google Scholar
  14. 14.
    M. Schmidt-Schauß. Computational Aspects of an Order-Sorted Logic with Term Declarations, volume 395 of Lecture Notes in Artificial Intelligence. Springer-Verlag, 1989.Google Scholar
  15. 15.
    M. Wenzel. Using axiomatic type classes in Isabelle — a tutorial. Available at Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1997

Authors and Affiliations

  • Markus Wenzel
    • 1
  1. 1.Institut für InformatikTechnische Universität MünchenMünchenGermany

Personalised recommendations