[CoFI] Comments on CASL v0.98

[bkb@informatik.uni-bremen.de]

[The following is taken from a fax Bernd sent to me yesterday.  --PDM]

CASL: The major thing I am still unhappy with is the fact that
selectors are now always partial [in datatype declarations --PDM].
This defeats the whole purpose of encouraging the user to have total
functions (in the presence of subsorts).  Remember that the compromise
after my original proposal was that total functions can be obtained
if(f) a separate subsort is introduced for each selector [rather:
alternative construct? --PDM]; this is exactly what one wants and
needs.  Otherwise one has to introduce selectors always as separate
functions, a nuisance.

[The problem there is that in an extension, further alternative
constructs for a (sub)sort may be provided, undermining the totality
of the selectors.  E.g., enrich sorts Pair>pair(left,right:Elem) by 
sorts Pair>nil; we expect left and right to be undefined on nil. 
Or perhaps you are proposing to prohibit such extensions?  --PDM]

Concrete syntax issues: I only noticed some discrepancies now:

 - 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).
   [Unfortunately, the preference for Verbose was indeed postfix... --PDM]

 - I thought we had tried to let asserts/axioms be optional; now it is
   very heavy.  Please recall my "bullet" proposal.
   [The problem with "asserts" being optional was context-free ambiguity 
    in, e.g.,
      sorts s=a|b; t=c(d)
    where t=c(d) might be taken either for an axiom or for a datatype
    declaration.  But you're welcome to suggest concise input and
    display for introducing one or more axioms, leaving the "asserts"
    keyword to the verbose style.  How about "(*)", displaying as
    $\bullet$?   Then you may write sorts s=a|b; (*) t=c(d)  --PDM]

best regards
Bernd