[plt-scheme] Standard ML in PLT Scheme

Shriram Krishnamurthi wrote:
> Hi Chongkai,
>
> I'm catching up on my email from having been away, so I've had a
> chance to read the whole thread before responding.
>
> On the one hand, I want to encourage you for doing what you are trying
> to do.  I'm sure interesting things will eventually come of this
> exercise, so keep pushing.
>
> On the other hand, I can't quite tell what it is you *are* trying, and
> at some point you seem to have stopped responding to the questions
> about static typing.  What is your bigger plan here?  Are you trying
> to implement Robby's paper, or what?
>
> Thanks,
> Shriram
>   

As I mentioned in one reply, in theory, it is possible to compile ML 
into typed-Scheme, which I think answered the static typing question. 
But in practice, there's some difficulties doing so:
1, unit.ss, as mentioned in a previous mail;
2, the type of ML records. Now ML record is mapped to Scheme hash table 
from symbol to value. There seems to be no existing support for such a 
type in typed-Scheme. Maybe I should also map ML records into Scheme 
structures (ML datatype is already maped to Scheme structure)?

For Robby's paper, as I understand, typed-Scheme implements it. Standard 
ML is more than typed lambda calculus, in that it has pattern match, 
module system, record, datatype, and so on.

As what I *am* trying, initially I was trying to build a Scheme version 
of HOL. Although the current version of "SML in PLT" have some small 
problems, I'm quiet sure that there is(will be) no difficulty to run 
large SML program such as HOL on it (and provides enough/minimal 
invariants as HOL needs). A question in my mind is: whether it is 
possible to express / macro-express SML in Scheme. It is time now to ask 
where to pushing next. Compiling into typed-Scheme seems to be a good goal.

Chongkai