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 problem. 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 assertion CS is derivable? Under arbitrary overloading, the problem is undecidable. Haskell limits overloading to a form similar to that proposed by Kaes 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.
Document Details
- Document Type
- Technical Report
- Publication Date
- May 01, 1994
- Accession Number
- ADA495129
Entities
People
- Dennis M. Volpano
Organizations
- Naval Postgraduate School