Programming languages with canonical functions Are there any (functional?) programming languages where all functions have a canonical form? That is, any two functions that return the same values for all set of input is represented in the same way, e.g. if f(x) returned x + 1, and g(x) returned x + 2, then f(f(x)) and g(x) would generate indistinguishable executables when the program is compiled.

Perhaps more importantly, where/how might I find more information on canonical representation of programs (Googling "canonical representation programs" has been less than fruitful)? It seems like a natural question to ask, and I'm afraid that I just don't know the proper term for what I am looking for. I'm curious as to whether it is possible for such a language to be Turing complete, and if not, how expressive a programming language you can have, while still retaining such a property.

My background is rather limited, so I would prefer sources with fewer prerequisites, but references to more advanced sources may be cool too, as that way I'll know what I want to work towards.
The extent to which this is possible is actually a major open question in the theory of the lambda calculus. Here's a quick summary of what's known:


The simply-typed lambda calculus with unit, products, and function space does have a simple canonical forms property. Two terms are equal if and only if they have the same beta-normal, eta-long form. Computing these normal forms is also quite straightforward.
The addition of sum types greatly complicates matters. The equality problem is still decidable (the keyword to search for is "coproduct equality"), but the known algorithms work for extremely tricky reasons and to my knowledge there is no totally satisfying normal form theorem. Here are the four approaches I know of:


Neil Ghani, Beta-Eta Equality for Coproducts, TLCA 1995.
Vincent Balat, Roberto di Cosimo, Marcelo Fiore, Extensional normalisation and type-directed partial evaluation for typed lambda calculus with sums, POPL 2004.
Sam Lindley, Extensional Rewriting with Sums, TLCA 2007.
Arbob Ahmad, Daniel R. Licata, and Robert Harper, A Proof-Theoretic Decision Procedure for the Finitary Lambda-Calculus. WMM 2007.

The addition of unbounded types, such as natural numbers, makes the problem undecidable. Basically, you can now encode Hilbert's tenth problem.
The addition of recursion makes the problem undecidable, because having normal forms makes equality decidable, and that would let you solve the halting problem.