An abstract interpretation for ML equality kinds

Carl A. Gunter, Elsa L. Gunter, David B. MacQueen

Research output: Chapter in Book/Report/Conference proceedingConference contribution


The definition of Standard ML provides a form of generic equality which is inferred for certain types, called equality types, on which it is possible to define a computable equality relation. However~ the standard definition is incomplete in the sense that there are interesting and useful types which are not inferred to be equality types but which nevertheless have a computable equality relation. In this paper, a refinement of the Standard ML system of equality types is introduced and is proven sound and complete with respect to the existence of a computable equality. The technique used here is based on an abstract interpretation of ML operators as monotone functions over a three point lattice. It is shown how the equality relation can be defined (as an ML program) from the definition of a type with our equality property. Finally, a sound, efficient algorithm for inferring the equality property which corrects the limitations of the standard definition in all cases of practical interest is demonstrated.

Original languageEnglish (US)
Title of host publicationTheoretical Aspects of Computer Software - International Conference TACS 1991, Proceedings
EditorsAlbert R. Meyer, Takayasu Ito
Number of pages19
ISBN (Print)9783540544159
StatePublished - 1991
Externally publishedYes
Event1st International Conference on Theoretical Aspects of Computer Software, TACS 1991 - Sendai, Japan
Duration: Sep 24 1991Sep 27 1991

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume526 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Other1st International Conference on Theoretical Aspects of Computer Software, TACS 1991

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)


Dive into the research topics of 'An abstract interpretation for ML equality kinds'. Together they form a unique fingerprint.

Cite this