Re: Total and partial functions

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

[The desire to make a last minute change w.r.t. lifting the restriction
on overloading total and partial function with the same profile, while
reasonable, came too late. Below reservations by Don, and some of the
discussion, are reported (BKB)]
> 
-------- earlier message ---------
> Peter wrote:
>  > It seems that there are 3 candidates for an institution catering for
>  > total and partial declarations ops f:w->s; f:w->?s :
>  >
>  > 1. allow the sets TF_{w,s} and PF_{w,s} to have non-empty intersection
>  > 2. always remove elements of TF_{w,s} from PF_{w,s}
>  > 3. use only PF_{w,s} plus definedness assertions
>  >
>  > [...]
>  > I now plan to follow 1. above in the DRAFT of the CASL Summary v1.0.
>  > Perhaps further discussion of the issues here is best left until
>  > the 14 days after that DRAFT appears.
> 
> Dear friends,
> 
> I am very uneasy about this last-minute reversal of one of our most
> fundamental design decisions.  I have spent a fair amount of time on
> the semantics of basic specifications (minus subsorts) and am now
> quite confident that there are no problems there other than the ones
> that I have already reported.  (I write this before looking at v1.00.)
> Between now and the deadline to report problems in v1.00 I will be
> able to spend at most one hour checking to see if this change
> introduces any problems.  If there is some serious problem, I doubt
> that I will find it in that time.  I suspect that there is no problem
> in this fragment of the language but I would not be willing to bet
> that there is none.
> 
> By the way, there is a big difference between partial functions with
> definedness assertions (3 above) and distinguishing between partial
> and total functions (1 above), namely that the latter allows static
> checking and the former does not.  This was the reason for making the
> distinction in the first place, I think.
> 
> Don Sannella
------------ (bits of a) message from Peter ------------
Peter Mosses wrote:
> 
...
> Till wrote:
> 
> Till> Dear Peter,
...
> Till> The point is that if we make a change to the language concerning
> Till> this point, it should also be reflected in the institution (otherwise,
> Till> the semantics of unions would become awkward and
> Till> institution-specific). Since there is no time to change the
> Till> institution in the IFIP book chapter (and I did not manage to persuade
> Till> Maura that this would be just a small change to the institution), I
> Till> think we should entirely stay with what we had in 0.99.
...
> I'm afraid that my current conclusion is indeed that this seemingly
> minor change has, contrary to my expectations, turned out to be too
> controversial to make at this late stage, and that the editing made to
> Section 1.1 in v1.0-DRAFT will presumably have to be reversed in the
> final v1.0.  (To avoid multiple patches of v1.0-DRAFT, I'd better not
> edit the document before 15 October - OK?)
> 
...
> 
> It's a pity that Till didn't notice this issue six months ago, before
> the IFIP chapter was finalized, and before the CASL semantics was
> updated to v0.99 - it might have had a better chance of acceptance,
> and we might have ended up with an even better CASL.  Never mind: he
> has helped so much to sort out so many other problems with our design
> ideas, and it's not his fault that we ourselves didn't question
> closely enough the motivation for the prohibition of total and partial
> function declarations for the same symbol.
...
[Peter]
----------- more recent message ------------
Don Sannella wrote:
> 
> Bernd Krieg-Brueckner writes:
>  > If you decide ist too late (which I hope you dont)
>  > then we should seriously establish a procedure for updates;
>  > remember (Don): this was a feedback from HO extensions.
> 
> Sure, I understand that.
> 
> As I understand what Till has written, the problem isn't that this bit
> of the design makes it any more difficult to do the HO extension, just
> that you happened to notice it while working on that.  I am simply
> worried that this is a change to a pretty basic part of the design, on
> top of which everything else builds; there isn't enough time to check
> that it is okay; and it isn't a necessary change in the sense that
> something else won't work if we don't make the change.
> 
> I think whatever we decide to call CASL v1.0, there will be some
> defect.  So the decision to stop the design process is determined by
> when we decide to stop rather than when we achieve absolute
> perfection.  I'm worried that in this case we are trading a known
> very small defect for something that has a non-zero chance of being a
> huge embarrassing defect.
> 
> Cheers, Don
------------------------
[some of my reply: (BKB)]
I find it easy to accept that it is too late now; that's the way of
life.
However, I do not accept that version 1.0 is the end of all our efforts.
I do insist that we adopt procedures that let us have versions 1.01
etc.,
with resonable intervals etc. It would be silly to let improvements be 
hindered "just" by the fact that more time is needed to evaluate 
consequences etc. I also do not accept the argument that the book
chapter is finished; it is just about to be sent to the printers. 
Even if it was (or is), this is no reason to stop.
Mind you, I am speaking in general, not just for this comparatively 
minor issue. But even here: I would not be afraid of publishing a
version
1.02 eventually, while we finish and adopt version 1.0 NOW.

------------- reply from Don -----------
I think it would be a waste to put non-trivial effort into perfecting
CASL once v1.0 is finished.  There are other things to be done.
Coming up with version 1.01 etc. will lead to confusion in the minds
of users and people working on other things in CoFI will need to track
the changes.  This is a terrible burden -- I have experience with this
in Extended ML.  If the reason for the modification is not extremely
convincing then I would be against doing it for a couple of years.

---------- the end so far -----------