[isabelle-dev] Transparent/opaque module signature ascription

[Brian Huffman]

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

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.

To see how widespread this situation is in Isabelle, I did a little
experiment this morning. I did a search-and-replace on all ML files in
src/Pure to use opaque ascription everywhere, and then compiled Pure
and HOL to see what would break. Here's what I found:

These were specified in their respective signatures as "type", but
other code required them to be eqtypes:
- Position.T
- Library.stamp

These were specified abstractly using "type", but other code required
the full representation to be visible:
- Symbol.symbol
- Library.serial
- Library.Object.T
- Syntax.mode
- Rule_Cases.cases
- Rule_Cases.cases_tactic
- Local_Theory.operations
- Overloading.improvable_syntax
- Outer_Syntax.isar
- PgipTypes.pgipurl
- Codegen.node
- Codegen.codegr
- 'a Codegen.codegen

And this is only the beginning. There is a lot more code in src/Tools
and src/HOL/Tools that I didn't switch over to opaque ascription.
Also, the problems with type representations "leaking out" don't
become apparent until you compile code that uses them. Compiling the
rest of the distribution might reveal more types from src/Pure to add
to the above list.

If Isabelle coding style is going to dictate the use of transparent
ascription, then I think we could really benefit from a new warning
message: Whenever Isabelle loads ML code where the representation of a
supposedly-abstract type "leaks out", a warning should display a list
of alternatives:

1. If the type is supposed to be abstract, use a single-constructor
datatype instead of a type synonym.
2. If the type is really not meant to be abstract, the full type
definition should be put in the signature.
3. If the type is not meant to be abstract, but the signature will be
instantiated multiple times with different types, then add the type
representation to each signature ascription with a "where" clause.

Anyway, automatic warning or not, someone should really examine all
the types in the list above and decide which of these three options
should be taken in each case.

- Brian