The functions definable in typed lambda calculus are the computable functions, for which idt is in turn possible to efine equivalences to the concepts of Turing machines, recursive enumerability and Type-0 grammars.

But what about typed lambda calculus — where on the Chomskian computability hierarchy are the functions definable by expressions of simply-typed lambda calculus?

Assuming that there is a natural way of transferring the idea of lambda-definability of a recursive function from untyped to simply-typed lambda calculus, along the lines of:

A $ k$ -ary number-theoretic function $ f$ is simply-typed-lambda definable iff there is a simply typable $ \lambda$ -term $ P$ such that for all $ x_1, \ldots x_k$ , where $ \underline{x}$ is the encoding of $ x$ , $ P \underline{\vec{x}} =_\beta \underline{y} \text{ iff } f(\vec{x}) = y$ , if $ f(\vec{x})$ is defined, and $ P$ has no $ \beta$ -normal form othewise.

To make the bridge from functions to formal languages and the Chomsky hierarchy, I guess my question is:

Between which levels of the Chomsky hierarchy is the class of languages located such that $ L$ is in the class iff there is a simply-typed-lambda-definable function $ f$ such that $ f(w)$ is defined if and only if $ w \in L$ ?

Alternatively, are there other ways of building an correspondence between typed lambda calculus and formal languages or automata that makes it possible to locate it on the known computability scale in a meaningful way?

All I could find so far was about modifications of lambda calculus corresponding to certain types of grammars, or auotmata to recognize strings certain kinds of lambda expressions, but, surpisingly, nothing specifically about (Curry-style) typed lambda calculus.