On Thu, 11 Nov 2010, Brian Huffman wrote:
Hello everyone,
The recent appearance of some new warning messages got me thinking
about transparent-vs-opaque ascription again. (I.e. "structure Foo :
FOO = struct ... end" vs "structure Foo :> FOO = struct ... end")
http://isabelle.in.tum.de/repos/isabelle/rev/daaa0b236a3f
The log message is also important here: "... saves extra paragraph in
implementation manual", i.e. this warning was meant to simplify life as
much as possible.
Here is the reason I am reluctant to use transparent ascription:
Programmers use modules and signatures as an abstraction mechanism. (I
shouldn't need to explain to anyone on this list why abstraction in
programming is a good thing.) But transparent ascription makes it easy
to accidentally break module abstractions: If signature FOO contains an
abstract type like "type foo" (with no definition in the signature), and
structure Foo implements it with a type synonym like "type foo = int",
then the ascription Foo : FOO will make "Foo.foo = int" globally
visible, violating the abstraction specified in the signature and
breaking modularity.
The way signatures and structures are used in Isabelle is more like "table
of contents" vs. "body text". I.e. the signature tells about intended
exports without necessarily abstracting the representation fully. There
are some modules that need to be fully abstract, and this is where abstype
is used with plain-old ":" matching. Moreover, in recent years we did
narrow-down the signatures more systematically, to delimited the
boundaries of modules more clearly, although some people have occasionally
complained about that.
When SML90 was young, other ways of module abstraction were propagated by
some authors of text books. I vaguely remember the "functorial style"
that was still present in our sources in the early 1990-ies, and greatly
complicating things until Larry purged it in one big sweep.
When SML97 came out, we adopted few of its features and ignored many new
problems introduced by the general NJ approach to ML. I don't think you
want to have their fixed-precisions ints or 8-bit characters, or worse
16bit wide chars.
Nonetheless, I started using opaque signature matching for some kernel
modules some years ago, for the reasons you have given above. This
destroyed the toplevel pretty printers for SML/NJ and recent Poly/ML. It
required a long time until the problem was detected, and eliminated by
going back to plain old ":" with "abstype".
This demonstrates once more, that anything coming from the 97/NJ update of
the SML language needs to be treated with extreme care.
Now I have spent much more than a paragraph ...
Makarius
_______________________________________________
Isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
