It's true that Turing complete languages are (almost by definition) equivalent for writing programs of type "Nat -> Nat". However, things are not so simple at o

It's true that Turing complete languages are (almost by definition) equivalent for writing programs of type "Nat -> Nat". However, things are not so simple at other types and it turns out there is actually something of a spectrum of computability. Andrej Bauer has a nice post on such things here: http://math.andrej.com/2011/07/27/definability-and-extensionality-of-the-modulus-of-continuity-functional/ http://math.andrej.com/2011/07/27/definability-and-extension...