Reference for the undefinability of modulus of continuity functional in PCF?
The proof is hidden somewhere in Troelstra and van Dalen, Constructivism in mathematics, volume 2, I suppose. More likely, it can be found in Troelstra's investigations, if you can lay your hands on it.

It goes like this. Suppose we could define the modulus of continuity in typed $\lambda$-calculus with fixpoint operators. Then we could interpret it in a domain-theoretic realizaiblity model, for example in $\mathsf{PER}(\mathcal{P}\omega)$ where $\mathcal{P}\omega$ is Scott's graph model. In this model the choice principle $AC_{2,0}$ is valid. But it is known that $AC_{2,0}$ together with extensionality of functions (which holds in every realizability model) is incompatible with existence of modulus of continuity. If I get a moment, I will fill in the details later.

See also M. Escardo, T. Streicher: In domain-realizability not all functionals are continuous, published in Mathematical Logic Quarterly, volume 48, issue Supplement 1, pages 41-44, 2002.