Edsko de Vries wrote:

See "What is a purely functional language" by Sabry. Not quite a formal proof about *Haskell*, but then we would first need a formal semantics of Haskell to be able to do that proof ;-)

Thanks for the reference, and also to everyone who replied - all very useful and interesting. For what it's worth, the blog posts I was writing are here: http://www.nobugs.org/blog/archives/2008/11/12/why-do-they-call-it-referenti... http://www.nobugs.org/blog/archives/2008/11/12/why-do-they-call-it-referenti... Andrew