[plt-scheme] Standard ML in PLT Scheme

On Dec 20, 2007 2:11 PM, Chongkai Zhu <czhu at cs.utah.edu> wrote:
> Matthias Felleisen wrote:
> >
> > Are the denotations of 1 the same in ML as in Scheme? How about closures?
> >
> > Conjecture: It looks like you have created an unsound hybrid language.
> > I.e., unsound from the perspective of ML; its invariants can be
> > undermined now.
> >
>
> My conjecture is that if type-inference (which includes type checking)
> of haMLet is used, you can't violate an ML invariant in pure ML: you
> have to do it in Scheme.

Of course. But you do allow Scheme programs and ML programs to
communicate, don't you? Maybe worth having a look at this paper:

http://people.cs.uchicago.edu/~robby/pubs/papers/popl2007-mf-color.pdf

(there's also a bw version, suitable for printing on my web page)

Robby