### Abstract

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 language | English (US) |
---|---|

Title of host publication | Theoretical Aspects of Computer Software - International Conference TACS 1991, Proceedings |

Editors | Albert R. Meyer, Takayasu Ito |

Publisher | Springer-Verlag |

Pages | 112-130 |

Number of pages | 19 |

ISBN (Print) | 9783540544159 |

DOIs | |

State | Published - Jan 1 1991 |

Event | 1st International Conference on Theoretical Aspects of Computer Software, TACS 1991 - Sendai, Japan Duration: Sep 24 1991 → Sep 27 1991 |

### Publication series

Name | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |
---|---|

Volume | 526 LNCS |

ISSN (Print) | 0302-9743 |

ISSN (Electronic) | 1611-3349 |

### Other

Other | 1st International Conference on Theoretical Aspects of Computer Software, TACS 1991 |
---|---|

Country | Japan |

City | Sendai |

Period | 9/24/91 → 9/27/91 |

### Fingerprint

### ASJC Scopus subject areas

- Theoretical Computer Science
- Computer Science(all)

### Cite this

*Theoretical Aspects of Computer Software - International Conference TACS 1991, Proceedings*(pp. 112-130). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 526 LNCS). Springer-Verlag. https://doi.org/10.1007/3-540-54415-1_43

**An abstract interpretation for ML equality kinds.** / Gunter, Carl A.; Gunter, Elsa L.; MacQueen, David B.

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

*Theoretical Aspects of Computer Software - International Conference TACS 1991, Proceedings.*Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 526 LNCS, Springer-Verlag, pp. 112-130, 1st International Conference on Theoretical Aspects of Computer Software, TACS 1991, Sendai, Japan, 9/24/91. https://doi.org/10.1007/3-540-54415-1_43

}

TY - GEN

T1 - An abstract interpretation for ML equality kinds

AU - Gunter, Carl A.

AU - Gunter, Elsa L.

AU - MacQueen, David B.

PY - 1991/1/1

Y1 - 1991/1/1

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=85030244930&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85030244930&partnerID=8YFLogxK

U2 - 10.1007/3-540-54415-1_43

DO - 10.1007/3-540-54415-1_43

M3 - Conference contribution

AN - SCOPUS:85030244930

SN - 9783540544159

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 112

EP - 130

BT - Theoretical Aspects of Computer Software - International Conference TACS 1991, Proceedings

A2 - Meyer, Albert R.

A2 - Ito, Takayasu

PB - Springer-Verlag

ER -