[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: concrete syntax
Dear Peter,
this is meant to be material for discussion; please feel free to advance to
CofiLang. [the comments about "Definedness", "Verbose and Concise Style"
are repeated from an earlier message to have everything together here].
Hope to see you soon
Bernd
Again, I apologize for not having reacted earlier due to a lot of problems here.
[Those of us attending ASF+SDF'97 in Amsterdam may be unable to react
to these late proposals before the meeting. I suggest that we regard
the following as advance warning of the lively discussion that we may
expect concerning the final adjustment of the CASL design, and of the
consideration of issues of concrete syntax.
So many of us have been suffering severely from lack of time during
the past month that it has delayed progress towards a decision
concerning concrete syntax (at least for basic specs) in Amsterdam.
My suggestion is that we are to take NO DECISIONS at all concerning
concrete syntax here, but use the time for making sure we are aware of
all the issues and possibilities. Afterwards I'll revise the
compromise proposal regarding concrete syntax and we'll take a new
round of cofi-language comments and discussion. The design of the
CASL concrete syntax is far too important for decisions to be rushed -
although I would prefer that contributions to the discussion would
appear more quickly, and the lack of concrete syntax for CASL is
indeed frustrating. --PDM]
Definedness
-----------
Definedness should be either pre or postfix, but not one in Verbose
and the other in Concise (my preference is prefix; for reasons of
extensions to HO explained elsewhere I would prefer not to have
any built-in/predefined postfix operators).
Verbose and Concise Style; a Single Version??
---------------------------------------------
[The comments in []s below are Bernd's, not mine, except where
finishing thus: --PDM]
following Dons comment that the compromise might be confusing, and in
view of Frederics comment that even he does not like "and, implies"
etc., it is perhaps worth putting another proposal on the table:
- distinguish only "Email" (i.e. input and verbose format)
and "Display" (i.e. more concise) formats
- either are allowed in publications (Email in Courier, teletype-like
font; Display in proportional Times, Helvetica or the like)
- Email is "Input", except for
DATATYPE-DECL "=" (not "generated")
"ops, gen, vars" allowed [or only these??!!]
[possibly: Assoc, Comm, Idem, Unit; plus AC, ACI, ACU]
"pred" (not "predicate")
the logical operators in concise input format, including "~" (sorry)
[possibly: reverse arrow "<=" instead of "if"]
"defined" as prefix operator
- Display is "Concise Display", except for
[possibly: Assoc, Comm, Idem, Unit; plus AC, ACI, ACU]
[possibly: reverse arrow "<=" instead of "if"]
[This seems to be still two formats? Personally, I'd prefer to have a
single canonical format, but with a possibility for users to configure
it to their personal taste regarding (at least) input. There could be
an approved configuration file (preferably a CASL specification
containing only annotations) for e.g. concise input and display. As
display annotations are already to be provided for customizing display
of user-declared symbols, the same mechanism could be used for
configuring the alternative input/display style. (I'd already
discussed this with the Paris side of the concrete syntax effort, but
ran out of time for formulating a message on it before leaving...)
--PDM]
Keywords
--------
In the "Single Version" compromise outlined above I could live with
slightly verbose input such as "forall, exist, defined, pred" instead of
"\A, \E, \D, \P", also "as" instead of "!", since then there is only ONE
version and no confusion arises (I would prefer this). However, the other
versions could coexist as abbreviations.
With respect to keywords "operators, variables, predicate, generated,
associative, commutative, idempotent" shorter versions should be allowed
(a) for shorter writing
(b) to avoid errors due to misspellings
(c) for more concise reading
The last case can of course be achieved by configurable formatters.
In any case, I would allow mixing in input.
I would prefer just one version for all these [obviously the short ones, if
we could only agree :-]. I am not so fond of allowing the singular forms as
well.
Axioms; omission of ";" etc.
----------------------------
I definitely prefer "axioms" over "asserts". A previous version of the
syntax proposal allowed to omit this keyword; not any more. I regret that
this is rather heavy now for those who prefer to group axioms directly with
a function declaration (rather than having all declarations first and then
all axioms).
If an axioms starts with a (universal) quantification, no keyword is needed.
If it is just a formula, my previous proposal was to start it just with the
bullet to indicate implicit universal quantification over the declared
variables. In this case, no keyword is needed either. Example:
ops Empty: List ;
IsEmpty: pred(List) ;
. IsEmpty(Empty)
[As I noted in my comments added to your fax message yesterday, this
simply means using `.' as a concise input and display alternative for
"axioms" or "asserts". --PDM]
Another solution is to use fomatting rules (as in Haskell etc.) that allow
the omission of separators (such as ";") by making proper indenting
relevant. I have experience in this (also in teaching) and like it a lot.
Roughly, indenting in the same position means sequencing with a new item of
the same kind, whereas indenting one more step (e.g. another blank) means
continuation of the previous item. This can be used to omit ";" in
BasicItems or "/\" in a big formula under a common quantifier.
Here, it could be used to distinguish declarations from axioms, e.g.
ops Empty: List
IsEmpty: pred(List)
IsEmpty(Empty)
Function Attributes
-------------------
I consider the Function Attributes to be a special case. As the AC and ACU
case are likely to occur quite often, my personal preference would be to
allow (only)
Assoc, Comm, Idem, Unit, AC, ACU, possibly also ACI, ACIU
then one would not even need a list of attributes.
[Note: the abbreviations A, C, I, U would then go away; this would be good
since they should not be reserved words (they should be usable as variable
names), and a special case may severely complicate lexical and syntactic
analysis]
As to the position of the Function Attributes: my personal preference would
still be to associate them with the function arrow since this allows
generalization to HO, e.g.
__+__: Int*Int ->[ACU Zero] Int
in a notation analogous to compound ids or parametrized types.
A colon would be confusing and error-prone.
[Please refer us to an existing specification language where such
attributes are incorporated in function types! Personally, I don't
recall any... --PDM]
Function Definitions
--------------------
I am unhappy about the syntax for function definitions because
(a) I would expect that ":" means "declared of type" in declarations,
whereas here it means "declared to have result type"
[as in MANY programming languages! --PDM]
(b) the syntax does not generalize well to Higher Order (strongest reason).
Example: a curried function, trying to generalize the notation
cf1 (a:T) -> (b:T) : T = a++b
Example: a curried function, as constant
cf1 : T->T->T = __++__
Example: a HO function, trying to generalize the notation
hof (a:T->T) -> (b:T) : T = a(b)
In all these cases there is a confusion between the two meanings of ":"
(see (a)).
(c) we will need a general construct for named parameters for dependent types
eventually anyway
Example: a function with dependent type, trying to generalize the notation
hog (a:T) -> (b:S(a)) : T = a++b
A better solution (for my taste) would be to reserve the meaning of ":" for
"declared of type" in declarations, and to introduce (eventually) the
possibility for (parameter) names in (product) types. Examples:
cf1 : (a:T) -> (b:T) -> T = a++b
cf1 : T->T->T = __++__
hof : (a:T->T) -> (b:T) -> T = a(b)
hog : (a:T) -> (b:S(a)) -> T = a++b
The syntax is then simply
SORTS SS ::= (VD) [additionally]
FUN-DEFN OD ::= FN:FT=T [substitute]
PRED-DEFN OD ::= PN:PT<=>F [new]
If the possibility for names is not generally desired for FO CASL, then
FUN-DEFN OD ::= FN:(VD)->S=T [substitute]
FUN-DEFN OD ::= FN:(VD)-?->S=T [substitute]
FUN-DEFN OD ::= FN:S=T [as is]
FUN-DEFN OD ::= FN:?S=T [as is]
PRED-DEFN OD ::= PN:\P(VD)<=>F [new]
PRED-DEFN OD ::= PN:\P()<=>F [new]
[As Don has already suggested, one might follow SML and allow both
styles. --PDM]
Predicate Types
---------------
Preferably just "pred" (never mind the predecessor function!).
Verbose Style of Quantifiers and Logical Connectives
----------------------------------------------------
Keep verbose style for quantifiers,
delete verbose style for logical connectives.
The latter is particularly nice since then "and, or, ..." will be
available for use (overloading) as boolean functions (for those who need
them); note: with a different precedence! Example:
/\ A or TT = TT /\ ...
Existential Equations
---------------------
I object to "=e=" [but not the display!!], since
e=e/\e=e=e/\.../\x=e/\x=e=e
even
e = e/\e =e= e/\.../\x = e/\x =e= e
are very confusing. Moreover, we do not otherwise have a mixture of letters
and SIGNS (good!); in this case it would very likely mean that one has to
use whitespace around EVERY "=" or "=e=" sign!!
Precedence in Terms
-------------------
I do care a lot about this; I think it would be terrible to have to use
parentheses everywhere. My previous proposal was to have few (about 5)
predefined precedence levels derived from the usual ones in Mathematics
(e.g. for +, *) [as in almost all programming languages], and to let
operators starting with such characters inherit the precedence, e.g. ++
Any other solution (user-defined precedences) raises the problem of union
of specifications where they may conflict. Although they could be resolved
locally (e.g. by giving one another precedence locally), it is still
confusing to have an operator symbol have one precedence here and another
elsewhere.
[That was precisely the motivation for having the uniform rule in the
current proposal. Kindly provide examples where the parentheses would
be too tedious (e.g., existing examples where you exploit your
suggested solution, with a count of how many parens would need
adding). --PDM]
Mixfix Application; HO Application
----------------------------------
I regret not to have more time now to go into the analysis of mixfix
application, context-free /-sensitive parsing etc.; another time.
Similarly, I want to point out again that user-defined prefix/postfix
notation does not go well with HO parameterless application, e.g.
pre f a b post c
Does post bind to b or (f a b)? Why does f no bind to all (f a b post c) ?
If the present precedence hierarchy is generalized (such that HO
application also binds strongest, as in HO languages), then the example
binds
pre ((f a b) post) c
Is this not a bit strange, to have the (presumably) second parameter of pre
so far away? [no more time for further analysis, sorry]
___________________________________________________________________
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