[isabelle-dev] Transparent/opaque module signature ascription

[Makarius]

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