In Lambda Calculus, natural numbers, boolean values, list processing functions, recursion, if function are defined in terms of lambda terms. For example, natural numbers are defined as Church numerals, and recursion is defined in terms of a fixed point of a function.

Functional languages are said to be based on Lambda Calculus.

Who shall be concerned about the above concepts in terms of lambda terms: the implementer/designer of the languages, and/or programmers in the languages?

  • Do functional programming languages define/implement the above concepts in terms of lambda terms?

  • As programmers in regular functional programming languages (such as Haskell, Lisp, ML), is it correct that the above concepts are always given in the same way as in imperative languages, and we never have to understand or deal with their definitions in terms of lambda terms?


  1. Those features are almost never implemented like the lambda calculus in modern programming language implementation. In some cases, using the lambda calculus representation for datatypes has performance improvements (this is associated with so-called tagless representations). Historically, the Haskell compiler did use this representation early on, but has since dropped it. In either case, it never affected user code, and was an implementation detail.
  2. Unless there's a compelling reason to, most code does not use said representations, so the programmer will never interface with them. So those concepts are generally the same as in imperative languages, although keep in mind that there are differences since most functional languages are expression-oriented; e.g. 'if ... then ... else ...' is an expression which returns a value, rather than a statement.
  • 2
    $\begingroup$ Just as a side note, one might (one will) run into such definitions when doing stuff with formal proofs and proof assistants such as Coq or Isabelle. $\endgroup$
    – Tassle
    Aug 3 '19 at 2:59
  • $\begingroup$ Do you have an example? I've never used Isabelle, but I can't imagine a case where you'd want to use lambda encodings instead of actual inductive datatypes (and due to predicativity for quantifiers, inductive datatypes are more powerful). $\endgroup$
    – Jason Carr
    Aug 3 '19 at 5:26

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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