1

What programming languages are functional and pure?

sepp2k
  • 363,768
  • 54
  • 674
  • 675
Delirium tremens
  • 4,623
  • 9
  • 46
  • 59
  • 1
    The answers to this question might be helpful: http://stackoverflow.com/questions/4382223/pure-functional-language-haskell – Greg Hewgill Jan 15 '11 at 20:31
  • 1
    Also the [functional languages section of the list of programming languages by category on Wikipedia](http://en.wikipedia.org/wiki/List_of_programming_languages_by_category#Functional_languages). – ephemient Jan 16 '11 at 04:14

3 Answers3

4

There are probably tons of them but the main one most people know about and use is Haskell.

Some others are Miranda and Clean

Matthew Manela
  • 16,572
  • 3
  • 64
  • 66
  • Just as a note, Miranda is essentially defunct at this point and superceded by Haskell. Clean is under active development still. – sclv Feb 10 '11 at 17:49
  • Miranda is still used in the SPJ paper on implementations of functional languages :). I feel like rewriting the entire paper to use a subset of haskell as the target language because I dislike Miranda's use of capitalization so much (or maybe thats just them) – alternative Aug 08 '11 at 01:07
2

A nice functional programming language is Agda: http://www.cse.chalmers.se/~ulfn/papers/afp08/tutorial.pdf

Due to dependent type some functions can be defined that could not be defined in other languages like haskell. E.g. the type of functions (Vec n -> Vec n), that return a vector of the same length as their argument is, for instance sort is of this type. [WAS "I believe some paper considered it purer than haskell." before edit.]

The advantage of agda is that the souce code is very nice, and similar to haskell. Further, any haskell function can be called and used. Drawback is mainly that the standard library changes too often at the moment.

Just look at the source code for lists: http://www.cse.chalmers.se/~nad/listings/lib-0.4/Data.List.html#209

Of course there are similar functional programming languages like coq, epigram, etc.

And reference to Curry-Howard in wikipedia:
http://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence

Some links regarding dependent types (and includes some agda links): http://www.reddit.com/r/dependent_types/

mrsteve
  • 4,082
  • 1
  • 26
  • 63
  • Agda is a dependently typed progamming language/theorem prover. It is largely for research at the moment, and is no purer than Haskell in any meaningful sense. Epigram is similar to agda except there is no good working implementation at all at the moment -- the development of Epigram 2 is an ongoing research broject. Coq isn't a language at all (although it can extract to some) but simply a theorem prover. – sclv Feb 10 '11 at 17:48
  • Hello Sclv. Changed one part of the post. Regarding Coq, according to Wiki pedia: "Coq implements a dependently typed functional programming language.[1]". Either Wikipedia is wrong or there is a misunderstanding on my part. Yes, Agda is largely for research but that can be said for haskell as well. I think there will be a keen interest if the development of agda continues. And it should be listed as one of the pure functional programming languages. – mrsteve Feb 14 '11 at 05:24
1

The Lambda calculus and SK-calculus are also two very important programming languages that are purely functional.

cdiggins
  • 17,602
  • 7
  • 105
  • 102