Re: [CoFI] Comments on CASL v0.99 DRAFT

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

This is again on the topic of empty carriers, in response to comments
on my previous message by Peter and the response by Egidio.  I will
try to keep this short, but if Peter adds as many comments as he did
to my last message then I will surely fail. :-)

[OK, only one comment this time... (apart from this one :-)  --PDM]

The bottom line: CASL is already dangerously complicated, and this
adds more complication in exchange for a tiny benefit.

Here is an almost-direct quote from Luca Cardelli during ETAPS a
couple of weeks ago:
    In order to add a feature to a language, it isn't enough that
    it is a pretty good idea.  It has to be a really FANTASTIC idea.
    And then you have to remove something else.

Peter> [... Horst's example with empty carriers is a natural one;
Peter> it appears in the CafeOBJ Report; if we want to translate
Peter> this CafeOBJ example to CASL then we need empty carriers ...]

I agree, and there are other examples like this.  I don't agree that
the need to deal with these examples justifies the extra complication.

Peter> Taking into account also the referees' views on this point, it
Peter> seems to me a bit difficult to motivate "ruling out" the Graphs
Peter> example.

Easy: allowing empty sorts adds more complexity to the language than
is justified by the need to deal with examples like this.

Egidio> I can see an analogue of Till's solution in the distinction we
Egidio> have between total and (possibily ) partial functions; so it
Egidio> looks a reasonable trick that we have already adopted.

I agree.  I just think that the number many people out there can't do
without partial functions is greater than the number who can't do
without empty carriers, and there is a power/complexity tradeoff.

I think I remember Peter arguing at some point in the past that we
couldn't use lambda notation because there might be people in the
intended audience to whom it would be unfamiliar.  This audience needs
empty carriers? 
 
[Lambda notation has crept in anyway, in connection with arch specs.
 But right: my personal view is that it'd be nice if CASL specs could
 be understood by programmers who have never even heard of lambda
 notation.  And since you ask: I personally think that this same
 audience may indeed need specs of graphs, and that they may feel a bit
 disappointed with CASL if discrete graphs can't be specified.  --PDM]

Regards, Don