🚀 go-pugleaf

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

> 	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!!

More precisely, it returns a value that the compiler knows how to print
as constA, of a type which you have no way to name.  Why is that any
more disturbing from this?

	let
	   datatype aType = constA | constB of int
	   type aType = int
	in
	   constA
	end

Here you can mention constA but you can't write its type either, because
aType is hidden.

Incidentally, in both cases, aType, constA, and constB are out of scope
after the `end' and you can't use any of them.
-- 
				--Andrew Koenig
				  ark@europa.att.com

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;
[ Gives ?.aType as a type.]
From what I recall, this isn't a really big problem because you can't
do anything with those values.  This occurs in a similar and possible
more obnoxious way with exceptions, I think you can look that up in
the SML manual, I know it's discussed somewhere.
This problem can also occur with recursive types and stuff like that.
It doesn't break the typechecking of the system, and I don't think it
causes any substantial semantical problems since you can't operate on
the values anymore.
          -Eric 
*********************************************************
"Overhead, without any fuss, the stars were going out."
           -The Nine Billion Names of God
"Yes, you're very smart.  Shut up."
           -In "The Princess Bride"
*********************************************************

In article <BzDIL1.B4I@cs.uiuc.edu>, morrison@cs.uiuc.edu (Vance Morrison) writes:
> I have just realized something about ML that I find rather odd and 
> I am hoping to get some advice about consequences.
> 
> 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!!
> 
> 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.  
> 
> 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.
> 
> Vance

Doesn't the "?.aType" mean that the object has a hidden type, ie a type inaccessible
in the current type environment. There is nothing you can actually do with the
returned value, so no problems should occur.

   .
   |on Hanson
 `-' jaxh@dcs.ed.ac.uk

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