$HA^{\omega}$ is a conservative extension of $HA$. But why? This is definitely a silly question, but I've no one to ask... $HA^{\omega}$ is an extension of $HA$ in all finite types. One can formalize a model of $HA^{\omega}$ in $HA$ using indicies of partial recursive functions to represent types, and in such a way that the base type of $HA^{\omega}$ gets interpreted as the natural numbers of $HA$, thus yielding the result that $HA^{\omega}$ is a conservative extension of $HA$. But how do we know this? Is it because $HA$ is also interpretable in $HA^{\omega}$ and this is an instance of a quite general result, or is something deeper at play, perhaps using particularities of number theory? I ask in part because I'm interested in general strategies for showing a theory to be a conservative extension of another

I think this is the general fact you are asking about:

> Suppose that $T$ and $T'$ are theories, the language of $T'$ extends the language of $T$, and every model $T$ extends to a model of $T'$ that satisfies the same sentences of the language of $T$. Then $T'$ is conservative over $T$ for sentences in the language of $T$.

Proof: Suppose that $\phi$ is a sentence in the language of $T$ that is not provable in $T$. Choose a model of $T$ in which $\phi$ is false. By assumption, this model extends to a model of $T'$ in which $\phi$ is false. Thus $T'$ does not prove $\phi$. By contraposition: if $\psi$ is a sentence of the language of $T$ that is provable in $T'$ then $\psi$ is provable in $T$. QED

This can be generalized to situations where $T'$ merely interprets the language of $T$, rather than extending it. But in the case of $HA$, the language of $HA^\omega$ does extend the language of $HA$.