[MLton] Question about Definition of SML :)

[Anoq of the Sun]

Stephen Weeks wrote:
> This seems like a problem to me, since the Definition requires if some
> elaboration succeeds (i.e. there is an element in the inductively
> defined relation), then the type inference should find it.  So, you
> have to find some way to prevent the elaboration that avoids type
> variables entirely.

Actually, if you look at rule (15) in the Definition of SML you
will see the side-condition:

U \cap tyvars VE' = \emptyset

This forces all "implicitly scoped" type variables to be bound
by the closure operation in ML.

In my semantics I have inference
rules for inferring these implicitly scoped type variables.
I also maintain those during the inference in an environment
that I call \Delta. At a val binding the \Delta contains
those type variables which are already implicitly scoped
by an enclosing val-binding (and \Delta' contains those
implicitly scoped that that val binding).
I have now changed my side condition here to be (the equivalent of):

tyvars VE' \backslash tyvars \Delta = \emptyset

This should hopefully be enough to ensure that all
free type variables are bound by each closure operation.

Actually my static semantics is not even recursive.
So I shouldn't even have to do any fixpoint iteration
anywhere to implement this semantics. So I think this
all makes the entire semantics quite simple to implement.

As you can see from my post on the MLton-user list,
my spec. is finally available now :)


Cheers
-- 
http://www.HardcoreProcessing.com