Sun Mar 7 21:19:03 CET 2010

Simply Typed LC is Strongly Normalizing

From [1]:

  Given the standard semantics, the simply typed lambda calculus is
  strongly normalizing: that is, well-typed terms always reduce to a
  value, i.e., a lambda abstraction. This is because recursion is not
  allowed by the typing rules.  Recursion can be added to the language
  by either having a special operator of type (a->a)->a or adding
  general recursive types, though both eliminate strong normalization.
  Since it is strongly normalizing, it is decidable whether or not a
  simply typed lambda calculus program halts: it does! We can
  therefore conclude that the language is not Turing complete.

In Haskell and OCaml the type inferencer doesn't like construction
of infinite types:

:t (\x -> x x) (\x -> x x)

To express the Y combinator in this direct form requires it to be
wrapped in a recursive type[3] (quotes from [2]):

  The problem with fix f = (\x -> f (x x))(\x -> f (x x)) is that one
  needs a solution to the type equation b = b -> a. Fortunately this
  can be done with Haskell’s data types.

> newtype Mu a = Roll { unroll :: Mu a -> a }
> fix f = (\x -> f ((unroll x) x)) (Roll (\x -> f ((unroll x) x)))

  Of course, this is just an academic exercise. To actually define a
  fixpoint combinator in Haskell, one would use recursive definitions.

I.e. the Y combinator can be defined directly in its recursive form:

> y f = f (y f)

[1] http://en.wikipedia.org/wiki/Simply_typed_lambda_calculus
[2] http://r6.ca/blog/20060919T084800Z.html
[3] http://en.wikipedia.org/wiki/Recursive_type
[4] http://en.wikipedia.org/wiki/System_F