On Tue, Jan 23, 2018 at 2:06 PM, Jeremy Yallop wrote: > > IHere's a closely > related property that's much harder to break: does adding annotations > leave the run-time behaviour of a program unchanged? There are far > fewer programs that violate that property, I think. > I'm no longer a type-theorist, so I don't have the knowledge to answer, but: It was a critically important property of *all* the original MLs (and of the theoretical development of ML) that a well-type ML program P could be "type-erased" to an untyped program TE(P); then when P -eval-> V, and TE(P) -eval-> V', TE(V) == V'. Where's I'm abusing notation, b/c "-eval->" means in the first case "evaluation on typed programs" and in the second, "evaluation on untyped programs" which might be entirely different things. This was the (famous amongst that admittedly tiny community) "commuting rectangles type erasure property". A -concrete- effect of this property in MLs (again, I'm no longer a type-theorist, so I might be getting this wrong) is ML-family languages don't support reflection, and when they support object-orientation, they don't support "instanceof" (e.g. like Java's). because these require that compile-time type-information be present at runtime. For those who think this is a bad design choice, I can only say that as a systems-jock, I appreciate a language that is -so- high-level, and -yet- can easily be programmed in such a way that I can understand the runtime behaviour in terms of a C-like runtime model. By contrast, to understand Java *for real* one must have enormously detailed knowledge of the JVM -- the particular JVM implementation -- one is using. --chet--