functional and pure programming languages

What programming languages are functional and p开发者_开发百科ure?

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

Some others are Miranda and Clean

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/

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