×

zbMATH — the first resource for mathematics

Haskell overloading is DEXPTIME-complete. (English) Zbl 0835.68008
Summary: Since coreML can be viewed as a subset of Haskell, the lower bound proven in A. J. Kfoury, J. Tiuryn and P. Urzyczyn, An analysis of ML typability, Lect. Notes Comput. Sci. 431, 206-220 (1990) and H. G. Mairson, Deciding ML typability is complete for deterministic exponential time, Proc. AMC Internat. Conf. on Principles of Programming Languages, 382-401 (1990)] also applies to Haskell in stating that deciding whether or not some Haskell program is type-correct is at least DEXPTIME-hard. Analyzing the type inference algorithm of Nipkow and Prehofer one observes that DEXPTIME is also enough to derive most general typings. The exponent in die estimation of the runtime thereby depends on the depth of nesting of let-constructs.
Our results complete the complexity analysis of the Haskell type system. We considered the question of deciding for a given type judgement whether or not the assumptions contained in the sort environment can be met or not. We found that this problem in DEXPTIME-complete as well – now however, the exponent in the runtime estimation depends on the maximal number of classes of type may be member of.

MSC:
68N01 General topics in the theory of software
68Q25 Analysis of algorithms and problem complexity
Software:
Haskell
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Frühwirth, T.; Shapiro, E.; Vardi, M.; Yardeni, E., Logic programs as types of logic programs, Proc. 6th symp. on logics in computer science, 300-309, (1991)
[2] Hudak, P.; Jones, S.P.; Wadler, P., Report on the programming language Haskell, A non-strict, purely functional language, ACM SIGPLAN notices, 27, 5, (1992), Version 1.2
[3] Kfoury, A.J.; Tiuryn, J.; Urzyczyn, P., An analysis of ML typability, (), 206-220 · Zbl 0760.68035
[4] Mairson, H.G., Deciding ML typability is complete for deterministic exponential time, Proc. ACM internat. conf. on principles of programming languages, 382-401, (1990)
[5] Nipkow, T.; Prehofer, C., Type checking type classes, Proc. ACM internat. conf. on principles of programming languages, 409-418, (1993)
[6] Seidl, H., Deciding equivalence of finite tree automata, Proc. STACS’89, Lecture notes on computer science, 349, 480-492, (1989)
[7] Volpano, D.M.; Smith, G.S., On the complexity of ML typability with overloading, Proc. 5th symp. on functional programming languages and computer architecture, Lecture notes on computer science, 523, 15-28, (1991)
[8] Volpano, D.M., Haskell-style overloading in NP-hard, ()
[9] Wadler, P.; Blott, S., How to make ad-hoc polymorphism less ad-hoc, Proc. ACM internat. conf. on principles of programming languages, 60-76, (1989)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.