# [MLton] Question about Definition of SML :)

Anoq of the Sun anoq@HardcoreProcessing.com
Thu, 27 Nov 2003 20:42:17 +0200

Hello!

I have a question which is not due to MLton - but maybe you guys
know this. Especially maybe Matthew knows after implementing
the front-end? :)

Anyway - I'm not sure about the purpose of the restriction:

tynames VE \subseteq T of C

in the rulle (26) p. 24 in the Definition of SML.

I can see the purpose of the limitation:

tynames \tau \subseteq T of C

in rule (4) p. 21. It prevents that one returns
datatypes out of the scope where they are defined.

As far as I can see, the restriction:

tynames VE \subseteq T of C

in rule (14) p. 23 does the same to ensure that
one doesn't unpack an exception with a datatype
value which was raised out of scope from where
it was declared.

However, isn't the rule (26) redundant then? The
restriction should be there already because of rule (14)
(because an exception will have to go through a handle clause
to re-enter the program).
Or is there something special about the recursive
binding? And in case it's not redundant, why not?
And shouldn't it be in rule (25) as well then?

More concretely: I would very much like to see a
program which fails to type-check due to the
limitation in rule (26).

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