Yes it has. Mercury is a perfect example of a purely functional language which is not lazy. I/O is made functional via a uniqueness typing system.

Right, so it uses uniqueness typing and not monads presumably.

There is Idris: http://idris-lang.org/

It seems similar to what plinkplonk is talking about.

Hmm, I always thought of Idris, Coq and Agda as proof assistants rather than programming languages, but perhaps that's just me being unimaginative.

Idris is explicitly billed as a programming language. You can do pretty sophisticated programming in Coq too (Coq can be reasonably straightforwardly compiled down to Ocaml, Haskell and some other languages.)

I'd better spend some time checking it out then!

what about disciple and mu ?

http://stackoverflow.com/questions/10784124/non-lazy-branch-...

http://anil.recoil.org/papers/2011-cufp-scribe-preprint.pdf

I'm not really sure how "pure" Disciple can be considered to be, and it doesn't use monads does it? Perhaps I'm being ignorant though.

Mu is a great example. I wish there was more information about it publically available.