Haskell is said to be a pure language because the language features are directly translatable into lambda calculus.

My question is: for languages considered to be non-pure functional languages (e.g. Scala, OCaml), which aspects of those languages are not translatable into lambda calculus?

  • 1
    $\begingroup$ Lambda calculus is Turing complete, but not Tetris complete $\endgroup$
    – adrianN
    Oct 25, 2016 at 7:55
  • 1
    $\begingroup$ Haskell, Scala and Lambda calculus are all Turing-complete, so we know that there are computable cross-compilers. What do you mean by "directly translatable"? $\endgroup$
    – Raphael
    Oct 25, 2016 at 8:14
  • $\begingroup$ @Raphael Turing-complete is a rather weak characterization of languages. For example, the lambda calculus is Turing complete, but we certainly can't do IO in it, like we can with Scala. $\endgroup$
    – gardenhead
    Oct 25, 2016 at 13:46

1 Answer 1


That's not what "pure" means. Pure means, generally, that there is no mutable state, and no way to interact with the outside world (i.e. IO).

Haskell is not "directly translatable" (what translation between language features really means needs to be defined fist, but let's ignore that for now) into either the untyped or simply-typed lambda calculus. There are many features that prevent it from being so, but a good example is polymorphism: there is no polymorphic identity function in the simply-typed lambda calculus.

Instead, Haskell and SML are actually derived from the Hindley-Milner type system, which is an extension of the simply-typed lambda calculus with polymorphism and type-constructors (aka higher-kinded types). Hindley-Milner has the nice property that type inference is decidable without any type annotations.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.