sml-implementers

Re: [Sml-implementers] sharing vs. definitional specs

[Matthias B. <bl...@re...>]

Matthias Blume wrote:
> 
> I am still not convinced about the need for an asymetric "where type".
> Consider the following scenario (which, in fact, has happened to us
> in similar form, and it was a very annoying experience).
> 
> Suppose we have the following signatures A, B, C, and D:
> 
>    signature A = sig type a end
> 
>    signature B = sig type b end
> 
>    signature C = sig
>       structure A : A
>       structure B : B where type b = A.a * A.a
>    end
> 
>    signature D = sig type d
>                      val f : d -> unit
>                  end
> 
> Now, suppose further that we want to construct a signature E (perhaps
> the formal argument of a functor) consisting of two substructures that
> match C and D, respectively:
> 
>    signature E = sig
>       structure C : C
>       structure D : D
>    end
> 
> Further, we want to be able to apply D.f to values of type C.B.b, so
> we must specify that D.d and C.B.b are the same type.  All I want to
> convey to the compiler is that D.d = C.B.b, but I can't do this --
> neither using "sharing" nor using "where type" because C.B.b
> is not flexible anymore!  So I have to say something like:
> 
>    signature E = sig
>       structure C : C
>       structure D : D where type d = C.A.a * C.A.a
>    end
> 
> In other words, the language forces me to trace back what C.B.b was
> defined to be -- even though this information is completely
> irrelevant to what I am trying to express.  Moreover, it is
> intuitively clear that the compiler could infer the above automatically
> from the equation D.d = C.B.b.

Reviewing what I wrote I realize that D.d was still flexible so I could have
said  " ... D where type d = C.B.b".  But imagine D.d was also rigid already
for some reason, e.g., because D was defined as:

   signature D = sig type d0
                     type d = d0
                     val f : d -> unit
                 end

Now I would have to "know" that I have to apply the "where type" spec to d0
instead of d.  Changes to D which change how d was defined would break clients --
even though clients really didn't care about such details.  All they wanted to
say is that C.B.b = D.d.

Anyway, the rest of what I wrote stands...

> I see not conceptual difficulty with making "where type" (or any
> type abbreviation in signatures) symmetric.  The meaning should be this:
> An attempt is made to "unify" the two types in question, with currently
> "flexible" type names playing the roles of type variables.
> 
>   - "unifying" two flexible type names generates a traditional sharing
>     constraint for them, i.e., it throws the two names into an equivalence class
>   - "unifying" a rigid type name, i.e., one that already has a definitonal
>     spec, applies recursively to the RHS of its spec
>   - "unifying" a flexible type name with a type constructor application
>     generates a definitional spec for the name (and its equivalence class)
>   - "unifying" two type constructor applications with equal head constructor
>     causes the respective arguments to be "unified" recursively
>   - "unifying" two type constructor applications with unequal head constructor
>     causes elaboration to fail with an error message
> 
> Why can't we have this?  It seems simple and intuitive and expressive.
> 
> Matthias
> 
> _______________________________________________
> Sml-implementers mailing list
> Sml...@li...
> https://lists.sourceforge.net/lists/listinfo/sml-implementers

Re: [Sml-implementers] sharing vs. definitional specs

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

I don't understand the problem with using where type in your example.  Define
signature E as follows:

signature E = sig
  structure C : C
  structure D : D where type d = C.B.b
end

This is precisely an example of where a symmetric sharing constraint doesn't
work but an asymmetric where type constraint works fine.  Where type allows you
to introduce a type sharing between a flexible type in the signature and *any
other type* in the context of the signature.  Am I missing something here?

Derek

