[plt-scheme] Standard ML in PLT Scheme

On Dec 20, 2007 4:17 PM, Chongkai Zhu <czhu at cs.utah.edu> wrote:
> Matthias Felleisen wrote:
> >
> > On Dec 20, 2007, at 3:11 PM, Chongkai Zhu 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
> >
> > This is unlikely unless you also impose contracts, which you haven't
> > shown.
> >
> > Export f : int -> int from an ML unit and in a Scheme unit, run (f
> > true). Please let us know what the result is.
> >
> > -- Matthias
>
>
> By "can't violate an ML invariant in pure ML", I mean if you only use ML
> (i.e. is not allowed to write any Scheme code).
>
> I have read the popl07 paper, and the typed Scheme implementation.
> Basicly they say you need contracts on the interface between two
> language to keep the invariant. I don't have them. Since the ML code is
> actually run as Scheme code, the run time type check will caught those
> errors.
>

What does run like Scheme code mean? Dynamic typing from what I infer.
Is this a desirable feature? If so, why?

What about the other way around? How do you deal with statically typed
ML functions calling dynamically typed Scheme functions?

Marco