sml-implementers — Standard ML implementers

Re: [Sml-implementers] Structure sharing and type abbreviations

[Andreas R. <ros...@ps...>]

Dave Berry wrote:
> 
> Should we also consider supporting "where structure..."? And perhaps
> removing the "and" derived form of "where type...", which I believe is
> ambiguous.

It is not ambiguous, only tedious to parse. As it stands this part of
the grammar is LALR(2) but a bunch of ugly transformations can turn it
into LALR(1). Of course, it is pretty useless anyway.

Regarding "where" for structures: I second it would be great if all
implementations supported it (together with a derived form for
definitional structure specifications) since that would allow getting
rid of sharing constraints in programs altogether. IMHO this would be
preferable to relying on a relaxed structure sharing semantics.

Still I think adopting the proposal is a good idea. I would also opt for
variation 2 since I do not see any application for such obfuscated uses
of sharing (but maybe I'm just not imaginative enough...)

BTW, another old issue that definitely ought to be fixed by all
implementations: allow the "datatype ... withtype" derived form in
signatures...

	- Andreas

-- 
Andreas Rossberg, ros...@ps...

"Computer games don't affect kids; I mean if Pac Man affected us
 as kids, we would all be running around in darkened rooms, munching
 magic pills, and listening to repetitive electronic music."
 - Kristian Wilson, Nintendo Inc.

Re: [Sml-implementers] Sensible Structure Sharing for Standard ML

[Derek R. D. <dr...@cs...>]

No, Leaf, I think Martin is saying that "structure sharing is
transitive, etc." for *his* rule that he's proposing, not for ours. 
Likewise, he's saying that *his* rule is less permissive than the
Definition, not ours.  I'm still trying to decipher what Martin's rule
does, but it seems quite unrelated to our proposal, so I'm not sure what
Martin means by saying it is "based on" our proposal, maybe that it is
based on the alternative proposal idea described on part 4 of our
Discussion section.  Perhaps, Martin, you could explain what it does in
layman's terms?

In particular, I am still somewhat mystified by the requirement that
\rea(E_1) = ... = \rea(E_n).  This would seem to force the signatures of
all structures being shared to be pretty much identical.  For instance,
it would seem to force all the structures to have exactly the same set
of value components.  Why?  I mean it's an interesting idea, but perhaps
overly restrictive.  Am I wrong about my interpretation of your rule,
Martin?  Examples of how it works (of the sort we gave in our design
note) would help.

Thanks!
Derek

Leaf Eames Petersen wrote:
> 
> Martin -
> 
> Thanks for taking the time to look into this.  I have a couple
> questions about one of your comments though:
> 
> >    1. Structure sharing is transitive, reflexive, and commutative,
> 
> I don't believe that this is true.  Consider the following spec
> 
> structure A : sig type t end
> structure B : sig type s end
> structure C : sig type t end
>  sharing A = B
>  sharing B = C
> 
> This does not introduce the same equations as "sharing A = C", which
> is what I would expect you to mean by transitive.  Perhaps you
> mean that structure sharing is transitive for the subset of the
> type names common to all the signatures in question?
> 
> >       thus the rule is less permissive than SML'97 in this respect;
> >       see The Def. page 85.
> 
> Our intention was to make our version strictly more permissive in the
> sense that all structure sharings accepted by the Definition would
> still be accepted by our proposal, and have the same effect.  Are you
> claiming that this is not the case?  If so, can you give an example of
> something that breaks?
> 
> Cheers,
> Leaf
> 
> _______________________________________________
> Sml-implementers mailing list
> Sml...@li...
> https://lists.sourceforge.net/lists/listinfo/sml-implementers

Re: [Sml-implementers] Sensible Structure Sharing for Standard ML

[Leaf E. P. <le...@cs...>]

Martin - 

Thanks for taking the time to look into this.  I have a couple
questions about one of your comments though:

>    1. Structure sharing is transitive, reflexive, and commutative,

I don't believe that this is true.  Consider the following spec

structure A : sig type t end
structure B : sig type s end
structure C : sig type t end
 sharing A = B
 sharing B = C

This does not introduce the same equations as "sharing A = C", which
is what I would expect you to mean by transitive.  Perhaps you
mean that structure sharing is transitive for the subset of the
type names common to all the signatures in question?

>       thus the rule is less permissive than SML'97 in this respect;
>       see The Def. page 85.

Our intention was to make our version strictly more permissive in the
sense that all structure sharings accepted by the Definition would
still be accepted by our proposal, and have the same effect.  Are you
claiming that this is not the case?  If so, can you give an example of
something that breaks?

Cheers,
Leaf

Re: [Sml-implementers] Sensible Structure Sharing for Standard ML

[Martin E. <ma...@di...>]

Hi again,

The rule for structure sharing specifications I posted earlier
contained yet a few flaws related to getting the unification of type
names right. Based on the suggestion by Derek Dreyer and Leaf
Petersen, here is my third go for a rule for structure sharing
specifications:
                                                    +----------------+
                                                    | B |- spec => E |
                                                    +----------------+

              B |- spec => E                E_i = E(longstrid_i)
        (\rea_(j-1) o ... o \rea_1)(E_i(longtycon_j)) = (t_ij, VE_ij)
      t_ij \not\in T of B     \rea_j = { t_1j -> t_j, ..., t_nj -> t_j }    
      t_j \in {t_1j, ..., t_nj}     t_j admits equality, if some t_ij does
   \rea = \rea_k o ... o \rea_1     \rea(E_1) = ... = \rea(E_n)     i=1..n, j=1..k
  ----------------------------------------------------------------------------
         B |- spec sharing longstrid_1 = ... = longstrid_n => \rea(E)

Notes:

   1. Structure sharing is transitive, reflexive, and commutative,
      thus the rule is less permissive than SML'97 in this respect;
      see The Def. page 85.

      Reflexivity:
         If   B |- spec => E   and    E' = E(longstrid)  
         then   B |- spec sharing longstrid = longstrid => E

      Reflexivity':
         If   B |- spec sharing longstrid_1 = ... = longstrid_n => E
         then   B |- spec sharing longstrid_1 = ... = longstrid_n
                          sharing longstrid_1 = ... = longstrid_n => E

      Commutivity: 
         If   B |- spec sharing longstrid_1 = longstrid_2 => E 
         then    B |- spec sharing longstrid_2 = longstrid_1 => E 

      Commutivity': 
         If   B |- spec sharing longstrid_1 = ... = longstrid_n
                        sharing longstrid_1' = ... = longstrid_m' => E
         then  B |- spec sharing longstrid_1' = ... = longstrid_m'
                         sharing longstrid_1 = ... = longstrid_n => E

      Transitivity:    
         If   B |- spec sharing longstrid_1 = longstrid_2
                        sharing longstrid_2 = longstrid_3 => E 
         then    B |- spec sharing longstrid_1 = longstrid_2
                           sharing longstrid_1 = longstrid_3 => E

   2. The requirement \rea(E_1) = ... = \rea(E_n) forces all long type
      constructors bound to flexible type names to be considered.

In the framework of my thesis work, the rule may be formulated as
follows; see chapters 2 and 3 of my thesis:
                                                    +-------------------+
                                                    | B |- spec => T(E) |
                                                    +-------------------+

              B |- spec => (T)E              E_i = E(longstrid_i)
        (\rea_(j-1) o ... o \rea_1)(E_i(longtycon_j)) = (t_ij, VE_ij)
      t_ij \in T     \rea_j = { t_1j -> t_j, ..., t_nj -> t_j }    
      t_j \in {t_1j, ..., t_nj}     t_j admits equality, if some t_ij does
   \rea = \rea_k o ... o \rea_1     \rea(E_1) = ... = \rea(E_n)     i=1..n, j=1..k
  ----------------------------------------------------------------------------
         B |- spec sharing longstrid_1 = ... = longstrid_n => (T)(\rea(E))

In this framework, a realisation-closedness property holds:

 Proposition 3.1.10: Let phrase be either a specification or a
 signature expression. If   B |- phrase => (T)E    then
    1.  tynames((T)E) \subseteq tynames(B)
    2.  \rea(B) |- phrase => \rea((T)E) for any realisation \rea

Proposition 3.1.10, which is essential for a proof of type-safety,
continues to hold with the rule for structure sharing added. (This is
not surprising, but important, nevertheless.)

Cheers,

Martin

RE: [Sml-implementers] Structure sharing and type abbreviations

[Dave B. <da...@ta...>]

At 16:27 10/09/2001, Stephen Weeks wrote:
>> The official definition of structure sharing is useless; 
>
>This is an overstatement,

Indeed, the official definition of structure sharing satisfies one clear
requirement: it simplifies the porting of SML'90 code to SML'97.  The
original draft of SML'97 deleted the structure sharing construct
altogether, and one of the reasons for keeping it as a derived form was
precisely to simplify the porting of SML'90 code.  Of course, SML'90 didn't
allow type abbreviations in signatures, so the problems found by the TILT
team didn't arise.

>although I would agree that the effect of the
>definition is to strongly encourage a programming style in which type
>definitions do not appear in signatures. 

Given the history, the intent might have been more to discourage a
programming style that uses the structure sharing derived form.
Personally, I find it occasionally useful, e.g. when a structure contains
all the type definitions for a type checker or for an abstract syntax, in
which cases the large number of type sharing equations would be unwieldy.
If MLWorks ever makes it to open source (which seems unlikely after all
this time), I'd be happy to implement a more permissive regime.  Of the
choices offered by the TILT team, I would be conservative and plump for the
error option.

Should we also consider supporting "where structure..."?  And perhaps
removing the "and" derived form of "where type...", which I believe is
ambiguous.

Dave.

 

Re: [Sml-implementers] Sensible Structure Sharing for Standard ML

[Martin E. <ma...@di...>]

Hi again,

The rule for structure sharing I posted earlier contained a few flaws;
a better rule is given below.

Based on the suggestion by Derek Dreyer and Leaf Petersen, I came up
with the following rule for structure sharing specifications:

           B |- spec => E      E_i = E(longstrid_i)     i=1..n
    E_i(longtycon_j) = (t_ij, VE_ij)     t_ij \not\in T of B     i=1..n, j=1..k
               \rea_j = { t_1j -> t_j, ..., t_nj -> t_j }    j=1..k  
             t_j admits equality if some t_ij does,  j=1..k
          \rea = \rea_k o ... o \rea_1     \rea(E_1) = ... = \rea(E_n)
    ----------------------------------------------------------------------------
           B |- spec sharing longstrid_1 = ... = longstrid_n => \rea(E)

Notes:

   1. Structure sharing is transitive, reflexive, and commutative,
      thus the rule is less permissive than SML'97 in this respect;
      see The Def. page 85.

   2. The requirement \rea(E_1) = ... = \rea(E_n) forces all long type
      constructors bound to flexible type names to be considered.

I counted the number of structure sharing constraints in the ML Kit
sources and found 123 such constraints, thus I won't consider the
SML'97 notion of structure sharing completely useless. On the other
hand, if the major sml-implementers agree on some (better) rule for
structure sharing, I would consider implementing the rule in the ML
Kit implementation.

Cheers,

Martin

Re: [Sml-implementers] Sensible Structure Sharing for Standard ML

[Martin E. <ma...@di...>]

Hi there,

Based on the suggestion by Derek Dreyer and Leaf Petersen, I came up
with the following rule for structure sharing specifications:

    B |- spec => E              E_i = E(longstrid_i)                     i=1..n
    E_i(longtycon_j) = (t_ij, VE_ij)     t_ij \not\in T of B     i=1..n, j=1..k
    \rea = { t_11 -> t_1, ..., t_1k -> t_1, ..., t_n1 -> t_n, ..., t_nk -> t_n }
    t_i admits equality if some t_ij does                        i=1..n, j=1..k
                               \rea(E_1) = ... = \rea(E_n)
    ----------------------------------------------------------------------------
           B |- spec sharing longstrid_1 = ... = longstrid_n => \rea(E)

Notes:

   1. Structure sharing is transitive, reflexive, and commutative,
      thus the rule is less permissive than SML'97 in this respect;
      see The Def. page 85.

   2. The requirement \rea(E_1) = ... = \rea(E_n) forces all long type
      constructors bound to flexible type names to be considered.

The question is whether the requirement \rea(E_1) = ... = \rea(E_n) is
too strong for some practical purposes? I counted the number of
structure sharing constraints in the ML Kit sources and found 123 such
constraints, which would all elaborate with the rule above. Although I
do not consider the SML'97 notion of structure sharing completely
useless, I would consider implementing a (better) rule for structure
sharing in the ML Kit implementation if the major sml-implementers
would agree on such a rule.

Cheers,

Martin

[Sml-implementers] Sensible Structure Sharing for Standard ML

[Derek R. D. <dr...@cs...>]

A question arose on the sml-implementers list about the way structure sharing is
defined in SML '97.  The issue is that the Definition has the effect of
precluding the appearance of type abbreviations in the signatures of the
structures being shared.  Below is a design note describing a new more
permissive definition of structure sharing that we have implemented in the TILT
compiler.

 ------------------------------------------
|Sensible Structure Sharing for Standard ML|
 ------------------------------------------

Introduction
------------

The topic of structure sharing came up a while back in the context of
the TILT compiler, and we spent quite a bit of time heatedly hashing
this out.  The consensus was that structure sharing as defined by the
Definition is overly restrictive to the point of being useless, since
you can rarely share structures whose signatures contain any type
definitions.  SML/NJ extends the Definition to allow sharing between
structures whose signatures are the same signature *variable*.  This
seems to cover most cases that come up in practice, but the limitation
to signature variables was felt to be somewhat arbitrary.  In
addition, it seems strange that one cannot replace an occurrence of a
signature variable with the signature it is supposed to abbreviate.

In this note, we will present our proposal for sensible structure
sharing.  It is strictly more permissive than both the Definition and
SML/NJ.  First, we will go into some detail on the Definition of type
and structure sharing, for those not intimately familiar with the
details.  Some terminology given here (some from the Definition, some
of our own) will be important in the subsequent description of our
proposal.


The Details of the Problem
--------------------------

1) How is structure sharing Defined?

