Haskell-style Overloading is NP Hard
Abstract
Extensions of the ML type system, based on constrained type schemes, have been proposed for languages with overloading. Type inference in these systems requires solving the following satisfiability problems. Given a set of type assumptions C over finite types, and a type basis A, is there is a substitution S that satisfies C in that A 1- CS is derivable? Under arbitrary overloading, the problem is undecidable. Haskell limits overloading to a form similar to that proposed by Keas called parametric overloading. We formally characterize parametric overloading in terms of a regular tree language and prove that although decidable, satisfiability is NP-hard when overloading is parametric.
Description
The article of record as published may be found at http://dx.doi.org/
Rights
This publication is a work of the U.S. Government as defined in Title 17, United States Code, Section 101. Copyright protection is not available for this work in the United States.Collections
Related items
Showing items related by title, author, creator and subject.
-
TEMPORAL CONNECTIVITY AS A MEASURE OF ROBUSTNESS IN NONORTHOGONAL MULTIPLE ACCESS WIRELESS NETWORKS
Pimentel, Benjamin A. (Monterey, CA; Naval Postgraduate School, 2022-06);Nonorthogonal multiple access (NOMA) is recognized as an important technology to meet the performance requirements of fifth generation (5G) and beyond 5G (B5G) wireless networks. Through the technique of overloading, NOMA ... -
Lower Bounds on Type Checking Overloading
Volpano, Dennis (1996-01);Smith has proposed an elegant extension of the ML type system for polymorphic functional languages with overloading. Type inference in his system requires solving a satisfiability problem that is undecidable if no restrictions ... -
Type inference with overloading using an attribute grammar
Bull, Bruce James (Monterey, California. Naval Postgraduate School, 1994-03);Interactive programming environment for language offer many advantages over traditional batch-oriented ones, such as immediate static analysis. One form of analysis is type checking, yet type checking in this setting for ...