  We introduce a syntactic translation of Goedel's System T parametrized by a
weak notion of a monad, and prove a corresponding fundamental theorem of
logical relation. Our translation structurally corresponds to Gentzen's
negative translation of classical logic. By instantiating the monad and the
logical relation, we reveal the well-known properties and structures of
T-definable functionals including majorizability, continuity and bar recursion.
Our development has been formalized in the Agda proof assistant.
