This question is about what I presume is a basic construction in type theory.
The finite types are defined as follows: 0 is a finite type; if $\sigma, \tau$ are finite types, then so is $\sigma\rightarrow \tau$; and the set of finite types is the smallest set satisfying those two properties. The interpretation of these types which I am currently using is: objects of type 0 are natural numbers, and objects of type $\sigma\rightarrow\tau$ are funtions from the set of objects of type $\sigma$ to the set of objects of type $\tau$.
Now, amongst the finite types are the so-called standard types: $0$, $0\rightarrow 0$, $(0\rightarrow 0)\rightarrow 0$, etc. These are identified with natural numbers: $0\rightarrow 0$ is abbreviated by 1, and $n\rightarrow 0$ is abbreviated by $n+1$. Given a finite type $\sigma$, we can associate to $\sigma$ a standard type, the height of $\sigma$, given by $$ht(0)=0, ht(\sigma\rightarrow \tau)=\max\{ht(\sigma)+1, ht(\tau)\}.$$
Now intuitively, it is clear that, "morally speaking," all objects can be represented by objects of standard type. For example, given an object $F$ of type $0\rightarrow 1$, we can represent $F$ by the type-1 functional $$ G: \langle x, y\rangle\mapsto Fxy,$$ where $\langle\cdot,\cdot\rangle$ is your favorite pairing function on $\mathbb{N}$. Now, inductively we can carry this out through all the finite types, in a somewhat-messy-to-write-out but still fairly natural way: to each object $F$ of type $\sigma$ we associate an object $st(F)$ of type $ht(\sigma)$ in such a way that $F$ can be "recovered" from $st(F)$ and $\sigma$. (Morally, that recovered ought to mean something like "recovered computably.")
My question is the following: I've seen this alluded to in a number of sources, but I've never seen it worked out in detail. I've written out a procedure for encoding arbitrary objects of finite type by standard-type objects, but it's long and messy, I'm sure it can be made shorter, and I'm not totally certain it's correct; moreover, I'd like to see how it's been done in the past. So my question is:
Can someone recommend for me a source where this encoding is written out explicitly?