Matthias Blume wrote:
> 
> I am still not convinced about the need for an asymetric "where type".
> Consider the following scenario (which, in fact, has happened to us
> in similar form, and it was a very annoying experience).
> 
> Suppose we have the following signatures A, B, C, and D:
> 
>    signature A = sig type a end
> 
>    signature B = sig type b end
> 
>    signature C = sig
>       structure A : A
>       structure B : B where type b = A.a * A.a
>    end
> 
>    signature D = sig type d
>                      val f : d -> unit
>                  end
> 
> Now, suppose further that we want to construct a signature E (perhaps
> the formal argument of a functor) consisting of two substructures that
> match C and D, respectively:
> 
>    signature E = sig
>       structure C : C
>       structure D : D
>    end
> 
> Further, we want to be able to apply D.f to values of type C.B.b, so
> we must specify that D.d and C.B.b are the same type.  All I want to
> convey to the compiler is that D.d = C.B.b, but I can't do this --
> neither using "sharing" nor using "where type" because C.B.b
> is not flexible anymore!  So I have to say something like:
> 
>    signature E = sig
>       structure C : C
>       structure D : D where type d = C.A.a * C.A.a
>    end
> 
> In other words, the language forces me to trace back what C.B.b was
> defined to be -- even though this information is completely
> irrelevant to what I am trying to express.  Moreover, it is
> intuitively clear that the compiler could infer the above automatically
> from the equation D.d = C.B.b.
> 
> I see not conceptual difficulty with making "where type" (or any
> type abbreviation in signatures) symmetric.  The meaning should be this:
> An attempt is made to "unify" the two types in question, with currently
> "flexible" type names playing the roles of type variables.
> 
>   - "unifying" two flexible type names generates a traditional sharing
>     constraint for them, i.e., it throws the two names into an equivalence class
>   - "unifying" a rigid type name, i.e., one that already has a definitonal
>     spec, applies recursively to the RHS of its spec
>   - "unifying" a flexible type name with a type constructor application
>     generates a definitional spec for the name (and its equivalence class)
>   - "unifying" two type constructor applications with equal head constructor
>     causes the respective arguments to be "unified" recursively
>   - "unifying" two type constructor applications with unequal head constructor
>     causes elaboration to fail with an error message
> 
> Why can't we have this?  It seems simple and intuitive and expressive.
> 
> Matthias
> 
> _______________________________________________
> Sml-implementers mailing list
> Sml...@li...
> https://lists.sourceforge.net/lists/listinfo/sml-implementers

Re: [Sml-implementers] sharing vs. definitional specs

[Matthias B. <bl...@re...>]

"Derek R. Dreyer" wrote:
> 
> I don't understand the problem with using where type in your example.  Define
> signature E as follows:
> 
> signature E = sig
>   structure C : C
>   structure D : D where type d = C.B.b
> end
> 
> This is precisely an example of where a symmetric sharing constraint doesn't
> work but an asymmetric where type constraint works fine.  Where type allows you
> to introduce a type sharing between a flexible type in the signature and *any
> other type* in the context of the signature.  Am I missing something here?

Well, you are right, the example was not quite what I wanted it to be.  (Also, see the
followup to my own message.)

As long as one of the two sides of the equation is still flexible, you can add
a definitional spec.  However, sometimes this is not the case.  Moreover, when it is the
case, then it forces an ordering on other things: C _must_ come before D.  If there is
another pair of types for which you also want equality but where the flexible type is
in C, then you have a problem.

You can always get it to work by applying the recursive algorithm that I outlined 
"by hand".  But that is not very convenient, it may obscure what you are really
trying to say, and it is fragile with respect to future revisions.