The Definition says that the (n-ary) structure sharing specification

> spec sharing A1 = ... = An

is a derived form that expands out to "spec" modified by a series of
type sharing constraints, each of the form

> sharing type Ai.longtycon = Aj.longtycon

for every pair of longtycons Ai.longtycon and Aj.longtycon specified
by the spec such that 1 <= i < j <= n.  Below, we will refer to any
such pair as "type components of the same name".  Note that sharing
occurs here between pairs of type components, so there is no
requirement that the type components being shared need to exist in all
the structures.  This leads us to:

2) How is type sharing Defined?

The problem is that type sharing constraints are only permitted
between abstract types defined in the spec.  Actually, the Definition
is slightly looser: type sharing is permitted only between type
components that denote "flexible type names" of the same "arity".  A
flexible type name is an abstract type name that was introduced by the
spec being constrained.  The arity of a type is the number of type
variables it is parameterized over.  For example, consider the spec

> type s
> type t = s
> type u
> type v = u

Introducing a sharing type constraint between any two types here is
legal because all of them are equal to abstract types introduced by
the spec.  (Sharing between (s and u), (s and v) or (t and v) would
introduce a sharing constraint between s and u, and any other sharing
would add no constraints.)  Now, consider the following spec:

> type s
> type t = s * s
> type u
> type v = u * u

