Yes, sure. Many typed lambda calculi accept only
strongly normalizing terms, by design, so they cannot express arbitrary computations. But a type system can be anything you like; make it broad enough, and you can express all deterministic computations. A trivial type system that encompasses a Turing-complete fragment of the lambda calculus is the one that accepts every term as well-typed (with a
top type). $$dfrac{}{Gamma vdash M : top}$$ More practically, statically typed functional programming languages have at their core a typed lambda calculus which allows a
fixpoint combinator as well-typed. For example, start with the
simply typed lambda calculus (or the ML type system or
system F or any other type system of your choice) and add a rule that makes some fixpoint combinator like $mathbf{Y} = lambda f. (lambda x. f (x,x)) (lambda x. f (x,x))$ well-typed. $$ dfrac{Gamma vdash f : T rightarrow T} {Gamma vdash mathbf{Y},f : T} qquad dfrac{Gamma vdash f : T rightarrow T} {Gamma vdash (lambda x. f (x,x)) (lambda x. f (x,x)) : T} $$ The rules as presented above are rather clumsy, as they make terms like $mathbf{Y},f$ well-typed even though their constituents are not well-typed — they are not fully compositional. A simple fix is to add a fixpoint combinator as a language constant and provide a delta rule for it; then it is a simple matter to have a type system and reduction semantics with
type preservation. You do get away from the pure lambda calculus into the realm of lambda calculus with constants. $$begin{gather*} dfrac{}{Gamma vdash textbf{fix} : (T rightarrow T) rightarrow T} textbf{fix},f to f (textbf{fix},f) end{gather*}$$ Sticking to the pure lambda calculus, an interesting type system is the lambda calculus with intersection types. $$ dfrac{Gamma vdash M : T_1 quad Gamma vdash M : T_2} {Gamma vdash M : T_1 wedge T_2} (wedge I) qquadqquad dfrac{} {Gamma vdash M : top} (top I) $$ Intersection types have interesting properties with respect to normalization:
- A lambda-term can be typed without using the $top I$ rule iff it is strongly normalizing.
- A lambda-term admits a type not containing $top$ iff it has a normal form.
See Characterization of lambda-terms that have union types for an insight as to why intersection types have such a remarkable scope. So you have a type system that defines a Turing-complete language (since every term is well-typed), and a simple characterization of terminating computations. Of course, since this type system characterizes normalization, it is not decidable. A remark on the rule names $(top I)$ and $(wedge I)$: they have no formal meaning, but they are chosen deliberately. the $I$ stands for “introduction”, because these are introduction rules — they introduce the symbol ($wedge$ or $top$) into the type below the line. Dually, you’ll find elimination rules, when a symbol appears above the line but not below. For example, the rule to typecheck a lambda expression in the simply-typed lambda calculus is the introduction rule for $rightarrow$, and the rule to typecheck an application is the elimination rule for $rightarrow$.
