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