Deciding ML Typability is Complete for Deterministic Exponential Time

Abstract

A well known but incorrect piece of functional programming folklore is that ML expressions can be efficiently typed in polynomial time. In probing the truth of that folklore, various researchers, including Wand, Buneman, Kanellakis, and Mitchell, constructed simple counterexamples consisting of typable ML programs having length n, with principal types having Ω(2cn) distinct type variables and length Ω(22cn). When the types associated with these ML constructions were represented as directed acyclic graphs, their sizes grew as Ω(2cn). The folklore was even more strongly contradicted by the recent result of Kanellakis and Mitchell that simply deciding whether or not an ML expression is typable is PSPACE-hard.