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

[Chet Murthy <murthy.chet@gmail.com>]

[-- Attachment #1: Type: text/plain, Size: 1694 bytes --]

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

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

[-- Attachment #2: Type: text/html, Size: 2534 bytes --]