[MLton] free type variables in datatype decs

[Claudio Russo]

The reason I believe it to be sound is that the Moscow "Definition"
prevents any local typename from escaping via the type of the let
expression and the the context itself. Without this restriction, it
would indeed be unsound. For Moscow, I wanted to relax the SML
restriction because it seemed unnecessary and got in the way of Moscow's
generalised modules constructs. Lambda lifting a type just to avoid the
closure restriction means changing its arity, which changes the type
declarations it can match in a signature.

The 1997 Definition (Rule 4) does states that the type of a let
expression must not contain new type names, but unfortunately, rule 17
only requires
that the freshly generated type name for a datatype doesn't appear in T
of C, not tynames(C) (free names appearing in C), so I think allowing
open datatype definitions in ML would probably be unsound.

If you relax the closure condition in the Definition, without
strengthening the freshness constraint on datatypes, 
the following function would elaborate (it doesn't in Moscow):

fun f r = let datatype t = C of 'a in r:= SOME (C,fn C x => x) end: 
: !'a. ('a -> C * C -> 'a) option ref -> unit;

It would now be easy to do nasty stuff that goes wrong.

Claudio
> -----Original Message-----
> From: Ken Friis Larsen [mailto:ken@friislarsen.net] 
> Sent: Thursday, February 03, 2005 8:12 PM
> To: mlton@mlton.org
> Cc: Peter Sestoft; Claudio Russo
> Subject: Re: [MLton] free type variables in datatype decs
> 
> Matthew Fluet wrote:
> > Perhaps.  But it appears that MLton is going out of its way 
> to choose 
> > a solution at odds with every other SML compiler.  And, 
> there is very 
> > little practical benefit of MLton's behavior over the 
> no-free-type-vars solution.
> 
> This is not exactly true.  If you give Moscow ML 2.01 the program
> 
> val id = fn x =>
>     let
>        datatype z = Z of 'a
>        val unZ = fn Z x => x
>     in
>        unZ (Z x)
>     end;
> 
> Then it will accept the program but gives you the following warning:
> 
> !       datatype z = Z of 'a
> !                         ^^
> ! Compliance Warning:
> ! The phrase, although accepted as a Moscow ML extension, ! 
> is not supported by the Definition of Standard ML:
> ! the type variable
> !   'a
> ! should be a parameter of the datatype binding
> 
> [Unless you start Moscow ML with the flag -orthodox, in which 
> case all such warnings are treated as errors; or similar if 
> you start Moscow ML with flag -liberal, in which case all 
> such warnings are suppressed.]
> 
> Likewise if you give Moscow ML the program:
> 
> > Note, that the example given in mlton.org/FunctionalRecordUpdate
> > 
> > fun << ({a, b, c}, (f, z)) =
> >    let
> >       datatype t = A of 'a | B of 'b | C of 'c
> >       fun g h z =
> >          {a = case h z of A a => a | _ => a,
> >           b = case h z of B b => b | _ => b,
> >           c = case h z of C c => c | _ => c}
> >    in
> >       f {a = g A, b = g B, c = g C} z
> >    end
> 
> You'll get the above warning three times, one for each of the 
> constructors A, B, and C.
> 
> And if you try to give it Andreas' example:
> 
>    datatype t = C of 'a
>    fun cast x = case C x of C x' => x'
>    val ouch = 1 + cast "string"
> 
> Then you get the error:
> 
> ! Toplevel input:
> ! ..datatype t = C of 'a
> !   fun cast x = case C x of C x' => x'
> !   val ouch = 1 + cast "string"
> ! Unguarded type variables at the top-level
> 
> 
> I'll leave it to Claudio to explain why it is sound :-)
> 
> Thus, I think that MLton's behaviour is perfectly reasonable.
> 
> 
> Cheers,
> 
> --Ken
>