[plt-scheme] Standard ML in PLT Scheme

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