I was told that the runtime of OCAML or Scala is EXPTIME - which seems really bad! However, since people use type inference (deciding the type of a term or program or expression) in practice - it must be fine in programs humans write somehow.

I was looking for an official reference for such a facts - especially in the simplest setting: Simply Typed Lambda Calculus. In addition if it's simple enough the analysis would be awesome to see it here (since it's 2021 I'd assume have a good simple understanding of this/good ways to teach it...I hope!).

Note, the type of answer I expect is something like this:

  1. Given a simply typed lambda term $e$ with number of nodes $O(n)$ or max height of tree $O(n)$ (or whatever the input length is)
  2. Then the run-time (time complexity) of type inference in simply typed lambda calculus is $O(f(n))$ for some explicitly given function $f$.

As far as I understand, this is the algorithm:

enter image description here

$$ \begin{algorithm} \caption{Type inference for Simply Typed Lambda Calculus} \begin{algorithmic}[1] \State{\textbf{Definition }infer\_type($e$, $\Gamma$)}: \State{\textbf{Input:} $e$ input term we want to infer the type. Context $\Gamma$ with term-type pairs $x:\tau$.} % \State {\textbf{match:} $e$ \textbf{with:}} \If{ term $e$ is a $Variable$} \State{ $\tau_e = \Gamma.get\_type(e)$ } \State{ \textbf{Return:} $\tau_e$ } \ElsIf{term $e = \lambda x: \tau. body$ is an $Abstraction$} \State{ $\Gamma' = \Gamma \cup \{ x: \tau \}$ } \State{ $\tau_{abs} = infer\_type(body, \Gamma' ) $ } \State{ \textbf{Return:} $\tau_{abs}$ } \Else{ term $e = (e_{left}) e_{right}$ is an $Application$ \textbf{then}} \State{ $\tau_{left} = infer\_type(e_{left}, \Gamma) $ } \State{ $\tau_{right} = infer\_type(e_{right}, \Gamma) $ } \State{ $\tau_{apply} = \tau_{left} \to \tau_{right}$ } \State{ \textbf{Return:} $\tau_{apply}$ } \EndIf \end{algorithmic} \end{algorithm} $$

(note couldn't get the latex to compile)

Which looks like you just traverse node in the tree once and then start constructing the desired type by using the correct constructors $Var, Apply, Abs$. So I'd guess in the format I am requesting the time complexity is:

  1. Input size is $n$ - the number of nodes in the tree term $e$
  2. $T(n) = O(n)$ linear, since we look at each node once.

I am assuming that getting the type for base variables takes $O(1)$ with hash tables/dictionaries. Adding one element to the typing environment/context is O(1) and it takes just as long to look for any size dictionary/hash table (so looking for more types in the context is fine).

Without hash tables it would take $O(n(V+n))$ in a very pessimistic analysis. For each look up at the leafs which we have $(n+1)/2$ we could do a linear search for the term we want so $O(V+n)$ where the +n comes from the worst case that we have always at most the number of elements in the context plus all the nodes we could have added when creating abstractions.

Related questions:

since I am also interested in a general set of references and reasons for type inferences in those systems.

  • $\begingroup$ found the same question cstheory.stackexchange.com/questions/47639/… but I do not understand the answer's terminology (PTIME complete) and they don't provide an answer in the format I request e.g. $T(n) = O(f(n))$ $\endgroup$ Commented Dec 20, 2021 at 18:00
  • $\begingroup$ related: cs.stackexchange.com/questions/6617/… $\endgroup$ Commented Dec 20, 2021 at 18:57
  • $\begingroup$ This question seems about Hindley-Milner type inference, which does not affect Scala but OCaml. Simply-typed lambda calculus has a slightly simpler inference problem, so it’s not quite comparable. $\endgroup$ Commented Dec 20, 2021 at 19:09
  • 2
    $\begingroup$ The algorithm is wrong. The lambda case should return a function type, the application case should check that the left type is a function type. $\endgroup$ Commented Dec 20, 2021 at 19:11
  • 2
    $\begingroup$ In addition to @AndrásKovács’s comment, your algorithm does “type inference” for programs with type annotations, which is usually called type checking and has very different complexity. $\endgroup$ Commented Dec 20, 2021 at 19:12


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.