[plt-scheme] Standard ML in PLT Scheme

From: Marco Morazan (morazanm at gmail.com)
Date: Sat Dec 22 00:11:39 EST 2007

Matthias has given you a good piece of advice.

A question that is sure to come up: Why, after static type checking,
would you turn everything into a dynamically typed world?

If you have a good argument for this, I would be delighted to hear it.

Cheers,

Marco

On Dec 21, 2007 12:49 PM, Chongkai Zhu <czhu at cs.utah.edu> wrote:
>
> Marco Morazan wrote:
> > 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
> >
>
>
> Run *as* Scheme code. After compiling, there is NO ml code at all.
> Everything is turned into dynamically-typed Scheme code.
>
> Chongkai
>
>
>


Posted on the users mailing list.