The only legal sharing type constraint we can add to this spec is
between s and u, because neither t nor v denotes a flexible type name.
We will say that the "flexible type components" of a spec are the
longtycons defined by the spec that denote flexible type names.  It
should be noted that the set of flexible types of a spec remains the
same after a sharing type constraint is introduced --- the sharing has
the effect of equating the type names that each flexible type denotes,
but they are still flexible.

So, in summary, the problem is that sharing between structures that
have any non-flexible (for instance, transparent) type components of
the same name, will expand into a bunch of sharing type constraints,
including some between the non-flexible components, which are illegal.
This seems overly restrictive: at a minimum, it seems silly not to be
able to share between two structures that have *equivalent*
signatures.


Our Proposal
------------

The core proposal is that structure sharing will induce type sharing
constraints between all pairs of flexible type components of the same
name and arity (and only those components).  In other words, it will
only expand into the type sharing constraints that are guaranteed to
be legal.  This completely defines what spec is generated from the
(n-ary) structure sharing constraint.

The remainder of the proposal involves what extra "sanity" checks are
performed after the sharing between the flexible components has been
added to the spec.  There are two variations to this, both of which
are implemented in almost exactly the same way.  The plan is to make
the choice between them a flag in the compiler.

In both variations, any pair of non-flexible type components of the
same name and arity which denote equivalent types (or type
constructors) will be silently accepted.  This allows for the
signatures of two structures being shared to contain transparent type
definitions, so long as they are equivalent.

