Take the 2-minute tour ×
Theoretical Computer Science Stack Exchange is a question and answer site for theoretical computer scientists and researchers in related fields. It's 100% free, no registration required.

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#?

share|improve this question

1 Answer 1

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
    
share|improve this answer
    
@MartinBerger Oh, yes, of course. What's the name of F + recursive types? –  Gilles Mar 30 at 19:27

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.