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|
|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|
Items in eCommons are protected by copyright, with all rights reserved, unless otherwise indicated.