I'm reading Practical Foundations for Programming Languages by Robert Harper and am confused by the exercises in Chapter 4, "Statics", where he discusses a (monomorphic) type system. The exercise instructs to provide an "operational" reading to typing judgements by refining $e : \tau$ relation in...