[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.

> It makes sense, but I don't quite see how to fit this idea in the
> mathematical framework of the Definition.  You seem to need some way
> to look at properties of the set of possible elaborations, which is
> much more than a side condition on some inference rule.  It also
> sounds like there is some similar confusion as Andreas talked about
> between type variables as in the Definition and "unknown types" (often
> represented or displayed as type variables) used in an implementation.
> 
> But I will gladly await your document to see more detail :-).

The way I do it is in my description of the closure operation.
Here I include all inferred free types (which I actually describe
quite thoroughly as being meta variables in my unification
framework). I have described it as if the value restriction
appiles to both explicitly mentioned and implicitly inferred
type variables. Actually, to begin with I also thought this
was just a mistake in the Definition to forget these :)

And since I quantize everything at every point of closure
I believe there is no problem. The problem of finding an
elaboration thus also becomes a much more local problem.

Anyway - the closure operation would be the place to read
carefully in my spec. :) I really hope to get it out
tonight. It seems to continue to take longer time
because I continue to find little gritty details which
needs fixing (now at least it's mostly in the syntax rather
than the semantics ;)
But things seems to be OK now - just need the final
cleanup of the last descriptions now :)


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