[plt-scheme] Standard ML in PLT Scheme

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.

Chongkai