[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: Revised study note on generic specifications [MB-2] installed
Dear Michel,
I think your new version of the note is much improved; allow me to make
some more comments though.
o explicit parameter namse for Distinguishing Parameter Specifications
o possible extension: dot notation instead of compound names
o a simpler solution for Fixed parts
[These proposals are too late for incorporation in v0.94, but it's
useful to have them here in writing before the Edinburgh meetings.
Let's hope for reactions now from those who cannot join us there...
Unfortunately, Michel himself has no time for answering the questions
below before Edinburgh (neither do I). --PDM]
Distinguishing Parameter Specifications
---------------------------------------
It took me a long time to understand the significance of the keyword "par"
in your notation. The problem is, I think, that your approach is
incompatible with the intuition I (at least) have about parametrization
(e.g. lambda calculus).
The first problem is, that defining and applied occurrence appear to be
alike (par is used everywhere; why, one thinks) until you explain some more
in 2.2.
I guess you want to distinguish, in an instantiation (inside a parametrized
specification) with the actual ELEM, say, between the use of the globally
defined spec ELEM and the formal parameter ELEM.
The usual solution for this is that there is a name for the formal
parameter such that it becomes a bound variable in the body. Sorry, you do
not want this, but why not? This is the intuition.
Let us just assume, for the discussion, that there are *optional* names for
formal parameters. Then there basic use would be as actual parameters for
other specs in the body, e.g. (close to your notation):
spec SP (X: ELEM) =
enrich F(X) by
...
end spec
Of course, X is a name for a *specification*. Thus F(X) (using the formal
parameter) and F(ELEM) (using the global spec) are different. Note that in
this sense your example MISMATCH-TWO is *not* wrong, this may be intended;
you just want to rule it out, I guess, because it runs against the bound
variable intuition.
Anyway, I am not arguing for dot notation here! All items in the signature
of ELEM can be used in the body, e.g. Elem. Note that also
spec SP2 (X: ELEM) =
enrich G(X,X) by
...
end spec
now becomes possible, where X denotes *the same* actual specification (see
the recent emails by me and Till).
One interesting question is whether we could not introduce this in an
extension (if there is strong reaction against it for CL), i.e. how much
can not be expressed (if, in your notation, the formal parameter "par
ELEM-WITH-ORDER" can *not* be used as an actual "par ELEM-WITH-ORDER" in
the body)? can we live with it (note that there will be such an extension)?
Another question (raised by Peter, hopefully quoted correctly) is: if we
introduce names for formal parameters, does it make sense (and simplify
matters) to only allow their use as actuals in the body? and (my addition)
add dot notation in the sense below in an extension?
Possible extension: dot notation instead of compound names
----------------------------------------------------------
As an *extension* one might consider to use the formal name with dot
notation to distinguish several otherwise conflicting names (BTW: this also
solves the compound name problem), as in Ada. However, your renaming ELEM1
and ELEM2 also works, if (I think) awkwardly; certainly not with less
writing.
In Ada, names are visible directly, from any package that is in scope. A
name can always (in particular when a name conflict occurs) be "qualified"
by prefixing it (using dot notation) with the name of the enclosing package
where it is declared (and so on recursively); analogously for (nested)
blocks. Thus (apart from overloading, where a type qualification is used as
we do) a name (applied occurrence) can always be made unique by full
qualification (this is quite nice for tools), but this is *optional*.
[BTW since RAISE also has explicit names for algebras (as parameters), as
Anne told us, they presumably have a similar solution? Anne??]
Thus, if instantiations are given explict names in an instantiation or by
renaming, there is a handle to distinguish *all* items in the signature at
once:
spec NO_PROBLEM =
STACK(INT) renamed STACK_INT
+ STACK(NAT) renamed STACK_NAT
end spec
i.e. instead of compound names Stack[Int], STACK_INT.Stack is used; note
that there is no need to think of this beforehand by defining compound
names, or to define a lot of compound names in the signature.
Most importantly perhaps, this "facility" is only used when needed. Thus we
could e.g. omit compound names entirely, live with however awkward renaming
in the Common Language (as you did in PLUSS) and introduce this in an
extension.
As you know from my previous comments, I consider compound names for sorts
and functions to be a "poor mans" solution for real parametrized,
polymorphic sorts and functions; they are *not* a substitute and would
interact very badly with those in an extension. I also consider it too
heavy for the Common Language to introduce all the complications of induced
subsort relations for compound sorts, as you suggest; either nothing or
full parametrized sorts and functions. With parametrized (but *not*
polymorphic functions) some restricted higher order sneaks into CL!
Fixed parts
-----------
I still find the "par" solution you suggest quite sophisticated for the
average user. Why not (as I previously suggested, but perhaps not
understandably) use the "fixed" idea for a new enrichment operator? e.g.
spec WEIGHTED-ELEM =
import NATURAL in
sort ELEM
...
end spec
where "import" has the semantics of fixed persistent enrichment? then
NATURAL is *always* fixed in every use of WEIGHTED-ELEM, whether parameter
or not; is this not what is intended anyway?
This seems to be a much simpler solution for my taste (if it works).
___________________________________________________________________
Prof. Dr. Bernd Krieg-Brueckner courier mail only:
FB3 Mathematik und Informatik MZH 8071, FB3
Universitaet Bremen Universitaet Bremen
Postfach 330 440 Bibliothekstr. 1
D-28334 Bremen D-28359 Bremen
Telefon: (+49) 421-218-3660 telefax: (+49) 421-218-3054
bkb@Informatik.Uni-Bremen.DE privat: (+49) 421-25-1024
NEW: http://www.informatik.uni-bremen.de/~bkb