… which got it, I think, from Milner's exposition; see, for example, p. 351 of https://www.sciencedirect.com/science/article/pii/0022000078900144 https://www.sc

… which got it, I think, from Milner's exposition; see, for example, p. 351 of https://www.sciencedirect.com/science/article/pii/0022000078900144 https://www.sciencedirect.com/science/article/pii/0022000078... . This notation makes particular sense for function types, where a mathematician would write `f : A → B` even if not thinking type-theoretically.