HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation
Reports

Extension of ML type system with a sorted equation theory on types

Didier Rémy 1
1 FORMEL
INRIA Rocquencourt
Abstract : We extend the ML language by alowing a sorted regular equational theory on types for which unification is decidable and unitary. We prove that the extension keeps principal typings and subject reduction. A new set of typing rules is proposed so that type generalization is simpler and more efficient. We consider typing problems as general unification problems, which we solve with a formalism of unificands. Unificands naturally deal with sharing between types and lead to a more efficient type inference algorithm by splitting it into more elementary steps.
Document type :
Reports
Complete list of metadata

https://hal.inria.fr/inria-00077006
Contributor : Rapport de Recherche Inria Connect in order to contact the contributor
Submitted on : Monday, May 29, 2006 - 11:49:34 AM
Last modification on : Friday, February 4, 2022 - 3:16:14 AM
Long-term archiving on: : Monday, April 5, 2010 - 9:29:24 PM

Identifiers

  • HAL Id : inria-00077006, version 1

Collections

Citation

Didier Rémy. Extension of ML type system with a sorted equation theory on types. [Research Report] RR-1766, INRIA. 1992. ⟨inria-00077006⟩

Share

Metrics

Record views

59

Files downloads

243