Complexity of ML typing

To: types@theory.lcs.mit.edu
Subject: Complexity of ML typing
From: jcm@ra.stanford.edu (John Mitchell)
Date: Mon, 16 May 88 14:19:00 PDT



        Polymorphic Unification and ML Typing

                Paris Kanellakis
                 John Mitchell

There is a varied folklore regarding the complexity of ML typing,
but no previously published results, to the best of our knowledge.
We have studied the following problem.

    GIVEN: a term of the pure lambda calculus with LET
    FIND: whether there exists an ML typing for this term

The pure lambda calculus with LET is a fragment of the Core ML
expression language studied in Milner's 1978 paper. The typing 
problem for this language differs from pure Curry typing
(and Hindley's earlier algorithm) because of the polymorphic
LET declaration. Note that we do not try to find the type 
of a given term, since the size of the type may adversely effect
the running time of the algorithm.

For the above problem we have obtained
   (i)  a straightforward DEXP-time upper bound, and
   (ii) a nontrivial Co-NP-hard lower bound.  

The lower bound may be stated using a form of unification
on expressions (e.g., "type expressions") with "polymorphic" 
declarations. The proof uses techniques from our earlier work 
on the complexity of ordinary unification (with Cynthia Dwork, 
J. Logic Programming, 1).

It was previously known that for certain terms, the ML typing
algorithm takes exponential time, since the type of a term with
a deep nesting of LET's may have exponential size. In fact, as 
pointed out to us by Mitch Wand and (independently) Peter Buneman,
there exist ML expressions whose principal types contain 
exponentially-many distinct type variables.  So even the DAG 
representation of a type (with common subexpressions shared) 
may have exponential size. Using our "polymorphic" type expression 
representation (which is more succinct than DAGs) and "polymorphic"
unification, we can actually handle these examples (and represent 
the principle type) in polynomial-time. The exponential-time
behavior of the ML algorithm seems to be known to a number of 
researchers, although we have not been able to find any published commentary. 

We are in the process of writing this up for publication, but thought
the TYPES readership would want to be the first to know. Any comments
or suggestions of related references would be appreciated.