[plt-scheme] Standard ML in PLT Scheme

On Dec 22, 2007 3:16 PM, Richard Cobbe <cobbe at ccs.neu.edu> wrote:
> On Sat, Dec 22, 2007 at 11:20:16AM -0500, Sam TH wrote:
> > On Dec 22, 2007 9:08 AM, Chongkai Zhu <czhu at cs.utah.edu> wrote:
>
> > > 2.Dynamically typed code is the only thing available in PLT at run time.
> > > Even typed Scheme turns everything into a dynamically typed world after
> > > static type checking.
>
> > This is true, but somewhat misleading.  Every programming language,
> > typed or untyped, is ultimately executed on the untyped processor.
>
> To borrow a phrase, this is true but irrelevant.  :-)
>
> The untyped processor (at least on modern stock hardware like ppc or i386)
> doesn't unconditionally and automatically insert tag checks that are
> unnecessary if your source language has a sound type system.  This is what
> I understood to be the point of Tomi Neste's question up-thread.

I disagree.  In almost any case where a language that ensures some
invariant is translated to a different language that doesn't ensure
that invariant, dynamic checks are inserted instead.  For example, in
Standard ML, invalid memory accesses are impossible, but nonetheless
checked by the lower-level system (in this case, the OS).  Similarly,
in most languages, unaligned memory accesses are impossible, but
nonetheless checked dynamically by the hardware (I think).

Similarly, when ML was first implemented on top of Lisp, some of the
inserted dynamic checks were irrelevant.  But this would have been the
case if ML had been implemented as an interpreter in Lisp, instead of
a compiler to Lisp.

If we wanted to, we could implement a processor that performed only
the required dynamic checks for our language of choice.  But in the
absence of a Lisp machine revival, and in the absence of a desire to
compile everything to OS-free machine code, we have to put up with a
world that doesn't enforce the invariants of our particular type
system, and will instead dynamically check some things that are
unnecessary.

Thanks,
-- 
sam th
samth at ccs.neu.edu