Skip to main content


eCommons@Cornell >
College of Engineering >
Computer Science >
Computer Science Technical Reports >

Please use this identifier to cite or link to this item:
Title: On the Complexity of ML Typability with Overloading
Authors: Volpano, Dennis M.
Smith, Geoffrey S.
Keywords: computer science
technical report
Issue Date: May-1991
Publisher: Cornell University
Abstract: We examine the complexity of type checking in an ML-style type system that permits functions to be overloaded with different types. In particular, we consider the extension of the ML Type system proposed by Wadler and Blott in the appendix of [WB89], with global overloading only, that is, where the only overloading is that which exists in an initial type assumption set; no local overloading via over and inst expressions is allowed. It is shown that under a correct notion of well-typed terms, the problem of determining whether a term is well typed with respect to an assumption set in this system is undecidable. We then investigate limiting recursion in assumption sets, the source of the undecidability. Barring mutual recursion is considered, but this proves too weak, for the problem remains undecidable. Then we consider a limited form of recursion called parametric recursion. We show that although the problem becomes decidable under parametric recursion, it appears harder than conventional ML typability, which is complete for DEXPTIME [Mai90].
Appears in Collections:Computer Science Technical Reports

Files in This Item:

File Description SizeFormat
91-1210.pdf935.72 kBAdobe PDFView/Open
91-1210.ps268 kBPostscriptView/Open

Refworks Export

Items in eCommons are protected by copyright, with all rights reserved, unless otherwise indicated.


© 2014 Cornell University Library Contact Us