[MLton] free type variables in datatype decs
Stephen Weeks
MLton@mlton.org
Thu, 3 Feb 2005 16:16:44 -0800
> I have another, deeper technical argument: allowing val-bound type
> variables in type declarations destroys a very strong design
> invariant of SML, namely that the denotation of an explicit type
> declaration never depends on any implicitly passed type information.
I'm afraid I can't get much meaning out of this. Consider the
following two fragments
A.
type u = int
type t = u * u
B.
fun 'a f (x: 'a) =
let
type t = 'a * 'a
in ...
In what way does the definition of t in (B) depend on "implicitly
passed type information" more than the definition in (A)? Both simply
refer to types (which are in scope).
How about the following fragment.
C.
functor F (type a) =
struct
fun f x =
let
type t = a * a
in ... end
end
This is very similar to (B) -- I've just lifted the polymorphism up to
the module level. This is valid SML, and again I don't see how the
type information in (B) is any more implicit.
> In the implementation of Alice ML, which incorporates a form of
> module-level dynamics, this is very important. It allows us to
> employ the usual type-erasing compilation strategy for polymorphic
> functions, although we have to maintain dynamic type information for
> all explicit type declarations. With the more liberal rule this
> would no longer work, and we needed a costly type-passing
> translation for all polymorphic functions.
I'm treading on thin-ice understanding here, since MLton's ILs are
typeful. But, it seems like type erasure basically means using a
universal type. If that's the case, then why can't you simply replace
uses of 'a with that universal type when you erase its binding
occurrence.
I don't see why this needs to affect compilation beyond the front end,
since local {dat,typ}binds that refer to free type variables can be
easily expanded into a form in which they don't, and this can be
implemented as a source-to-source translation on SML. In fact, that's
exactly what MLton does in its front end.