Programming languages with canonical functions
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.