In the first variation, all other pairs of type components of the same
name will generate a compiler warning.

In the second variation, all other pairs of type components of the
same name will generate a compiler error.

So for example, consider the following varieties of behavior for

> structure A : sig A_spec end
> structure B : sig B_spec end
> sharing A = B

depending on what A_spec and B_spec are:

A_spec          B_spec		variation 1	variation 2
--------------------------------------------------------------
type t		type t		A.t = B.t	A.t = B.t
--------------------------------------------------------------
type t = int	type t = int	silent accept	silent accept
--------------------------------------------------------------
type t		type t = int	warning		reject (error)
--------------------------------------------------------------
type t = int	type t = bool	warning		reject (error)


Discussion
----------

1) It is important that the sharing between the flexible components be
added to the spec first, before the extra checks are performed.  For
example, consider the following:

> structure A : sig type t type s = t * int end
> structure B : sig type t type s = t * int end
> sharing A = B

In this case, A.s and B.s are only equivalent *after* the sharing
of A.t and B.t is added to the spec, so the sharing between all
flexible type components must be added first.

2) It is worth noting that, in variation 1, structure sharing is
always legal; the compiler may just whine a lot if you use it weirdly.

3) Why bother with the two variations?  At the time we studied this
issue, we couldn't agree on which was better and it seemed easy to
implement them both.  The distinction comes up in the case that there
are two type components of the same name that cannot be shared (as in
the third and fourth pairs of specs above).  The Definition of course
says to reject such cases.  When one of the types is flexible, one
could attempt to implement real sharing here, using a "where type" or
something to realize the flexible component in terms of the
non-flexible one, but it is unclear how to do this in general.
Consider for example,

> structure A : sig type a  type t        type s = a*a end
> structure B : sig type b  type t = b*b  type s end
> sharing A = B

Therefore, we decided that no definitions would be introduced in this
case, and that the compiler would emit either a warning or an error.

The argument for raising an error is that in some sense a structure
sharing spec can be thought of as a check, in addition to simply as a
mechanism for introducing type sharing specs.  It seems
counter-intuitive that a structure sharing spec can succeed without
all of the types present in both signatures being equal.  Raising an
error means that if a sharing spec is actually accepted, then any two
type components of the same name are known to be equal.

The argument for a warning is that the programmer might wish to share
two such signatures without expecting that all of the types will be
made equal, and hence should be allowed to do so.  However, at the
least a warning is desired to indicate that not all type components
of the same name can be made equal.

4) Another alternative idea we discussed was to give a stronger
meaning to multiple structure sharing specs, namely to only add type
sharing constraints between type components existing in all the
structures (as opposed to any two).  This seems like a reasonable
approach, but we opted against it because it causes some valid SML
programs to be rejected (i.e. it is not strictly more permissive than
the Definition).  For example,

