Order-Sorted Polymorphism in Isabelle

Tobias Nipkow

ML-style polymorphism can be generalized from a single-sorted algebra of types to an order-sorted one by adding a partially ordered layer of ``sorts'' on top of the types. Type inference proceeds as in the Hindley/Milner system, except that order-sorted unification of types is used. The resulting system has been implemented in Isabelle to permit type variables to range over user-definable subsets of all types. Order-sorted polymorphism allows a simple specification of type restrictions in many logical systems. It accommodates user-defined parametric overloading and allows for a limited form of abstract axiomatic reasoning. It can also explain type inference with Standard ML's equality types and Haskell's type classes.




author="Tobias Nipkow",
title="Order-Sorted Polymorphism in {Isabelle}",
booktitle="Logical Environments",
editor="G\'erard Huet and Gordon Plotkin",