Re: datatype constructor as syntax

On Sat, Mar 22, 2014 at 6:08 PM, Phil Clayton <[email protected]> wrote:
> 20/03/14 12:51, Matthew Fluet wrote:
>> On Wed, Mar 19, 2014 at 7:37 PM, Phil Clayton <[email protected]> wrote:
>>> 19/03/14 19:16, Matthew Fluet wrote:
>>>> On Tue, Dec 31, 2013 at 3:47 AM, Florian Weimer <[email protected]> wrote:
>>>>> * Henry Cejtin:
>>>>>
>>>>>> Sorry,  I  thought  I  was  being  clever,  but  if  you look at Andreas
>>>>>> Rossberg's Defects in the Revised Definition of Standard ML
>>>>>>       http://www.ps.uni-saarland.de/Publications/documents/Rossberg_DefectsSML.pdf
>>>>>> you will see that he points out that rule 126 of the  dynamic  semantics
>>>>>> implies  that  this  should really give you a bind exception at runtime.
>>>>>> This was fixed (meaning you get the in MLton way back in 2001 to give an
>>>>>> error at compile time.
>>>>>
>>>>> Curiously, the fun-based approach
>>>>>
>>>>>     datatype mytype = foo | bar of int
>>>>>     fun bar _ = ()
>>>>>     val bar = 23
>>>>>
>>>>> still runs without raising an exception when compiled with MLton.
>>>>
>>>> That seems to be an oversight.
>>>
>>> Perhaps I missed the point here but I'm hoping that it's intentional
>>> that MLton allows the status of a constructor id to be overwritten by a
>>> fun binding.
>>
>> The issue is that the static semantics specified in the Definition
>> allows a 'val rec' (and, therefore, a 'fun') declaration to override
>> the constructor status of an identifier, but the dynamic semantics of
>> a 'val rec' (and, therefore, a 'fun') declaration does not override
>> the constructor status, and hence binding attempts to perform a
>> pattern match that necessarily fails with a Bind exception.
>>
>> It seems that most SML implementations resolve this inconsistency by
>> adopting a dynamic semantics where a 'val rec' declaration does
>> override the constructor status.
>>
>> MLton, on the other hand, resolves this inconsistency by adopting a
>> static semantics where a 'val rec' declaration is not allowed to
>> override the constructor status of an identifier.  This was adopted in
>> 2004 (https://github.com/MLton/mlton/commit/110d6b6) as part of
>> Stephen's implementation of a proper front end.  I looked at the mail
>> archive from the time of the commit, but couldn't find any discussion
>> as to why the choice was to change the front end, rather than
>> documenting a deviation from the Definition with respect to the
>> dynamic semantics.
>
> Thanks for the explanation.  Do you have plans to change MLton to align
> 'val rec' and 'fun'?  (Changing both to follow the Definition seems
> least useful, in my humble opinion.)

I agree that following both rule 26 and rule 126 of the Definition
isn't particularly useful.

I did a little more digging in the MLton repository.  Henry is correct
that the issue with rules 26 and 126 were identified and addressed in
2001 (https://github.com/MLton/mlton/commit/1140673) thanks to Andreas
Rossberg's tests.  Interestingly, in order to properly implement rule
126, the type checker explicitly introduced a "raise Bind" expression
when a "val rec" pattern included a constructor:
https://github.com/MLton/mlton/commit/1140673#diff-866cd04R628.  Thus,
the normal behavior of elaboration would have been to implement a
dynamic semantics where the constructor status was overridden.
Presumably, this is why most implementations follow rule 26, but not
rule 126 --- its the natural implementation.

Given the comments in the Definition, it seems clear that the authors
meant for 'val rec' to allow an identifier's constructor status to be
overridden and it would seem natural for the dynamic semantics to also
allow an identifier's constructor status to be overridden.

I'm tempted to introduce a new MLB annotation: valrecConstr
{error|warn|ignore}  (which would also affect 'fun' declarations).
'error' would correspond the the current behavior, report an error
(which terminates compilation) if a 'val rec'/'fun' declaration
overrides an identifier's constructor status; 'warn' would accept but
warn if an identifier's constructor status was overridden (without
terminating compilation), and the dynamic semantics would also
override the identifier's constructor status (i.e., the natural
implementation); 'ignore' would silently accept if an identifier's
constructor status was overridden (without terminating compilation),
and the dynamic semantics would also override the identifier's
constructor status (i.e., the natural implementation).

To unsubscribe from this group and stop receiving emails from it, send an email to [email protected].

------------------------------------------------------------------------------
Learn Graph Databases - Download FREE O'Reilly Book
"Graph Databases" is the definitive new guide to graph databases and their
applications. Written by three acclaimed leaders in the field,
this first edition is now available. Download your free book today!
http://p.sf.net/sfu/13534_NeoTech