Re: [CoFI] Concrete syntax for basic specifications

[Don Sannella <dts@dcs.ed.ac.uk>]

I've had a look through the proposal, and have a number of comments.
I've looked through the earlier Bremen and Paris proposals but haven't
read them, so it's an accident if I propose something that has been
mentioned by one of them.

My comments are in the order that things appear in the proposal.


INPUT SYNTAX AND DISPLAY FORMAT

S generated by A | ... | A

    I would prefer S = A | ... | A as in the concise syntax, which
    fits nicely with S > A | ... | A immediately above.  But is there
    a problem of ambiguity with ISO-DECL when there is just one A?

asserts AX; ...

    I would very strongly prefer "axioms" to "asserts".  Asserts is
    from Larch where the keywords are verbs: includes, introduces,
    asserts.  Our keywords are nouns: sorts, operators, predicates.

exists1 (and \exists_1 in concise syntax)

    How about exists! which is standard in mathematics I think?

quantifiers and connectives

    I would be in favour of using the standard symbols in the display
    syntax.  (For implication', use <= ; this is missing in the
    concise syntax by the way.)  If not, it isn't consistent to use
    epsilon for membership in the display syntax.

[The omission of <= as a reserved symbol was deliberate, so as
 to leave it free for use as an ASCII version of LaTeX \leq.  But
 personally, I'd prefer to reserve <= for implication', using e.g. =<
 as input syntax for \leq (and >= for \geq).  --PDM]

predication, application

    In ML, parentheses are for grouping and juxtaposition denotes
    function application.  So one can write f x or f(x), where in the
    latter the parentheses serve only to (superfluously) group x.  One
    writes f(a,b) rather than f a,b because f takes a single argument
    (a pair).  For curried application, one can then write f a b .
    This works fine, is a little less verbose than using f(x) for
    application and predication, and generalizes smoothly to
    higher-order.

[It may not be clear from the proposal, but the intention was that
 declaring the prefix operator f__:X->C would allow one to write f x
 without parentheses, whereas declaring f:X->C would require writing
 f(x).  For a function with two arguments, one could either declare
 f:A*B->C and use f(a,b), or declare f__ __:A*B->C and use f a b.
 Bernd has studied this issue closely, also with respect to relative
 precedence of prefix application and functional application; I hope
 that he will follow up with a more detailed analysis.  --PDM]

PARTICULAR ISSUES FOR DISCUSSION

Concise and verbose forms

    This is okay as a compromise, but it is obviously a compromise.
    Far better would be to pick one of them.  To have both forms will
    just lead to confusion.  The benefit of having both is really not
    so enormous, especially if (as I suggest) the standard notation
    for quantifiers and connectives is used, with = instead of
    "generated by" in datatype decls.

Keywords

    Should singular forms of plural keywords be allowed?  Yes
    Should other abbreviations be allowed, e.g. assoc?  Yes

Function definition

    I suggest (surprise!) the ML solution, where one can attach a type
    to the function symbol, or to the arguments and result, or both.
    This certainly generalizes smoothly to higher order.

Precedence in terms

    I would like this to be as simple as possible.  Please no
    precedence numbers!

Qualified function and predicate symbols

    Use parentheses for all grouping.

Comments and annotations

    In display format, put comments in italics.  I don't care about
    the input syntax as long as it is something standard instead of a
    new invention, e.g. % at the beginning of the line as in Latex or
    (* ... *) as in ML.

Regards, Don