home *** CD-ROM | disk | FTP | other *** search
/ NetNews Usenet Archive 1992 #30 / NN_1992_30.iso / spool / comp / lang / function / 1476 < prev    next >
Encoding:
Internet Message Format  |  1992-12-21  |  4.6 KB
  1. Path: sparky!uunet!pipex!warwick!uknet!edcastle!dcs.ed.ac.uk!smk
  2. From: smk@dcs.ed.ac.uk (Stefan Kahrs)
  3. Newsgroups: comp.lang.functional
  4. Subject: Re: Values escaping their type definition
  5. Message-ID: <SMK.92Dec18141820@scarp.dcs.ed.ac.uk>
  6. Date: 18 Dec 92 14:18:20 GMT
  7. References: <BzDIL1.B4I@cs.uiuc.edu>
  8. Sender: cnews@dcs.ed.ac.uk (UseNet News Admin)
  9. Distribution: comp
  10. Organization: University of Edinburgh, LFCS
  11. Lines: 102
  12. In-Reply-To: morrison@cs.uiuc.edu's message of 16 Dec 92 22:31:49 GMT
  13.  
  14. In article <BzDIL1.B4I@cs.uiuc.edu> morrison@cs.uiuc.edu (Vance Morrison) writes:
  15.  
  16. >   The oddity is that a value can escape the scope in which its type
  17. >   definition was made.   Thus
  18. >
  19. >
  20. >       let 
  21. >          datatype aType = constA | constB of int;
  22. >       in
  23. >          constA
  24. >       end;
  25. >
  26. >
  27. >   This of course returns the value 'constA', in the outer scope, but
  28. >   in this scope there is no type for this value!!
  29.  
  30. In a certain sense, this is not much different from the following:
  31.  
  32.     datatype aType = constA | constB of int;
  33.     datatype aType = constB
  34.  
  35. The second type declaration overwrites the first,
  36. but 'constA' is still visible and has a non-accessible type.
  37.  
  38. >   I tried this SML of NJ and it accepted it and returned the message
  39. >
  40. >           val it = constA : ?.aType
  41. >
  42. >   It seems to me that this can cause problem with the sematics of
  43. >   the language and would be a problem in any language that allows
  44. >   type definitions in inner scopes.  
  45.  
  46. As my example shows, the problem (if it is one) could also occur in
  47. languages without types in inner scopes.
  48.  
  49. In SML it does not have to be a problem,
  50. but it is a bit tricky to correctly keep track of types.
  51. The SML definition does _not_ correctly handle it and indeed you can
  52. write programs that should pass the type-check (according to the
  53. definition of SML), in which numbers are used as functions.
  54. I have written a paper about errors like that in the SML definition,
  55. which is currently under scrutiny.
  56.  
  57. It is not a problem in practice, because any implementation I know
  58. implements this keeping track of types in a way which is
  59. different from the Definition.
  60. In particular, they all refuse these nasty programs that use numbers
  61. as functions.
  62.  
  63. >   Now my problem is that I don't know what the exact problems this 
  64. >   could cause, and I was hoping that those who have had more experience
  65. >   both defining and implementing ML could give their input.  
  66. >
  67. >   I have a copy of the Definition of ML, so if something there would
  68. >   make this clear, please feel free to refer to it.
  69.  
  70. A brief explanation how the SML Definition does it (and where the problem is):
  71. Each new type gets a kind of Personal Identification Number,
  72. the Definition calls it a "type name"
  73. (not to be confused with a "type identifier").
  74. Compatibility of types is checked by comparing the type names and
  75. (if they are parameterised such as "list") by comparing their argument
  76. types.  It does not matter at all whether these type names are
  77. accessible via any type identifier, the only important thing is that
  78. you have to make sure that any fresh type gets a fresh type name.
  79. The \oplus operation in the static semantics takes care of that, it
  80. not just adds an environment to the static context, it also grabs all
  81. the type names that fly around somewhere in the environment to make
  82. them known as non-fresh to the context.
  83. The problem I mentioned is that this method of keeping track of type names
  84. only works fine on the level of declarations,
  85. it breaks for let-expressions.
  86. After the declaration in a let-expression has been elaborated, its locally
  87. produced type names are added to the context of the elaboration of the
  88. body of the let-expression.  BUT: after elaborating the entire
  89. let-expression, everything is back again to the context in which the
  90. let-expression has been elaborated, i.e. WITHOUT the new type names.
  91.  
  92. The implementations do that sort of thing probably with a global
  93. counter and a side-effect, in particular they do not reset the counter
  94. after a let-expression (if they do -- Oh My!).
  95.  
  96.  
  97. >   P.S.  :  I am also curious about a discussion about the problem
  98. >        with arbitrary Type definitions in signatures.  Unfortuately
  99. >        I did not save it.  If someone has the reference to the
  100. >        relevant passage in the Definition Book I would love to
  101. >        get that too.
  102.  
  103. The Definition does not make this explicit (perhaps the Commentary
  104. does, I am not sure).  It is just excluded by the syntax.
  105.  
  106. Stefan
  107.  
  108.  
  109. --
  110. Stefan Kahrs                       JANET:    smk@uk.ac.ed.dcs
  111. LFCS, Dept. of Computer Science    Internet: smk@dcs.ed.ac.uk
  112. University of Edinburgh            UUCP:     ..!mcsun!uknet!dcs!smk
  113. Edinburgh
  114. EH9 3JZ                            Tel:      (44)-31-650-5139
  115. SCOTLAND                           Fax:      (44)-31-667-7209
  116.