[isabelle-dev] Transparent/opaque module signature ascription

[Brian Huffman]

On Fri, Nov 12, 2010 at 5:48 AM, Makarius <makarius at sketis.net> wrote:
> On Thu, 11 Nov 2010, Brian Huffman wrote:
>> 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.

So basically, you're saying that you normally don't care about
abstraction, except in the few special cases where you use abstype.
Maybe I do need to explain why abstraction is a good thing...

> 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.

The way to avoid such complaining is to make all modules as abstract
as possible in the first place. Of course, retrofitting a
more-abstract interface onto an existing module will cause some pain
for users of that module, who may have written problematic code that
doesn't follow the abstract discipline. But better now than later,
because otherwise users will continue to write more undisciplined,
error-prone code.

> 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.

The functorial style may have been cumbersome, but at least it
enforced module abstractions.

> When SML97 came out, we adopted few of its features and ignored many new
> problems introduced by the general NJ approach to ML.
[...]
> This demonstrates once more, that anything coming from the 97/NJ update of
> the SML language needs to be treated with extreme care.

I'm afraid your ad hominem attacks on the SML97/NJ group don't carry
much weight with me.

- Brian