> structure A : sig type t end
> structure B : sig type s end
> structure C : sig type t end
> sharing A = B = C

induces the sharing of A.t and C.t according to the Definition (and
thus our proposal), but no sharing according to the stronger idea
outlined above (since t is not present in the signature of B).
Admittedly, this is a stupid example.  We would be interested to know
if there are any examples of real SML programs that would not
typecheck under a stronger interpretation of multiple structure
sharing that induces less type sharing in this fashion.


Credits
-------

This proposal arose out of extended discussions among the TILT
developers:
  Robert Harper
  Karl Crary 
  Perry Cheng
  Derek Dreyer 
  Joshua Dunfield
  Tom Murphy
  Leaf Petersen
  Chris Stone
  David Swasey
  Joe Vanderwaart

Comments and suggestions are appreciated as always, especially
regarding the question of whether the first or second variation is
preferable.

Derek Dreyer & Leaf Petersen

RE: [Sml-implementers] Structure sharing and type abbreviations

[Stephen W. <sw...@in...>]

> The official definition of structure sharing is useless; 

This is an overstatement, although I would agree that the effect of the
definition is to strongly encourage a programming style in which type
definitions do not appear in signatures.  For example, I count 97 uses of
structure sharing in MLton, which is written using this style.  I don't find
completely avoiding type definitions in signatures very restrictive.

RE: [Sml-implementers] Could raise be non-expansive?

[Robert H. <Rob...@cs...>]

The issue is not one of soundness, but rather of semantic sensibility.
Essentially, it never makes sense in a CBV language to substitute a general
expression for a variable, unless that expression is known to be (tantamount
to) a value.  The basis for polymorphism in ML is the substitution
principle: behave as if the variable were replaced by its definition.  But
when the binding is not (tantamount to) a value, it is senseless to perform
the substitution that polymorphism required.

(None of this arises in a CBN language, precisely because you may always
substitute a variable by an expression without restriction.  In this sense
ML style polymorphism, as originally defined, is a CBN notion, and does not
make good sense for a CBV interpretation of let.)

One can also see the problem by considering a type reconstruction
interpretation of ML.  The expression /\t.hd[t](nil), which would arise by
pattern compilation followed by generalization from a binding such as val
h::t = nil, is a value --- it does not raise an exception (until it is
used).  But in the untyped semantics of ML the val binding itself raises an
exception.  So type reconstruction changes the semantics, which should not
be the case.

IMO the only sensible route is to assess valuability ("non-expansiveness")
only after pattern compilation.  This can be done neatly in the framework of
The Definition by restricting polymorphism to irrefutable patterns, and only
then if the rhs is valuable ("non-expansive").  In the presence of refutable
patterns conditions on the rhs alone are insufficient.

Bob

-----Original Message-----
From: Dave Berry [mailto:da...@ta...]
Sent: Saturday, September 08, 2001 5:17 PM
To: Robert Harper; 'Dave Berry'; sml...@li...
Subject: RE: [Sml-implementers] Could raise be non-expansive?


Thanks Bob.  

Please could you give an example program that would be unsound?  I'd like
to understand where the problem occurs.  

At 21:01 07/09/2001, Robert Harper wrote:
>I intend the second interpretation.  The explicit raise is
indistinguishable
>from the implicit raise caused by matching an expression against a
refutable
>pattern.
>
>The issue has nothing whatsoever to do with "generating names", whatever
>those are.
>
>Bob

RE: [Sml-implementers] Could raise be non-expansive?

[Dave B. <da...@ta...>]

Thanks Bob.  

Please could you give an example program that would be unsound?  I'd like
to understand where the problem occurs.  

At 21:01 07/09/2001, Robert Harper wrote:
>I intend the second interpretation.  The explicit raise is indistinguishable
>from the implicit raise caused by matching an expression against a refutable
>pattern.
>
>The issue has nothing whatsoever to do with "generating names", whatever
>those are.
>
>Bob

RE: [Sml-implementers] Could raise be non-expansive?

[Robert H. <Rob...@cs...>]

I intend the second interpretation.  The explicit raise is indistinguishable
from the implicit raise caused by matching an expression against a refutable
pattern.

The issue has nothing whatsoever to do with "generating names", whatever
those are.

Bob

-----Original Message-----
From: Dave Berry [mailto:da...@ta...]
Sent: Friday, September 07, 2001 6:50 PM
To: Robert Harper; 'Dave Berry'; sml...@li...
Subject: RE: [Sml-implementers] Could raise be non-expansive?


At 11:54 07/09/2001, Robert Harper wrote:
>I mistakenly reversed the senses of "expansive" and "non-expansive", as
must
>be obvious to everyone.  Sorry about that.


Hi Bob,

I'm afraid I'm now confused, as I can see two possible interpretations of
your message.  Please can you tell me which you intended?

Example:
	exception Foo
	val it = raise Foo
raise Foo has type 'a; can 'a be generalised?

