> Insofar as a program can be compiled and implemented in machine code, all the functions of that program's programming language can be mapped 1 to 1 to nat ->

> Insofar as a program can be compiled and implemented in machine code, all the functions of that program's programming language can be mapped 1 to 1 to nat -> nat operations. That mapping is a property of the implementation, not of the language. A user of the source language can't rely on the existence of this mapping - it would be literally impossible to run programs, say, using paper and pencil. > If a language has parametric polymorphism, is it therefore not Turing complete? Whut? > Because if the language with parametric polymorphism is Turing complete, then the Church-Turing thesis absolutely has something to say about that language. It says something about the functions of type `nat -> nat` that I can compute in the language. But a language with parametric polymorphism has lots of other types besides `nat -> nat`.