[MLton] Question about Definition of SML :)

[Anoq of the Sun]

Stephen Weeks wrote:
> Actually that was my point :-) (and Andreas didn't like it).

OK - then I guess the quoting of who wrote what was confusing to me :)

> I can't
> quite see how I would formalize such a rule in the definition, though.

The way I would do it is to require each and every closure operation
to do a complete closure without allowing any free type variables.
This has been my (wrong) understanding of the closure operation all along.
Then I also require the value-restriction on each and every local
closure operation.

> Will you accept or reject
> 
>         val x = ref nil

I will reject it - due to value-restriction (and the truly "closing closure").

> If you reject this based on some local rule, you must presumably also
> reject
> 
>         val x = ref nil
>         val _ = 1 :: !x
> 
> and
> 
>         val _ =
>            let
>               val x = ref nil
>               val _ = 1 :: !x
>            in
>               ()
>            end

Yes, I would reject them all. As far as I know I have never written
any program SML myself where I have had a ref nil or ref NONE or similar
without also having a type constraint or that it was because of a polymorphic
parameter of a function.

So I would accept for instance:

fun f a =
      let
        val v = ref [a]
      in
        v
      end

Because a is scoped at the outer val-binding (fun).

> It sounds nice in principle, but in practice the problem is that a
> top-level declaration has an open-ended scope including the rest of
> the program.

Yes - I would also reduce the scope here to be just at each val binding.

But I would accept the following both at top-level and locally:

val rec x = ref nil
and     _ = 1 :: !x

Because of rec + and.

> Maybe.  I tend not to mind type constraintgs too.  I agree it would
> certainly be an interesting experiment to have a more constrained rule
> and see what happens.  Perhaps you would like to write one in MLton
> and try some real programs to see how many break?

I would actually very much like to try that as an experiment! Very good idea :)
But I believe I won't have time for this before the deadline of my project (19. dec).
So I guess I won't have time to use such feedback to influence my semantics before
I release it - but at least the semantics seems to just be more restrictive.
"Losening up" later on should not cause any incompatibilities (as it seems to me?).

> I mean to say that this program must be accepted.  And in fact all
> implementations accept it.  And I have never heard an argument that it
> may be rejected.

OK :)


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