First interpretation:  Yes, 'a can be generalised.  The definition should
be changed to allow this, thus removing an inconsistency between an
explicit raise and the implicit raise caused by a refutable pattern.

Second interpretation:  No, 'a can not be generalised.  The definition
should be changed to also ban the generalisation of type variables in any
expression matched against a refutable pattern, regardless of whether the
rhs expression is expansive.

FWIW, the Commentary only discusses the question of generating exception
names.  If I understand correctly, simply raising an exception doesn't
generate a new name.

Dave.

RE: [Sml-implementers] Could raise be non-expansive?

[Dave B. <da...@ta...>]

At 11:54 07/09/2001, Robert Harper wrote:
>I mistakenly reversed the senses of "expansive" and "non-expansive", as must
>be obvious to everyone.  Sorry about that.


Hi Bob,

I'm afraid I'm now confused, as I can see two possible interpretations of
your message.  Please can you tell me which you intended?

Example:
	exception Foo
	val it = raise Foo
raise Foo has type 'a; can 'a be generalised?

First interpretation:  Yes, 'a can be generalised.  The definition should
be changed to allow this, thus removing an inconsistency between an
explicit raise and the implicit raise caused by a refutable pattern.

Second interpretation:  No, 'a can not be generalised.  The definition
should be changed to also ban the generalisation of type variables in any
expression matched against a refutable pattern, regardless of whether the
rhs expression is expansive.

FWIW, the Commentary only discusses the question of generating exception
names.  If I understand correctly, simply raising an exception doesn't
generate a new name.

Dave.

RE: [Sml-implementers] Could raise be non-expansive?

[Robert H. <Rob...@cs...>]

I mistakenly reversed the senses of "expansive" and "non-expansive", as must
be obvious to everyone.  Sorry about that.

Bob

-----Original Message-----
From: Robert Harper [mailto:Rob...@cs...]
Sent: Friday, September 07, 2001 10:19 AM
To: 'Dave Berry'; sml...@li...
Subject: RE: [Sml-implementers] Could raise be non-expansive?


Yes it can, and it should.  The name "non-expansive" was already obsolete
and misleading by the SML 97 revision, but was retained for continuity's
sake.

This brings up a related question of whether other expressions that may
raise an exception are to be non-expansive.  A typical example is the
binding

	val x as _::_ = nil

whose right-hand side is deemed "non-expansive", yet the binding for x is
uncons(nil) (in the obvious sense), which may raise an exception.  The
binding for x should be considered non-expansive, and hence non-polymorphic.

More generally, for val bindings whose pattern is refutable (ie, there
exists a value not matching it), the variables involved should not be
generalized.  For irrefutable patterns, they should be generalized iff the
rhs is syntactically non-expansive in the current sense (which is, of
course, conservative).

Bob

-----Original Message-----
From: Dave Berry [mailto:da...@ta...]
Sent: Wednesday, September 05, 2001 5:13 PM
To: sml...@li...
Subject: [Sml-implementers] Could raise be non-expansive?


Am I right in thinking that the definition of non-expansive expressions
could be extended with "raise nexp", with no ill-effects?  I'm not
suggesting that such a minor change is worthwhile; I'm just curious.

Dave.

_______________________________________________
Sml-implementers mailing list
Sml...@li...
https://lists.sourceforge.net/lists/listinfo/sml-implementers

_______________________________________________
Sml-implementers mailing list
Sml...@li...
https://lists.sourceforge.net/lists/listinfo/sml-implementers

RE: [Sml-implementers] Could raise be non-expansive?

[Robert H. <Rob...@cs...>]

Yes it can, and it should.  The name "non-expansive" was already obsolete
and misleading by the SML 97 revision, but was retained for continuity's
sake.

This brings up a related question of whether other expressions that may
raise an exception are to be non-expansive.  A typical example is the
binding

	val x as _::_ = nil

whose right-hand side is deemed "non-expansive", yet the binding for x is
uncons(nil) (in the obvious sense), which may raise an exception.  The
binding for x should be considered non-expansive, and hence non-polymorphic.

More generally, for val bindings whose pattern is refutable (ie, there
exists a value not matching it), the variables involved should not be
generalized.  For irrefutable patterns, they should be generalized iff the
rhs is syntactically non-expansive in the current sense (which is, of
course, conservative).

Bob

-----Original Message-----
From: Dave Berry [mailto:da...@ta...]
Sent: Wednesday, September 05, 2001 5:13 PM
To: sml...@li...
Subject: [Sml-implementers] Could raise be non-expansive?


Am I right in thinking that the definition of non-expansive expressions
could be extended with "raise nexp", with no ill-effects?  I'm not
suggesting that such a minor change is worthwhile; I'm just curious.

Dave.

_______________________________________________
Sml-implementers mailing list
Sml...@li...
https://lists.sourceforge.net/lists/listinfo/sml-implementers

RE: [Sml-implementers] Structure sharing and type abbreviations

[Robert H. <Rob...@cs...>]

Hello everyone!

