Cornell University
Library
Cornell UniversityLibrary

eCommons

Help
Log In(current)
  1. Home
  2. Cornell Computing and Information Science
  3. Computer Science
  4. Computer Science Technical Reports
  5. On the Complexity of ML Typability with Overloading

On the Complexity of ML Typability with Overloading

File(s)
91-1210.pdf (935.72 KB)
91-1210.ps (268 KB)
Permanent Link(s)
https://hdl.handle.net/1813/7050
Collections
Computer Science Technical Reports
Author
Volpano, Dennis M.
Smith, Geoffrey S.
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].

Date Issued
1991-05
Publisher
Cornell University
Keywords
computer science
•
technical report
Previously Published as
http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cs/TR91-1210
Type
technical report

Site Statistics | Help

About eCommons | Policies | Terms of use | Contact Us

copyright © 2002-2026 Cornell University Library | Privacy | Web Accessibility Assistance