CVS difference for ai05s/ai05-0153-3.txt
--- ai05s/ai05-0153-3.txt 2011/03/05 07:19:00 1.11
+++ ai05s/ai05-0153-3.txt 2011/03/10 04:49:49 1.12
@@ -2086,3 +2086,619 @@
****************************************************************
+From: John Barnes
+Sent: Wednesday, February 16, 2011 4:07 AM
+
+I am sorry not to be with you again at the meeting in sunny Florida.
+Although improving, I am still very reluctant to fly. I am especially annoyed at
+missing the opportunity to see the new Dali museum.
+
+In my absence, Jeff Cousins is taking my place. I am sure I will see you all in
+Edinburgh. Meanwhile, please read the following:
+
+As you will have perceived from reading the latest draft of the Rationale
+I am unhappy with two areas of Ada 2012. One is some aspects of
+aspects (groan); the other is subtype predicates..
+
+[For the aspect part of the discussion, see AI05-0229-1.]
+
+Subtype predicates
+
+I am very surprised at where we currently stand on subtype predicates.
+Namely Static_Predicate which can be used in contexts such as loops, and
+Dynamic_Predicate which is more general and cannot.
+
+I understand that the reason given for the fact that a seemingly static
+predicate such as in
+
+subtype Even is My_Integer
+ with Static_Predicate => Even mod 2 = 0;
+
+is actually not allowed is that an implementation might want to compute and
+hold all the allowed values of such a subtype as a sort of set.
+
+The consequences seem foolish. I would expect to be allowed to write
+
+ for E in Even loop ...
+
+especially if My_Integer was not an overwhelming range.
+
+The problem seems to me to be twofold.
+
+First there is the fundamental problem that Ada does not support Sets.
+Neither finite sets nor (thankfully?) infinite sets. I recall that many
+years ago (long before Ada 83) there was a proposal for unordered
+enumeration types which might have formed the foundation for sets. These
+were abandoned.
+
+Note that there is an inkling of this in Ada already since Integer'Base is
+considered to be unconstrained - and thus almost represents an infinite set.
+
+In the example to hand it would be appropriate if an implementation recorded
+ an infinite set as a rule and a finite set as a collection of values. If
+the predicate Even is applied to a finite set then clearly a loop could be
+compiled as an iteration over the elements of the set. However, if the
+predicate Even is applied to an effectively infinite set such as Integer
+then the loop can be compiled with a test as if written
+
+for X in Integer loop
+ if X mod 2 = 0 then
+ ...-- body of loop
+ end if;
+end loop;
+
+
+
+It would perhaps be excellent if Ada did support sets as a real feature.
+It might well improve Ada's perception as a good foundation vehicle for
+teaching about discrete mathematics in CS degree classes.
+
+However, to put sets into Ada is clearly not a task for this revision. We
+need a proper direction to do so and this perhaps could be an objective for
+Ada 2020.
+
+Second, there is the problem (for me anyway) that I think of Integer as
+really an infinite set. (I see I am repeating myself.) It is an unfortunate
+fact that for implementation reasons we have to put limits on Integer.
+Taking this infinite view one might want to forbid
+
+ for I in Integer loop
+
+but clearly it is too late for that.
+
+In the absence of sets, I believe we should abandon the subdivision of
+subtype predicates into dynamic and static forms. They introduce a whole lot
+of new rules for the restricted form of expression allowed in a
+Static_Predicate which make the language gross and is liable to confuse
+users. In any event the choice of names is misleading.
+
+We should revert to the one predicate, Subtype_Predicate and perhaps
+restrict its use so that it cannot be applied to the (effectively)
+unconstrained types such as Integer, Long_Integer and so on.
+
+****************************************************************
+
+From: Robert Dewar
+Sent: Wednesday, February 16, 2011 7:11 AM
+
+> I am very surprised at where we currently stand on subtype predicates.
+>
+> Namely Static_Predicate which can be used in contexts such as loops,
+> and Dynamic_Predicate which is more general and cannot.
+>
+> I understand that the reason given for the fact that a seemingly
+> static predicate such as in
+
+I don't think you have the reason right. This is not hard to implement at all,
+in fact GNAT for a while had a full implementation. The trouble is that it
+potentially involves huge inefficiencies which are hidden, consider
+
+ type R is new Integer with
+ R in N .. M;
+
+where N is 1 and M is 2
+
+The obvious implementation is to iterate through all integers doing the test,
+yes, in practice you may be able to do better in some simple cases like this,
+but in general you cannot, and I think it not in the spirit to have hidden
+inefficiencies like this. Let the programmer write
+
+ for J in R'Base loop
+ if J in R then
+ ...
+ end if;
+ end loop;
+
+so that the inefficiency is obvious, and furthermore, the programmer might
+prefer to write
+
+ for J in R'Base range N .. M loop
+
+to eliminate the inefficiency in this particular case
+
+> is actually not allowed is that an implementation might want to
+> compute and hold all the allowed values of such a subtype as a sort of set.
+
+Nope, no implementation would even think of such a silly implementation
+
+> for E in Even loop ...
+>
+>
+>
+> especially if My_Integer was not an overwhelming range.
+
+Well there you go! Surely you don't think legality should depend on what is or
+is not an overwhelming range.
+
+> First there is the fundamental problem that Ada does not support Sets.
+
+No, this has nothing to do with the problem at all
+
+> Neither finite sets nor (thankfully?) infinite sets. I recall that
+> many years ago (long before Ada 83) there was a proposal for unordered
+> enumeration types which might have formed the foundation for sets.
+> These were abandoned.
+
+And now of course we DO have the equivalent of unordered enumeration types, in
+that we can have noncontiguous subtypes. Note that GNAT also has pragma
+Unordered(enum-type) (I suppose we should make that an aspect as well ...) which
+warns on inappropriate operations like comparison.
+
+****************************************************************
+
+From: Robert Dewar
+Sent: Wednesday, February 16, 2011 7:28 AM
+
+> In the absence of sets, I believe we should abandon the subdivision of
+>
+> subtype predicates into dynamic and static forms. They introduce a
+> whole lot
+>
+> of new rules for the restricted form of expression allowed in a
+>
+> Static_Predicate which make the language gross and is liable to
+> confuse
+>
+> users. In any event the choice of names is misleading.
+
+First of all, as per my previous message, sets have nothing to do with this.
+
+This is an endlessly discussed issue and there is nothing new here (check the
+dciscussion threads in gory detail if you want to revisit that discussion).
+
+I think at this stage that we all agree that we should not allow loops through
+the dynamic case because of the implicit inefficiency which we never like to see
+in Ada. I understand you disagree, but I don't think you bring any new argument
+which would change peoples minds.
+
+> We should revert to the one predicate, Subtype_Predicate and perhaps
+> restrict its use so that it cannot be applied to the (effectively)
+> unconstrained types such as Integer, Long_Integer and so on.
+
+First, I think it would be really unfortunate not to allow
+
+ type Non_Zero_Integer is new Integer with
+ R /= 0;
+
+You don't present any convincing argument for taking away this useful
+functionality.
+
+Second, given we don't want to allow loops in the dynamic case, the strong
+argument against having only one predicate is that it is annoying for legality
+to be affected by a small change from static to dynamic (e.g. from 1 .. 10 to M
+.. N).
+
+You definitely have some people who agree with you on this (inccluding Bob Duff
+and Robert Dewar, and indeed GNAT has this single aspect called simply Predicate
+as well as the official ones, and only has a pragma Predicate, we did not do the
+pragmas for the two official aspects).
+
+But one extra vote here is not going to change the agreed on result in the
+absence of new arguments, and you don't present anything here that has not been
+presented before.
+
+You definitely need to understand the ratoinale behind the choice of two
+separate aspects to write the rationale!
+
+Summary
+
+1. We don't want to allow loops for dynamic predicates, because in the general
+ case that could result in implicit hidden inefficiency which in some case
+ could be disastrous (the Integer example I gave earlier).
+
+[you would like to allow them, and ban integer, but neither is going to happen,
+so these tastes do not affect the rationale for Ada 2012]
+
+2. Given that static and dynamic predicates behave very differently, we
+ deliberately want to distibnguish them,
+
+if we write
+
+ subtype R is Integer with
+ Static_Predicate => R in 1 .. 10 or R in 20 .. 30;
+
+then we can have a loop
+
+ for J in R loop ...
+
+and that will be implemented efficiently
+
+Now suppose we want to change 30 to a dynamic value M
+
+ subtype R is Integer with
+ Static_Predicate => R in 1 .. 10 or R in 20 .. M;
+
+That will be illegal since the condition is not static, so we get an indication
+of a significant change at the point of declaration.
+
+If we had only the single aspect Predicate, we could make the above change and
+get no indication of a problem at the site of the declaration, but some client
+could now become illegal. This is considered (by some who feel very strongly
+about it) to be a significant maintenance issue, which is why we have two
+aspects.
+
+Yes, if we allowed the loop, this problem would not surface as an illegality,
+but actually things would be even worse, when we change 30 to M, both the
+package and the client remain legal, but suddenly we have a drastic inefficiency
+in the client.
+
+I do think this argument is pretty strong. For me I still slightly prefer to
+have a single predicate, but I don't feel strongly, and the opposition
+definitely feels strongly (strongly enough to want to throw out predicates
+completely if this were done).
+
+In practice the most useful use of predicates is for constrainining variant
+types, and making non-contiguous enumeration types (be sure the rationale has
+these two examples!) and those important uses are not affected by this
+discussion.
+
+P.S. interestingly, we could allow loops through dynamic predicates in GNAT for
+the Predicate aspect, since that one is ours .. interesting thought! We have all
+the code in some old revision, so it's tempting to do that.
+
+And if you are worrying about portability, fear not, the pragma Profile
+(No_Implementation_Features) will banish this evil GNAT extension from your
+programs :-) :-)
+
+****************************************************************
+
+From: Robert Dewar
+Sent: Wednesday, February 16, 2011 7:32 AM
+
+By the way on modern 64-bit machines
+
+ for J in Integer loop
+ A(J) := ' ';
+ end loop;
+
+is perfectly fine, the array fits fine in memory (it's only
+4 gigabytes long, even my notebook has 8 gigs of memory), and it executes pretty
+quickly on a fast machine (probably something like a second or two on a
+moderately fast single core).
+
+Machines move on!
+
+****************************************************************
+
+From: Bob Duff
+Sent: Wednesday, February 16, 2011 9:16 AM
+
+> Subtype predicates
+>
+> I am very surprised at where we currently stand on subtype predicates.
+> Namely Static_Predicate which can be used in contexts such as loops,
+> and Dynamic_Predicate which is more general and cannot.
+>
+> I understand that the reason given for the fact that a seemingly
+> static predicate such as in
+>
+> subtype Even is My_Integer
+> with Static_Predicate => Even mod 2 = 0;
+>
+> is actually not allowed is that an implementation might want to
+> compute and hold all the allowed values of such a subtype as a sort of set.
+
+The implementation MUST compute such a set, in order to check the full-coverage
+rules for case statements, etc. I expect the internal representation of these
+sets in the compiler will be as a sorted sequence of ranges. That's not the
+only possibility, but it seems reasonable. And representing Even in this way is
+infeasible, so it's illegal (no great loss -- you just have to make the above
+predicate Dynamic_).
+
+Loops are not the main issue. I originally proposed NOT to allow 'for' loops. They're merely a "nice to have".
+Case statements/expressions are the important feature. But folks said 'for'
+loops are easy enough to implement, so what the heck, let's throw them into the
+pot. Fine with me.
+
+> The consequences seem foolish. I would expect to be allowed to write
+>
+> for E in Even loop ...
+>
+> especially if My_Integer was not an overwhelming range.
+
+As Robert said, this could lead to hidden inefficiencies.
+I know how to loop through "Even" efficiently, but I don't know of any general
+way that would be efficient for arbitrary predicates.
+
+Besides, we want the rules for case statements and loops to be the same -- it's
+bad enough to have two kinds of predicates, three kinds would be worse.
+
+> Note that there is an inkling of this in Ada already since
+> Integer'Base is considered to be unconstrained - and thus almost represents an
+> infinite set.
+
+Almost infinite? Hmm. There are a lot more integers NOT in Integer'Base than
+are in it!
+
+It's really annoying to me that Ada doesn't support arbitrary-range integers
+(except at compile time). We've been struggling with that here at AdaCore
+lately regarding proof tools. For example, the precondition of Integer "+" is
+conceptually (in part):
+
+ Left + Right <= Integer'Last -- no overflow
+ ^
+ |
+ except that "+" is wrong, because it CAN overflow
+
+And calling this meager subset of the integers "Integer" adds insult to injury.
+
+> for X in Integer loop
+> if X mod 2 = 0 then
+> ...-- body of loop
+> end if;
+> end loop;
+
+What if it were "Pre => Page_Aligned mod 2**12 = 0"?
+
+> In the absence of sets, I believe we should abandon the subdivision of
+> subtype predicates into dynamic and static forms.
+
+That was my position. A lot of folks are (inexplicably) uncomfortable with
+that.
+
+>...They introduce a whole lot
+> of new rules for the restricted form of expression allowed in a
+>Static_Predicate which make the language gross and is liable to confuse
+>users.
+
+Well, we still need the same rules. If we recombined the two kinds of predicate
+into one aspect, then we would still have the definition, "a predicate is
+predicate-static if...", and we would still disallow non-predicate-static
+predicates in case statements etc.
+
+>...In any event the choice of names is misleading.
+
+I don't see why. They're annoyingly long, but why "misleading"?
+
+> We should revert to the one predicate, Subtype_Predicate and perhaps
+
+"Subtype_" is just noise, IMHO. I'd call it "Predicate".
+
+> restrict its use so that it cannot be applied to the (effectively)
+> unconstrained types such as Integer, Long_Integer and so on.
+
+I wouldn't want such arbitrary restrictions. What about "type T is range
+0..2**24". Is that "effectively infinite"? Where do you draw the line?
+Besides, many predicates on Long_Integer CAN be static, and implemented
+efficiently. It's the "mod" that causes trouble, not the large number of values.
+
+****************************************************************
+
+From: Robert Dewar
+Sent: Wednesday, February 16, 2011 9:37 AM
+
+> The implementation MUST compute such a set, in order to check the
+> full-coverage rules for case statements, etc. I expect the internal
+> representation of these sets in the compiler will be as a sorted
+> sequence of ranges. That's not the only possibility, but it seems
+> reasonable. And representing Even in this way is infeasible, so it's
+> illegal (no great loss -- you just have to make the above predicate
+> Dynamic_).
+
+That's just not true, you don't need to compute a set for the dynamic case, you just loop through the base range and test the predicate for each value. That's the only general possible approach. It's quite easy, well defined, but can be inefficient.
+
+> That was my position. A lot of folks are (inexplicably) uncomfortable
+> with that.
+
+I find it odd that Bob finds in inexplicable, I find the explanations given by
+these "lots of folks" quite reasonable and quite understandable, they don't
+balance out my preference for having a single predicate, but I am not set on
+this strongly, especially since the implementation can provide it anyway.
+
+> Well, we still need the same rules. If we recombined the two kinds of
+> predicate into one aspect, then we would still have the definition, "a
+> predicate is predicate-static if...", and we would still disallow
+> non-predicate-static predicates in case statements etc.
+
+Right, obviously we can't have full dynamic predicates in case statements, well
+i guess we could with an others, but that's just silly.
+
+> I wouldn't want such arbitrary restrictions. What about "type T is
+> range 0..2**24". Is that "effectively infinite"?
+> Where do you draw the line? Besides, many predicates on Long_Integer
+> CAN be static, and implemented efficiently.
+> It's the "mod" that causes trouble, not the large number of values.
+
+Actually the mod causes no trouble if the predicate is just being used for
+membership and run time checking.
+
+****************************************************************
+
+From: Tucker Taft
+Sent: Wednesday, February 16, 2011 9:56 AM
+
+> That's just not true, you don't need to compute a set for the dynamic
+> case, you just loop through the base range and test the predicate for
+> each value. That's the only general possible approach. It's quite
+> easy, well defined, but can be inefficient.
+
+I think you are agreeing with Bob. Bob was explaining why "mod" is not allowed
+in Static_Predicates, because of the full coverage requirement for case
+statements, which implies being able to enumerate the set efficiently.
+
+...
+>> It's the "mod" that causes trouble, not the large number
+>> of values.
+>
+> Actually the mod causes no trouble if the predicate is just being used
+> for membership and run time checking.
+
+Again, I think you are agreeing with Bob. The "mod" is not a problem for
+membership, it is a problem for full coverage checks, which makes it a no-no for
+Static_Predicates.
+
+****************************************************************
+
+From: Robert Dewar
+Sent: Wednesday, February 16, 2011 10:38 AM
+
+> Again, I think you are agreeing with Bob. The "mod" is not a problem
+> for membership, it is a problem for full coverage checks, which makes
+> it a no-no for Static_Predicates.
+
+Yes, of course, that's exactly right and handling that "Right" would be a huge
+pain.
+
+****************************************************************
+
+From: Bob Duff
+Sent: Wednesday, February 16, 2011 11:05 AM
+
+> > The implementation MUST compute such a set, in order to check the
+> > full-coverage rules for case statements, etc. I expect the internal
+> > representation of these sets in the compiler will be as a sorted
+> > sequence of ranges. That's not the only possibility, but it seems
+> > reasonable. And representing Even in this way is infeasible, so
+> > it's illegal (no great loss -- you just have to make the above
+> > predicate Dynamic_).
+>
+> That's just not true, you don't need to compute a set for the dynamic
+> case, you just loop through the base range and test the predicate for
+> each value. That's the only general possible approach. It's quite
+> easy, well defined, but can be inefficient.
+
+I meant that the implementation MUST compute such a set for static predicates. However we define "static predicates", those are the ones allowed in case statements (etc).
+
+I agree that it need not (and cannot) compute the set for dynamic predicates,
+and that it is possible to allow dynamic predicates in 'for' loops. But it's a
+potentially huge hidden inefficiency, which makes it inadvisable. And as I said,
+I prefer not to have a different rule for 'for' loops than for case statements.
+
+> > That was my position. A lot of folks are (inexplicably)
+> > uncomfortable with that.
+>
+> I find it odd that Bob finds in inexplicable, I find the explanations
+> given by these "lots of folks" quite reasonable and quite
+> understandable, they don't balance out my preference for having a
+> single predicate, but I am not set on this strongly, especially since
+> the implementation can provide it anyway.
+
+I am going to refrain from answering this question, because I don't see any
+value in continuing the argument about a (most likely) settled issue.
+
+****************************************************************
+
+From: John Barnes
+Sent: Friday, February 18, 2011 7:41 AM
+
+The various messages gave me further insight into why we have come to what we
+have. It really is quite complex and will give me lots of food for a detailed
+section of the rat. I find it quite amazing how easy it is to get out of touch
+by missing just one meeting. But my concern remains that we don't mess up any
+possible broader feature in the future, it's just an unease and I cannot really
+put my finger on anything too specific. But remember how the original rules
+about null and access parameters were a pain when null was added more generally.
+
+However the names Static_Predicate and Dynamic_Predicate still seem not ideal.
+That's because the static are somewhat different to our usual use of static. But
+I must confess I cannot think of much better names. And its a pity to lose
+subtype in the name because that distinguished them from type invariants rather
+neatly.
+
+Maybe general and special could be a starting point. Or general and restricted.
+Hmm.
+
+****************************************************************
+
+From: Robert Dewar
+Sent: Friday, February 18, 2011 7:54 AM
+
+I don't like Subtype in the name. Like Specification, Subtype is a term which
+has a different meaning to Ada progammers and RM language lawyers
+
+ type R is new Integer;
+
+to ada programmers, R is a type, not a subtype, to RM LL's it is a subtype. I
+HATE this, but we are stuck with it. In GNAT error messages we never use subtype
+to mean type as well. If you used it in the name of the predicate, lots of Ada
+programmers would assume this means that you can't use it, e.g. in
+
+ type R is new Integer with
+ Static_Subtype_Predicate => R /= 0;
+
+since R is not a subtype. Because subtype predicates can perfectly well apply to
+all types, I don't see why this distinguishes them from Invariants anyway.
+
+> Maybe general and special could be a starting point. Or general and
+> restricted. Hmm.
+
+Static really is better, since this echoes the restriction of case statements to
+static expressions. Yes, we don't allow all static expressions because of
+implementation difficulties, though we could if we really wanted to (at some
+expense!)
+
+****************************************************************
+
+From: Bob Duff
+Sent: Friday, February 18, 2011 7:02 PM
+
+> I don't like Subtype in the name. Like Specification, Subtype is a
+> term which has a different meaning to Ada progammers and RM language
+> lawyers
+>
+> type R is new Integer;
+>
+> to ada programmers, R is a type, not a subtype, to RM LL's it is a
+> subtype. I HATE this, but we are stuck with it. In GNAT error messages
+> we never use subtype to mean type as well. If you used it in the name
+> of the predicate, lots of Ada programmers would assume this means that
+> you can't use it, e.g. in
+>
+> type R is new Integer with
+> Static_Subtype_Predicate => R /= 0;
+>
+> since R is not a subtype. Because subtype predicates can perfectly
+> well apply to all types, I don't see why this distinguishes them from
+> Invariants anyway.
+
+I agree 100% with Robert's comments above. Even I think of R as a type, except
+when I've got my language-lawyer hat on.
+
+> > Maybe general and special could be a starting point. Or general and
+> > restricted. Hmm.
+>
+> Static really is better, since this echoes the restriction of case
+> statements to static expressions. Yes, we don't allow all static
+> expressions because of implementation difficulties, though we could if
+> we really wanted to (at some expense!)
+
+Right, except it's not just that we're more restrictive with "predicate-static"
+than "static". The main point is that we want the name of the current instance
+in there, even though it is not static -- it will be (conceptually) static once
+we have a value for it. When we say:
+
+ subtype S is Integer with
+ Static_Predicate => (S /= 0 and S < 100 and S > -100) or S = Integer'Last;
+
+the expression after "=>" is certainly not static, since S is not a static
+expression, but we allow it because if you plug in a static value for S, then
+that expression is static. And we can construct a statically-known set,
+represented as a sequence of ranges:
+
+ {-99..-1, 1..99, Integer'Last..Integer'Last}
+
+One key point to put in the Rat is that the number of ranges in this set is
+roughly proportional to the size of the program text.
+
+****************************************************************
+
Questions? Ask the ACAA Technical Agent