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.
ps
BibTeX:
@inproceedings{Nipkow-LF-91,
author="Tobias Nipkow",
title="Order-Sorted Polymorphism in {Isabelle}",
booktitle="Logical Environments",
editor="G\'erard Huet and Gordon Plotkin",
publisher=CUP,year=1993,pages="164--188"}