Say D.d was defined to be some D.d' * D.d' (D.d' still being flexible).  Then all you
can do is express the desired type equality by saying "C.A.a = D.d'" -- which completely
obscures the original purpose of saying "D.d = C.B.b" and which will break if the
definition of D.d is changed to, say D.d'' * D.d'' at some later time.

Anyway, I don't see what the _advantage_ of the assymetric solution is.  I definitely see
its disadvantages, even though others might disagree with me as to whether these
disadvantages are really a big problem or not.  So all else being equal, I don't see why
we should not adopt a symmetric approach.

Matthias

> Matthias Blume wrote:
> >
> > I am still not convinced about the need for an asymetric "where type".
> > Consider the following scenario (which, in fact, has happened to us
> > in similar form, and it was a very annoying experience).
> >
> > Suppose we have the following signatures A, B, C, and D:
> >
> >    signature A = sig type a end
> >
> >    signature B = sig type b end
> >
> >    signature C = sig
> >       structure A : A
> >       structure B : B where type b = A.a * A.a
> >    end
> >
> >    signature D = sig type d
> >                      val f : d -> unit
> >                  end
> >
> > Now, suppose further that we want to construct a signature E (perhaps
> > the formal argument of a functor) consisting of two substructures that
> > match C and D, respectively:
> >
> >    signature E = sig
> >       structure C : C
> >       structure D : D
> >    end
> >
> > Further, we want to be able to apply D.f to values of type C.B.b, so
> > we must specify that D.d and C.B.b are the same type.  All I want to
> > convey to the compiler is that D.d = C.B.b, but I can't do this --
> > neither using "sharing" nor using "where type" because C.B.b
> > is not flexible anymore!  So I have to say something like:
> >
> >    signature E = sig
> >       structure C : C
> >       structure D : D where type d = C.A.a * C.A.a
> >    end
> >
> > In other words, the language forces me to trace back what C.B.b was
> > defined to be -- even though this information is completely
> > irrelevant to what I am trying to express.  Moreover, it is
> > intuitively clear that the compiler could infer the above automatically
> > from the equation D.d = C.B.b.
> >
> > I see not conceptual difficulty with making "where type" (or any
> > type abbreviation in signatures) symmetric.  The meaning should be this:
> > An attempt is made to "unify" the two types in question, with currently
> > "flexible" type names playing the roles of type variables.
> >
> >   - "unifying" two flexible type names generates a traditional sharing
> >     constraint for them, i.e., it throws the two names into an equivalence class
> >   - "unifying" a rigid type name, i.e., one that already has a definitonal
> >     spec, applies recursively to the RHS of its spec
> >   - "unifying" a flexible type name with a type constructor application
> >     generates a definitional spec for the name (and its equivalence class)
> >   - "unifying" two type constructor applications with equal head constructor
> >     causes the respective arguments to be "unified" recursively
> >   - "unifying" two type constructor applications with unequal head constructor
> >     causes elaboration to fail with an error message
> >
> > Why can't we have this?  It seems simple and intuitive and expressive.
> >
> > Matthias
> >
> > _______________________________________________
> > 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] compilation management

[Matthias B. <bl...@re...>]

Andrew Kennedy wrote:
> 
> (A) Agree on some way to map top-level SML Module identifiers (for
> structures, functors and signatures) to full file names identifying the
> file that contains the single binding for that Module entity (structure,
> functor or signature).

Sorry.  I will NEVER agree to that!

We had this discussion before in an OCaml vs. SML context.  A naming convention
such as the above can be used by an implementation, but it should _not_ be
the common ground on which we all live.  It is trivial to map implicit file
naming such as the one you suggest to explicit naming, but not vice versa.

As I said, I will try to come up with a simple (although perhaps verbose)
and very explicit description format that we all can implement.  Systems such
as CM or your implementation can take whatever scheme they use and _generate_
the explicit format.   It is unlikely that we will ever agree on a high-level
format (I for one will never agree to a modulename->filename mapping scheme,
and others seem to think that such as scheme is the only way they can accept),
so abstracting from this issue is the only way to go.

Matthias

Re: [Sml-implementers] compilation management

[John H. R. <jh...@re...>]

In message <BCD...@re...rp.microso
ft.com>, "Andrew Kennedy" writes:
>
> Our model consists of the following:
> 
> (A) Agree on some way to map top-level SML Module identifiers (for 
> structures, functors and signatures) to full file names identifying the 
> file that contains the single binding for that Module entity (structure,
> functor or signature).

I'm strongly opposed to requiring a fixed mapping from module names to
file names.  But it isn't necessary to have such a requirement on the
interchange format to support implementations that impose such a requirement.
If we have a mapping from module names to source files in the project
file, a simple script can generate a symbolic link "RedBlackSetFn" to
"red-black-set-fn.sml".  Of course, there are broken operating systems
that don't have symbolic links, but renaming would work for those cases.

I think that it is important the the interchange format not impose
unnecessary restrictions on library and application authors.  It should
be designed to make it as easy as possible to port existing code to
use the format.

	- John

Re: [Sml-implementers] compilation management

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

I would be interested to hear from other groups (Moscow ML, Poly/ML, ML Kit,
TILT) about the compilation management system they use.

