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 '16 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 '16 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 '16 at 13:46

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.

| cite | improve this answer | |

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.