We've hashed this one out locally.  Derek Dreyer and Leaf Petersen will
shortly post a summary of our approach.  The official definition of
structure sharing is useless; something else must be adopted.

Best,
Bob

-----Original Message-----
From: David Matthews [mailto:Dav...@pr...]
Sent: Thursday, September 06, 2001 5:40 AM
To: sml...@li...
Subject: [Sml-implementers] Structure sharing and type abbreviations


Dave's question reminded me that there was something that I had been
meaning to ask.  Structure sharing in ML97 is defined as a textual
expansion of type abbreviations.  So if we have
signature S = sig type s type t end
signature T = sig structure A: S and B: S sharing A=B end
then this is equivalent to
signature T = sig structure A: S and B: S sharing type A.s=B.s sharing
type A.t=B.t end

But this seems, if I have understood correctly, to have a problem if s
or t are anything but a type name.  e.g.
signature S = sig type s type t = s * s end
signature T = sig structure A: S and B: S sharing A=B end
appears to be illegal, even though its meaning is perfectly clear.  

This was actually brought to my attention some time ago by Frank
Pfenning who had some code which had compiled under SML/NJ but was
rejected by Poly/ML.  My feeling is that although this is strictly
illegal there is a strong case for allowing it on pragmatic grounds.  Is
my interpretation correct and what do other implementations do?

David.


_______________________________________________
Sml-implementers mailing list
Sml...@li...
https://lists.sourceforge.net/lists/listinfo/sml-implementers

[Sml-implementers] Structure sharing and type abbreviations

[David M. <Dav...@pr...>]

Dave's question reminded me that there was something that I had been
meaning to ask.  Structure sharing in ML97 is defined as a textual
expansion of type abbreviations.  So if we have
signature S = sig type s type t end
signature T = sig structure A: S and B: S sharing A=B end
then this is equivalent to
signature T = sig structure A: S and B: S sharing type A.s=B.s sharing
type A.t=B.t end

But this seems, if I have understood correctly, to have a problem if s
or t are anything but a type name.  e.g.
signature S = sig type s type t = s * s end
signature T = sig structure A: S and B: S sharing A=B end
appears to be illegal, even though its meaning is perfectly clear.  

This was actually brought to my attention some time ago by Frank
Pfenning who had some code which had compiled under SML/NJ but was
rejected by Poly/ML.  My feeling is that although this is strictly
illegal there is a strong case for allowing it on pragmatic grounds.  Is
my interpretation correct and what do other implementations do?

David.

Re: [Sml-implementers] Could raise be non-expansive?

[Mads T. <to...@it...>]

Dear Dave
Sounds plausible.
Best regards,
Mads


Dave Berry wrote:
> 
> Am I right in thinking that the definition of non-expansive expressions
> could be extended with "raise nexp", with no ill-effects?  I'm not
> suggesting that such a minor change is worthwhile; I'm just curious.
> 
> Dave.
> 
> _______________________________________________
> Sml-implementers mailing list
> Sml...@li...
> https://lists.sourceforge.net/lists/listinfo/sml-implementers

[Sml-implementers] Could raise be non-expansive?

[Dave B. <da...@ta...>]

Am I right in thinking that the definition of non-expansive expressions
could be extended with "raise nexp", with no ill-effects?  I'm not
suggesting that such a minor change is worthwhile; I'm just curious.

Dave.

[Sml-implementers] PR opportunity

[Daniel W. <da...@CS...>]

Just wanted to make sure everyone new about 
 http://www.bagley.org/~doug/shootout/

It's been around for quite some time, but just got a lot of PR by showing up
on Slashdot. MLton and SML/NJ are already on the list. It be nice to see
MoscowML and some of the other implementation's show up. We can't let OCaml
steal all the hacker mind share. 

[Sml-implementers] SML/NJ test suite imported as test/smlnj

[Dave M. <db...@re...>]

I've imported the SML/NJ regression test suite into the sml CVS
repository as test/smlnj.  Our testing scripts will not be of
direct use to other implementations, since they are based on diffing
against reference output files, so any difference with SML/NJ output
will be counted as failure.  However, the test files themselves will
mostly be appropriate for other implementations.

I hope that other implementers will follow up by importing their test
suites, and then we can perhaps find volunteers to work on a unified
test suite.

The SML/NJ benchmarks should be imported soon, at benchmarks/smlnj.

Dave

[Sml-implementers] standardml.org URLs working

[David M. <db...@re...>]

Thanks to Tom Murphy (tom7), the URLs standardml.org and
www.standardml.org
now point to the SourceForge Standard ML project web page.

A reminder -- the fact that you are on this mailing list does not imply
that
you are a member of the Standard ML project at SourceForge.  To become a
project member, you'll need to create a user account and send your
SourceForge
login name to one of the project administrators.  You can check the
membership
of the project at the project summary page:

  <https://sourceforge.net/projects/sml>

Dave
-- 
Dave MacQueen
mac...@re...
Room 2C-480, Bell Labs, 600 Mountain Ave, Murray Hill, NJ 07974