Re: [Sml-implementers] compilation management

[Doug C. <e...@fl...>]

At 10:18 AM -0700 9/19/01, Stephen Weeks wrote:
>I would be interested to hear from other groups (Moscow ML, Poly/ML, ML Kit,
>TILT) about the compilation management system they use.

Porting Moscow ML 1.x to the Mac was hindered by the use of UNIX make 
files in the distribution. Ultimately I made several additions and 
changes to the Mac version of Moscow ML to enable full bootstrapping 
capability without external tools. I integrated the Moscow ML 
dependency generator and linker into the toplevel, along with a new 
make function that uses the dependencies to compute a compile 
ordering, and use file modification times to implement conditional 
compilation. The make function processes a directory at a time, with 
additional directory arguments as a search path for dependencies. 
This directory at a time approach follows from the organization of 
the distribution. With the new functions, Mac Moscow ML can rebuild 
itself from sources in less than a page of code.

Integrating the compile management and link mechanisms into the 
toplevel required very close coordination. There is a lot of state 
maintained by each of these pieces (toplevel, compiler, and linker) 
that needs to be kept independently and dynamically wound in and out 
as each of the pieces is invoked. Nevertheless, I found the end 
result invaluable in maintaining Moscow ML on a platform without the 
standard UNIX style development environment.

The tools in Moscow ML 1.x enforced a one to one correspondence 
between signatures (structures) and identically named .sig (.sml) 
files. This greatly simplified the dependency generator and linker.

More recent versions of Moscow ML (>= 2.0) support a "structure" mode 
wherein this correspondence is broken. We have experimented with a 
compilation manager that takes the "recursive list of files" 
approach, and a separate tool to discover the inter-file dependencies 
and compute these lists. This compilation manager abstracted the 
interface to the compiler; there are at least two concrete 
implementations: one uses the "system" call to invoke the compiler, 
and the other uses a compiler integrated into the toplevel, as with 
the Mac make function.

e

Re: [Sml-implementers] compilation management

[Ken F. L. <kf...@it...>]

Stephen Weeks <sw...@in...> writes:
> I would be interested to hear from other groups (Moscow ML, Poly/ML, ML Kit,
> TILT) about the compilation management system they use.

Let me reply about what Moscow ML and (partly) ML Kit use.

Moscow ML traditionally uses ordinary make and the distribution
includes a simpleminded dependency analysis tool.  But if you are
willing to commit to GNU make it is possible to make a generic
Makefile that will "just work" in most projects (it does take quite a
bit of make hacking).

I dislike make as much as any other sane person.  But it is standard
tool that many programmers know how to use.  And it is easy to
integrate components writen in another programming language such as C.

But Moscow ML 2.00 also came with mosmlpm[1], which is a project manager
that accepts the same project files (PM files) as the ML Kit (almost).
PM files are quite simple, the grammar is:

   pm ::=  "import" imports "in" body "end" 
       |   body

   imports ::= path.pm imports
            |  empty
  
   body ::=  path.sml body
         |   path.sig body
         |   "local" body "in" body "end" body
         |   empty

Where path is a unix-style path (much to Doug Currie's grief ;-), and
we also allow SML-style comments.  Example:

  import Ast.pm Lexer.pm Parser.pm in
     Typechecker.sml
     local Optimizer.sml in
       Compiler.sml
     end
  end

I like PM because it is *simple* and it is simple to explain what the
semantics of a PM file is (even with respect to side-effects!).  And
it is simple to implement.

I think PM is a good candidate for a common exchange format.  The only
flows I know of is:

  * No way to specify compiler options for a specific file (or a whole
    .pm file).  My suggestion is to extend the format to allow
    something like:

        | RedBlack.sml [mosml : "-orthodox", mlkit : "-inline 40 -fix-reduce"]

  * No way to make a big library pm file that exports other pm files
    (for example for the Basis Lib).


Martin Elsmann is the designer behind PM and I'll let him correct any
mistake I've made in the description above.


Cheers,

--Ken

[1] Unfortunately is mosmlpm still unannounced and a bit hard to find.
But those who are interested can find a quick prototype in
mosml/src/mosmlpm in the Moscow ML distribution.