[isabelle-dev] Transparent/opaque module signature ascription
makarius at sketis.net
Fri Nov 12 17:09:00 CET 2010
On Fri, 12 Nov 2010, Brian Huffman wrote:
> 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...
I do care about abstraction, and I did a lot of "narrowing" in the
interfaces, but these things need to be done in a way that solves more
real problems than introducing new ones by wild changes. (Maybe you know
the internal joke "SOMEthing went utterly wrong".)
Even if you have very abstract module interfaces (which are hard to figure
out in the first place), there is a more fundamental lack of abstraction
that is not addressed at all, namely how one works with the logic.
This starts with types typ and term, which are very concrete, but term is
modulo aconv most of the time (I wonder how often this is violated in the
code). It continues when you refer to concrete logical constants and
rules when building tools (decision procedures, packages etc.). You are
hooked to a particular concrete representation, and cannot easily
transport the tool to another formulation of the same logical structure.
The local theory infrasturcture with its declarations plus morphisms
addresses this to some extent, but very few tools are "localized" in that
way. At least the main specification packages are already "abstract" by
being based on the Local_Theory interface.
More information about the isabelle-dev