Re: [Sml-implementers] SML sourceforge project

[Dave M. <db...@ns...>]

> From:  Peter Sestoft <se...@di...>
> To:    Dave MacQueen <db...@re...>
> Cc:    sml...@li...
> Date:  Sat, 17 Feb 2001 12:57:08 +0100
> Subject: Re: [Sml-implementers] SML sourceforge project

> On Thu, 15 Feb 2001, Dave MacQueen wrote:
> 
> > I intend to import the SML/NJ test suites as test/smlnj in the
> > repository
> 
> I'll do the same for Moscow ML's Basis Library test suite, then.
>  
> > 3. I plan to expand on the web pages, with at least a list of links
> > to the web pages of all Standard ML implementations.  
> 
> Already it's quite useful: I wasn't aware of the current state of
> Poly/ML, for instance.
> 
> >   ML Kit
> >     Ken Larsen (kf...@it...)
> >     Mads Tofte (to...@it...)
> > 
> >   Moskow ML
> >     Peter Sestoft (se...@di...)
> >     Martin Elsman (ma...@di...)
> 
> Actually, the assignment of people is more like this:
> 
>    ML Kit
>      Mads Tofte (to...@it...)
>      Martin Elsman (ma...@di...)
>      Niels Hallenberg (nh...@it...)
>  
>    Moscow ML
>      Claudio V. Russo (cr...@mi...)
>      Doug Currie (e...@fl...)
>      Ken Friis Larsen (kf...@it...)
>      Peter Sestoft (se...@di...)
> 
> I hope this represents what people are doing (Claudio is working on
> MLJ/SML.NET also, of course).
> 
> Peter

I've made the change to my list and added Doug Currie to the
sml-implementers mailing list.  I had also included Sergei Romanenko
(responsible for the Moscow in "Moscow ML"?).  Should I drop his name?

  Moscow ML
    Peter Sestoft (se...@di...)
    Doug Currie (e...@fl...)
    Ken Larsen (kf...@it...)
    Sergei Romanenko (ro...@ke...)
    Claudio Russo (Cla...@cl...)

Dave

Re: [Sml-implementers] SML sourceforge project

[Peter S. <se...@di...>]

On Thu, 15 Feb 2001, Dave MacQueen wrote:

> I intend to import the SML/NJ test suites as test/smlnj in the
> repository

I'll do the same for Moscow ML's Basis Library test suite, then.
 
> 3. I plan to expand on the web pages, with at least a list of links
> to the web pages of all Standard ML implementations.  

Already it's quite useful: I wasn't aware of the current state of
Poly/ML, for instance.

>   ML Kit
>     Ken Larsen (kf...@it...)
>     Mads Tofte (to...@it...)
> 
>   Moskow ML
>     Peter Sestoft (se...@di...)
>     Martin Elsman (ma...@di...)

Actually, the assignment of people is more like this:

   ML Kit
     Mads Tofte (to...@it...)
     Martin Elsman (ma...@di...)
     Niels Hallenberg (nh...@it...)
 
   Moscow ML
     Claudio V. Russo (cr...@mi...)
     Doug Currie (e...@fl...)
     Ken Friis Larsen (kf...@it...)
     Peter Sestoft (se...@di...)

I hope this represents what people are doing (Claudio is working on
MLJ/SML.NET also, of course).

Peter

[Sml-implementers] Test-suite for ML compilers

[Niels H. <nh...@it...>]

Hi all,

first of all, this mailing list is a great initiative.

At ITU, we are working on the next release of the ML Kit (url:
http://www.it-c.dk/research/mlkit/) and are currently testing that
everything works. To that end, it would be very nice, if some of you
are sitting on SML programs that are suitable to include in our test
suite. The ML Kit implements most of the basis library, so large
programs with structures and functors etc. would be very nice. We have
already included many test programs from the New Jersey implementation
and test programs for the basis library from the Moscow ML
implementation.

If you are sitting on test programs that you would like to share with
us and other SML implementers, then we will also include the
test-programs in the ML Kit distribution, so that we can build up a
large collection of programs that can be compiled out of the box on
most ML compilers implementing the basis library. The value of having
a large repository of test programs is priceless.

Below I list some of the programs that are currently in our test
suite:

  tmergesort.sml 
  qsort.sml      
  mandelbrot.sml 
  life.sml      
  knuth_bendix.sml        
  simple.sml     
  fft.sml           
  vliw.sml          
  lexgen.sml        
  mlyacc.pm         
  logic.pm          
  barnes-hut.pm     
  nucleic.pm        
  ray.pm            
  ratio-regions.sml 
  msort.pm          

-- Niels
-------------------------------------------------------
Niels Hallenberg                 Email: nh...@it...
The IT University of Copenhagen  Tel.:  +45-38 16 88 24
Glentevej 67                     Fax:   +45-38 16 88 99
DK-2400 Copenhagen NV            WWW:   www.it.edu
-------------------------------------------------------