This is a pretty basic question about realizability interpretations. I am just starting to learn this subject so hopefully this question makes sense, please feel free to improve it. It seems that although statements in logic typically have little uniqueness in their proofs, there could/should be a lot more uniqueness in their realizers. The kind of example I have in mind is a proof of something like $ p \rightarrow (q \rightarrow p)$. Depending on the exact details of the interpretation, a realizer should be something like a function from p to functions from q to p, and the only sensible thing to do seems to be to associate to a given x in p, the constant function from q to p with value x.
Does anyone know if there has been work along these lines, or in general what work exists constraining the realizers of proofs?