<p>If you want to include a fixpoint combinator in the language, you don't need to change anything to the syntax of types or the rules to type existing expressions. All it takes is adding one constant, a rule to type it and a rule to reduce expressions containing it:
$$
  \dfrac{}{\mathsf{fix} : (\tau \rightarrow \tau) \rightarrow \tau} \qquad
  \mathsf{fix} \, f \to f (\mathsf{fix} f)
$$</p>

<p>If you want to be able to define a fixpoint combinator in terms of the core lambda-calculus syntax, that's a different matter. There are a lot of type systems, some of them allowing arbitrary recursion, some of them not. There isn't a simple way of telling by looking at a type system whether it allows arbitrary recursion. For example, some very sophisticated type systems (e.g. the <a href="https://en.wikipedia.org/wiki/Calculus_of_constructions" rel="nofollow noreferrer">calculus of inductive constructions</a> which <a href="https://en.wikipedia.org/wiki/Coq" rel="nofollow noreferrer">Coq</a> is based on) include a $\mathsf{fix}$ combinator with a typing rule that limits the types at which it can be used in such a way that only terminating functions can be defined. Here are a few ways arbitrary recursion can be added to a typed lambda calculus:</p>

<ul>
<li>Intersection types: they allow any lambda-term to be typed, in a way that you can read from the type whether the term is strongly normalizing and whether it has a normal form. See <a href="https://cs.stackexchange.com/questions/2638/does-there-exist-a-turing-complete-typed-lambda-calculus/2639#2639">Does there exist a Turing complete typed lambda calculus?</a></li>
<li>If you add (sufficient) recursion to the type language, this <a href="http://en.wikipedia.org/wiki/Fixed_point_combinator#Type_for_the_Y_combinator" rel="nofollow noreferrer">adds recursion to the term language as well</a>. In ML, this leads to a recursive function definition without using <code>let rec</code>, by relying instead on a type definition of the form <code>type t = Constructor of (t -&gt; …)</code>.</li>
<li>The typing rules for ML-like languages are based on defining a typing rule for <code>let rec</code> that allows the variable to be used in its own definition. This makes <code>let rec</code> not syntactic sugar for a lambda-expression, unlike plain <code>let</code>.</li>
</ul>

<hr>

<p>The need to write <code>let rec</code> in ML is unrelated, or at least only loosely related, to the type theory. Here are a few reasons to annotate recursive definitions differently:</p>

<ul>
<li>ML started out as the metalanguage for a theorem prover, and the designers may have felt that it was best programming practice to explicitly mention the use of unbounded recursion (which has the potential to make the proof building process not terminate).</li>
<li>Having the <code>rec</code> indication can make compiler design and type theory design slightly simpler, because there are cases where <code>let</code> can have a more generalizable type than <code>let rec</code>, and different kinds of terms that can or cannot be defined recursively.</li>
<li><p>There are cases where it's useful in programs to have a non-recursive <code>let</code>, which defines a new variable of the same name as an existing one: when an object undergoes a series of transformation, but they're intuitively different stages of the same object.</p>

<pre><code>let widget = read_widget_source () in
let widget = parse_widget widget in
let widget = compile_widget widget in
execute_widget widget
</code></pre></li>
</ul>

CC BY-SA 3.0
2014-03-30T19:27:10.960Z
@MartinBerger Oh, yes, of course. What's the name of F + recursive types?
Gilles 'SO- stop being evil'
CC BY-SA 3.0
2014-03-30T14:00:24.320Z
2014-03-30T19:37:50.800Z
2017-04-13T12:48:30.830Z
Gilles 'SO- stop being evil'
<p>I'm reading some lecture notes saying that “<code>fix</code> cannot be defined in the simply typed lambda-calculus” and that “<em>no</em> expression that can lead to non-terminating computations can be typed using only simple types.”</p>

<p>I'm sure more of this will be covered later, but it left me curious: What is needed in a type system to support defining <code>fix</code>? I.e., how can I simply type (in Haskell): <code>fix f = let x = f x in x</code> and get the type <code>(a → a) → a</code>? Also, is this related to needing to write <code>let rec</code> in ML/F#?</p>

<type-theory><type-systems><recursion>
Extending simple types to allow `fix`
beta
# Extending simple types to allow `fix`

(Asked by: username_0 on 2014-03-30)

I'm reading some lecture notes saying that “`fix` cannot be defined in the simply typed lambda-calculus” and that “*no* expression that can lead to non-terminating computations can be typed using only simple types.”

I'm sure more of this will be covered later, but it left me curious: What is needed in a type system to support defining `fix`? I.e., how can I simply type (in Haskell): `fix f = let x = f x in x` and get the type `(a → a) → a`? Also, is this related to needing to write `let rec` in ML/F#?

**Tags:** type-theory, type-systems, recursion

---

## 1 answers

### Answer by username_1 on 2014-03-30. Score: 9

If you want to include a fixpoint combinator in the language, you don't need to change anything to the syntax of types or the rules to type existing expressions. All it takes is adding one constant, a rule to type it and a rule to reduce expressions containing it:
$$
  \dfrac{}{\mathsf{fix} : (\tau \rightarrow \tau) \rightarrow \tau} \qquad
  \mathsf{fix} \, f \to f (\mathsf{fix} f)
$$
If you want to be able to define a fixpoint combinator in terms of the core lambda-calculus syntax, that's a different matter. There are a lot of type systems, some of them allowing arbitrary recursion, some of them not. There isn't a simple way of telling by looking at a type system whether it allows arbitrary recursion. For example, some very sophisticated type systems (e.g. the calculus of inductive constructions which Coq is based on) include a $\mathsf{fix}$ combinator with a typing rule that limits the types at which it can be used in such a way that only terminating functions can be defined. Here are a few ways arbitrary recursion can be added to a typed lambda calculus:

Intersection types: they allow any lambda-term to be typed, in a way that you can read from the type whether the term is strongly normalizing and whether it has a normal form. See Does there exist a Turing complete typed lambda calculus?
If you add (sufficient) recursion to the type language, this adds recursion to the term language as well. In ML, this leads to a recursive function definition without using let rec, by relying instead on a type definition of the form type t = Constructor of (t -> …).
The typing rules for ML-like languages are based on defining a typing rule for let rec that allows the variable to be used in its own definition. This makes let rec not syntactic sugar for a lambda-expression, unlike plain let.


The need to write let rec in ML is unrelated, or at least only loosely related, to the type theory. Here are a few reasons to annotate recursive definitions differently:

ML started out as the metalanguage for a theorem prover, and the designers may have felt that it was best programming practice to explicitly mention the use of unbounded recursion (which has the potential to make the proof building process not terminate).
Having the rec indication can make compiler design and type theory design slightly simpler, because there are cases where let can have a more generalizable type than let rec, and different kinds of terms that can or cannot be defined recursively.
There are cases where it's useful in programs to have a non-recursive let, which defines a new variable of the same name as an existing one: when an object undergoes a series of transformation, but they're intuitively different stages of the same object.
let widget = read_widget_source () in
let widget = parse_widget widget in
let widget = compile_widget widget in
execute_widget widget

> **Comments:**
> **username_1**: @MartinBerger Oh, yes, of course. What's the name of F + recursive types?  

---

