Re: [Caml-list] Are record types generative?

[Jacques Garrigue <garrigue@math.nagoya-u.ac.jp>]

On 2018/01/24 10:05, Chet Murthy wrote:
> 
> On Tue, Jan 23, 2018 at 2:06 PM, Jeremy Yallop <yallop@gmail.com> 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”.

This property is still true in OCaml (minus Obj.magic, but Obj.magic is not valid OCaml :-).
I.e., types can be used to optimize a program, but they do not change its semantics.
It’s true of so-called “overloaded” record labels, it’s true of a labeled and default arguments
(which use type information for compilation, but not semantics), it’s true of objects,
 it’s true of GADT pattern-matching (again optimized), etc…

> 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.

Indeed, as soon as we add type classes, type witnesses or (type-selected) implicit arguments, this property is lost.

> 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.


Indeed.

Jacques