🚀 go-pugleaf

In article <BzDIL1.B4I@cs.uiuc.edu> morrison@cs.uiuc.edu (Vance Morrison) writes:

>   The oddity is that a value can escape the scope in which its type
>   definition was made.   Thus
>
>
>	   let 
>	      datatype aType = constA | constB of int;
>	   in
>	      constA
>	   end;
>
>
>   This of course returns the value 'constA', in the outer scope, but
>   in this scope there is no type for this value!!

In a certain sense, this is not much different from the following:

	datatype aType = constA | constB of int;
	datatype aType = constB

The second type declaration overwrites the first,
but 'constA' is still visible and has a non-accessible type.

>   I tried this SML of NJ and it accepted it and returned the message
>
>		   val it = constA : ?.aType
>
>   It seems to me that this can cause problem with the sematics of
>   the language and would be a problem in any language that allows
>   type definitions in inner scopes.  

As my example shows, the problem (if it is one) could also occur in
languages without types in inner scopes.

In SML it does not have to be a problem,
but it is a bit tricky to correctly keep track of types.
The SML definition does _not_ correctly handle it and indeed you can
write programs that should pass the type-check (according to the
definition of SML), in which numbers are used as functions.
I have written a paper about errors like that in the SML definition,
which is currently under scrutiny.

It is not a problem in practice, because any implementation I know
implements this keeping track of types in a way which is
different from the Definition.
In particular, they all refuse these nasty programs that use numbers
as functions.

>   Now my problem is that I don't know what the exact problems this 
>   could cause, and I was hoping that those who have had more experience
>   both defining and implementing ML could give their input.  
>
>   I have a copy of the Definition of ML, so if something there would
>   make this clear, please feel free to refer to it.

A brief explanation how the SML Definition does it (and where the problem is):
Each new type gets a kind of Personal Identification Number,
the Definition calls it a "type name"
(not to be confused with a "type identifier").
Compatibility of types is checked by comparing the type names and
(if they are parameterised such as "list") by comparing their argument
types.  It does not matter at all whether these type names are
accessible via any type identifier, the only important thing is that
you have to make sure that any fresh type gets a fresh type name.
The \oplus operation in the static semantics takes care of that, it
not just adds an environment to the static context, it also grabs all
the type names that fly around somewhere in the environment to make
them known as non-fresh to the context.
The problem I mentioned is that this method of keeping track of type names
only works fine on the level of declarations,
it breaks for let-expressions.
After the declaration in a let-expression has been elaborated, its locally
produced type names are added to the context of the elaboration of the
body of the let-expression.  BUT: after elaborating the entire
let-expression, everything is back again to the context in which the
let-expression has been elaborated, i.e. WITHOUT the new type names.

The implementations do that sort of thing probably with a global
counter and a side-effect, in particular they do not reset the counter
after a let-expression (if they do -- Oh My!).


>   P.S.  :  I am also curious about a discussion about the problem
>	    with arbitrary Type definitions in signatures.  Unfortuately
>	    I did not save it.  If someone has the reference to the
>	    relevant passage in the Definition Book I would love to
>	    get that too.

The Definition does not make this explicit (perhaps the Commentary
does, I am not sure).  It is just excluded by the syntax.

Stefan


--
Stefan Kahrs	                   JANET:    smk@uk.ac.ed.dcs
LFCS, Dept. of Computer Science    Internet: smk@dcs.ed.ac.uk
University of Edinburgh            UUCP:     ..!mcsun!uknet!dcs!smk
Edinburgh
EH9 3JZ                            Tel:      (44)-31-650-5139
SCOTLAND                           Fax:      (44)-31-667-7209