CVS difference for ai05s/ai05-0153-1.txt
--- ai05s/ai05-0153-1.txt 2010/05/04 03:55:06 1.9
+++ ai05s/ai05-0153-1.txt 2010/05/20 06:36:05 1.10
@@ -1,4 +1,4 @@
-!standard 3.2.4(0) 10-04-27 AI05-0153-1/05
+!standard 3.2.4(0) 10-05-19 AI05-0153-1/06
!class Amendment 09-05-27
!status work item 09-05-27
!status received 09-05-27
@@ -50,17 +50,6 @@
values of the subtype to satisfy a certain condition. The values of a
subtype are a subset of the values of its type.
-RM-3.2(8/2) says:
-
- ...The set of values of a subtype consists of the values of its type that
- satisfy its constraint and any exclusion of the null value.
-
-Change it to:
-
- ...The set of values of a subtype consists of the values of its type that
- satisfy its constraint, any exclusion of the null value, and any predicate.
-
-
Add new section 3.2.4:
3.2.4 Subtype Predicates
@@ -88,9 +77,6 @@
- For a base subtype, True.
- [???I don't think we need to say anything about ranges or discrete_ranges,
- here.]
-
[Editor's note: The predicate has no effect on the static or dynamic semantics
of the subtype indication except as noted here. In particular, it has no effect
on the range of scalar subtypes.]
@@ -98,18 +84,21 @@
Dynamic Semantics
-On every subtype conversion, the predicate of the target subtype is evaluated,
-and a check is made that the predicate is True. Redundant[This includes all
-parameter passing, except for certain parameters passed by reference, which are
-covered by the following rule: ] After normal completion and leaving of a
-subprogram, for each in out or out parameter that is passed by reference, the
-predicate of the subtype of the actual is evaluated, and a check is made that
-the predicate is True. For an object created by an object_declaration with no
-explicit initialization expression, or by an uninitialized allocator, if any
-subcomponents have explicit default values, the predicate of the nominal subtype
-is evaluated, and a check is made that the predicate is True.
-Assertions.Assertion_Error is raised if any of these checks fail.
+If the Assertion_Policy in effect is Check, then:
+ On every subtype conversion, the predicate of the target subtype is
+ evaluated, and a check is made that the predicate is True. Redundant[This
+ includes all parameter passing, except for certain parameters passed by
+ reference, which are covered by the following rule: ] After normal completion
+ and leaving of a subprogram, for each in out or out parameter that is passed
+ by reference, the predicate of the subtype of the actual is evaluated, and a
+ check is made that the predicate is True. For an object created by an
+ object_declaration with no explicit initialization expression, or by an
+ uninitialized allocator, if any subcomponents have explicit default values,
+ the predicate of the nominal subtype is evaluated, and a check is made that
+ the predicate is True. Assertions.Assertion_Error is raised if any of these
+ checks fail.
+
AARM Ramification: Predicates are not evaluated at the point of the [sub]type
declaration.
@@ -125,33 +114,35 @@
discrete_subtype_definition is illegal if it statically denotes a subtype with a
user-specified predicate.
-[???Question: The above disallows for loops. Maybe we should allow predicates
-for the discrete_subtype_definition of a loop_parameter_specification. The
-implementation model for:
-
- for X in S loop ...
-would be:
-
- for X in S'Range loop
- if X'Predicate then
- ...
-]
-
Dynamic Semantics
The elaboration of the declaration or body of an instance of a generic unit
-raises Program_Error if it contains an index subtype, discrete_range of an
-index_constraint or slice, or a discrete_subtype_definition with a
-user-specified predicate.
+raises Program_Error if any of the following occurs within that declaration or
+body, but not further nested within a generic unit: an index subtype,
+discrete_range of an index_constraint or slice, or a discrete_subtype_definition
+with a user-specified predicate.
AARM Reason: We don't want to have arrays with holes determined by arbitrary
predicate expressions -- that would be very confusing. The same goes for entry
families. It would be particularly troublesome for slices that are required to
be passed by reference. The run-time check is needed to prevent generic contract
model problems, but we also have a legality rule for cases where we can detect
-the problem at compile time.
+the problem at compile time. Note that the run-time check happens at the
+elaboration of each instance, not just when the offending construct is reached.
+Therefore, the check could fail even if the offending construct cannot be
+reached.
+AARM Reason: The wording forbids "for X in S loop ..." when S has a
+user-specified predicate. Although it might make sense for it to mean:
+
+ for X in S'Range loop
+ if X'Predicate then
+ ...
+
+we decided that would be too confusing.
+
+
Implementation Permissions
A predicate check may be omitted if the subtype with the predicate statically
@@ -175,12 +166,24 @@
Modify 4.5.2(29):
-The tested type is scalar, and the value of the simple_expression belongs
-to the given range, or the range of the named subtype {and
-any predicate of the named subtype evaluates to True}; or
+The tested type is scalar, and the value of the simple_expression belongs to the
+given range, or the range of the named subtype {and any predicate of the named
+subtype evaluates to True}; or
AARM Ramification: If S has a predicate, S'First in S may evaluate to False.
-Similarly for S'Last.
+Similarly for S'Last. We certainly don't want to require the implementation to
+calculate the lowest/highest values that satisfy the predicate. Nor do we want
+to require a check that the bounds satisfy the predicate, because that would
+just complicate the programmer's job. For example, if you want to attach a
+predicate like "is even" to a subtype of Integer, you don't want to have to
+carefully construct a subrange of Integer first.
+
+Modify AARM-4.5.2(29.a):
+
+ Ramification: The scalar membership test only does a range check {and
+ a predicate check}. It does not perform any other check, such as
+ whether a value falls in a "hole" of a "holey" enumeration type. The
+ Pos attribute function can be used for that purpose.
Modify 4.5.2(30/2):
@@ -190,14 +193,15 @@
Add at the end of 4.6(51/2):
-If the target subtype has a predicate, the predicate is applied to the value and
-Assertions.Assertion_Error is raised if the result is False.
+If the target subtype has a predicate, and the Assertion_Policy in effect is
+Check, the predicate is applied to the value and Assertions.Assertion_Error is
+raised if the result is False.
Modify 4.9.1(2/2):
A subtype statically matches another subtype of the same type if they have
-statically matching constraints, {neither has a predicate or both predicates
-come from the same predicate_clause, }and, for access subtypes, either both or
+statically matching constraints, {all predicate_clauses that apply to them come
+from the same declarations, }and, for access subtypes, either both or
neither exclude null. ...
Modify 6.4.1(13/3) (as modifed by AI05-0196-1):
@@ -206,7 +210,14 @@
actual, without checking that the value satisfies any
constraint{, any predicate,} or any exclusion of the null value;
+Modify 13.9.2(3):
+
+ X'Valid Yields True if and only if the object denoted by X is normal[ and]{,}
+ has a valid representation{, and the predicate of the nominal subtype
+ of X evaluates to True}. The value of this attribute is of
+ the predefined type Boolean.
+
!discussion
Predicates are similar to constraints. The differences are:
@@ -233,35 +244,17 @@
---
-The model here is that a predicate has *no* effect on the static or dynamic semantics
-of a constraint. That is, if a predicate is applied to an indefinite type, the
-resulting subtype is indefinite. If a predicate is applied to an unconstrained
-subtype, the resulting subtype is unconstrained. And so on.
+The model here is that a predicate has *no* effect on the static or dynamic
+semantics of a constraint. That is, if a predicate is applied to an indefinite
+type, the resulting subtype is indefinite. If a predicate is applied to an
+unconstrained subtype, the resulting subtype is unconstrained. And so on.
This mirrors the semantics of null exclusions (which also are not constraints).
---
-
-We define predicates to be part of static matching, so that subtypes with different
-predicates are not considered identical.
-
----
-
-???The following para is obsolete, but I'm leaving it in for discussion purposes.
- The exception "Constraint_Error" seems wrong for something that is not a
- constraint. Therefore, failed predicates raise Predicate_Error. This seems
- necessary in order to avoid confusing constraint checks (which generally can
- be assumed to remain True after the first check) with predicate checks (which
- generally cannot be assumed to be remain True).
-
-Bob replies: If we have Predicate_Error, then we should have Precondition_Error
-and Postcondition_Error. But we don't: Those just use Assertion_Error. So I got
-rid of Predicate_Error, and used Assertion_Error.
-
-I'd be just as happy with Constraint_Error. Null exclusions use
-Constraint_Error, even though they aren't constraints. And Constraint_Error is
-used for a whole bunch of other not-quite-constraint things.
+We define predicates to be part of static matching, so that subtypes with
+different predicates are not considered identical.
---
@@ -307,17 +300,42 @@
checks are not required. However, that seems too complicated, since we can't
allow checks anywhere at all -- that would allow the implementation to introduce
arbitrary race conditions into the program!
+
+---
+
+RM-3.2(8/2) says:
+
+ ...The set of values of a subtype consists of the values of its type that
+ satisfy its constraint and any exclusion of the null value.
+
+We considered changing it to:
+
+ ...The set of values of a subtype consists of the values of its type that
+ satisfy its constraint, any exclusion of the null value, and any predicate.
+
+because conceptually, the values of the subtype include only values that obey
+the predicate, and indeed membership tests reflect that (X in T returns False if
+X the predicate is False). This view makes sense for well-defined predicates.
+However, 13.9.1(2) says:
+
+ A scalar object can have an invalid representation, which means that the
+ object's representation does not represent any value of the object's
+ subtype.
+
+and there are all kinds of permissions to check for invalid data. We don't want
+to allow optional evaluation of predicates in such cases. Anyway, an
+implementation can always have a mode where it does additional predicate checks.
+An implementation-defined Assertion_Policy could be used for this.
-???Question: Should we reconsider this? Perhaps allow a predicate check on any
-read of an object. Or any read of part of an object?
+However, we do say that the X'Valid is False if the predicate is False.
!example
-In a compiler familar to the author, type Symbol_Ptr references a symbol
-table entry. Most routines that take a symbol table entry only allow
-certain kinds of entry. It would be valuable to be able to specify
-those kinds of entry as part of the profile of the routine.
+In a compiler familar to the author, type Symbol_Ptr references a symbol table
+entry. Most routines that take a symbol table entry only allow certain kinds of
+entry. It would be valuable to be able to specify those kinds of entry as part
+of the profile of the routine.
A simplified example:
@@ -341,10 +359,11 @@
Now, a call to Type_Size or Generate_Call_Parameters with a pointer to the wrong
-kind of symbol record will be detected at the call site rather than at some later
-point. The call site is closer to the source of the error; in addition, it is
-possible that the compiler can prove that the predicate will succeed and be able to
-remove the check altogether. That can't happen for a check inside of a subprogram.
+kind of symbol record will be detected at the call site rather than at some
+later point. The call site is closer to the source of the error; in addition, it
+is possible that the compiler can prove that the predicate will succeed and be
+able to remove the check altogether. That can't happen for a check inside of a
+subprogram.
Other examples of useful predicates:
@@ -3144,8 +3163,1505 @@
****************************************************************
From: Bob Duff
-Date: Wednesday, April 28, 2010 5:30 PM
+Date: Monday, April 12, 2010 4:48 PM
+
+We've been discussing subtype predicates at AdaCore recently. Quote:
+
+I wrote:
+> Robert Dewar wrote:
+>
+> > By the way, in Ada 2012, you will be able to say something like
+> >
+> > if X in (Button_Pressed, Button_Released, Button_Broken) then ...
+> >
+> > making it easier to have a full list of the alternatives.
+>
+> Right, and that way, they don't need to be a contiguous subrange.
+>
+> Also (if I get my way) something like this:
+>
+> subtype Button_Event is Event
+> with Predicate =>
+> Button_Event in (Button_Pressed, Button_Released, Button_Broken);
+>
+> And then:
+>
+> if X in Button_Event then...
+
+Can we (ARG) please discuss this some more? My thinking is that this feature is
+far more important than "type invariants" (as currently defined).
+
+****************************************************************
+
+From: Robert Dewar
+Date: Monday, April 12, 2010 5:00 PM
+
+> Can we (ARG) please discuss this some more? My thinking is that this
+> feature is far more important than "type invariants"
+> (as currently defined).
+
+The reason I think this is more important than type invariants is that it is
+much more generally useful. Invariants are only useful if you adopt this style
+of programming.
+
+Subtype predicates if done right allow the definition of non-contiguous subtypes
+of enumeration types.
+
+I am tired of having to juggle the order of enumeration types so I can create
+the subtypes I need (the solution to this in general is NP complete of course,
+and of course there may not BE a solution).
+
+Would be much nicer to just define non-contiguous subtypes with an appropriate
+predicate (which can use set notation).
+
+****************************************************************
+
+From: Randy Brukardt
+Date: Monday, April 12, 2010 5:23 PM
+
+> Can we (ARG) please discuss this some more? My thinking is that this
+> feature is far more important than "type invariants"
+> (as currently defined).
+
+Discuss what? Supposedly, you guys decided how to fix all problems during the
+last ARG meeting (Burlington) [I was out of the room for most of that discussion
+and there are no minutes, at least of anything that fixes any problems.] There
+hasn't been a new draft since that meeting, so either you (a) want us to discuss
+old, superceded ideas (which is pointless), or (b) discuss new ideas that
+haven't been fleshed out (or even understood by me and I suspect others).
+
+I'd suggest that you (Bob) make a new draft that we can then discuss OR ask some
+specific questions that we can answer! Else we're discussing ghosts...
+
+P.S. I'm on record as opposing all of these ideas unless we have a mechanism for
+being able to safely (and correctly) eliminate them. That necessarily includes a
+way for the compiler to tell when these expressions have any (significant) side
+effects. The Global In/Global Out annotations being felt too complex (at least
+by many people), we need an alternative approach or we are wasting our time
+inventing things that don't meet the mandate to "improve contracts".
+
+****************************************************************
+
+From: Bob Duff
+Date: Sunday, April 18, 2010 4:37 PM
+
+Suppose we have:
+
+ type Color is (Red, Orange, Yellow, Green, Blue, Indigo, Violet);
+ subtype Primary_Color is Color
+ with Predicate => Primary_Color in (Red, Green, Blue);
+
+It would be really nice if this played well with the full coverage rules:
+
+ procedure P (X: Primary_Color) is
+ begin
+ case X is
+ when Red => ...;
+ when Green => ...;
+ when Blue => ...;
+ end case;
+ end P;
+
+So that "when Orange" is neither required nor allowed.
+
+So I suggest we say that if the predicate is given by "in" of a list of static
+expressions and subtypes and ranges (and nothing else), that the subtype be
+considered static.
+
+****************************************************************
+
+From: Tucker Taft
+Date: Sunday, April 18, 2010 4:59 PM
+
+Couldn't we generalize this to say that the subtype is static if it would be in
+the absence of the predicate expression, and the predicate expression would be
+static if the type name were replaced with a static value? This is similar to
+the static-in-the-instance rule -- see AARM 12.3(15.f).
+
+It will be annoying to have to use some
+very specific syntax for the predicate.
+
+****************************************************************
+
+From: Bob Duff
+Date: Sunday, April 18, 2010 6:09 PM
+
+> Couldn't we generalize this to say
+> that the subtype is static if it would be in the absence of the
+> predicate expression, and the predicate expression would be static if
+> the type name were replaced with a static value?
+
+Yes. Good idea. And I suppose the rules for static expressions of the "blah in
+blah" sort make this work?
+
+> This is similar to the static-in-the-instance rule -- see AARM
+> 12.3(15.f).
+
+Right.
+
+> It will be annoying to have to use some very specific syntax for the
+> predicate.
+
+Agreed. So you apparently agree with me that one should not have to put
+
+ when others => raise Program_Error; -- can't get here
+
+or
+
+ when Orange | ...etc => raise Program_Error; -- can't get here
+
+in such case statements! In fact, not allowed to.
+
+Shall I wax poetic once again to sing praises to the full coverage rules? ;-)
+
+****************************************************************
+
+From: Tucker Taft
+Date: Sunday, April 18, 2010 10:16 PM
+
+Yes, we can all sing in harmony about how much we love full coverage. While we
+are at it, I would love to solve the problem some day that nested variants
+always need a "when others" which is logically unnecessary. It would be nice if
+the discriminant's subtype, when inside a particular variant, effectively had a
+Predicate expression added that corresponds to the "when Red | Green =>" that
+started the variant.
+
+****************************************************************
+
+From: John Barnes
+Date: Monday, April 19, 2010 2:09 AM
+
+I must say that this topic seems really useful - unlike a lot of other stuff we
+have put into or contemplated putting into Ada lately.
+
+****************************************************************
+
+From: Bob Duff
+Date: Monday, April 19, 2010 9:24 AM
+
+I'm glad at least SOMEbody agrees with me!
+
+I think this feature is far more useful than:
+
+AI05-0146-1 -- Type and Package Invariants
+
+because predicates are not restricted to private types, and they work for
+subtypes.
+
+****************************************************************
+
+From: Edmond Schonberg
+Date: Monday, April 19, 2010 9:45 AM
+Note also that other languages have proposed type invariants, but subtypes as we
+understand them are Ada-specific, and it's reasonable to have additional formal
+properties of subtypes.
+
+****************************************************************
+
+From: Robert Dewar
+Date: Monday, April 19, 2010 10:01 AM
+
+>> I must say that this topic seems really useful - unlike a lot of
+>> other stuff we have put into or contemplated putting into Ada lately.
+>
+> I'm glad at least SOMEbody agrees with me!
+
+Me too! I agree with you and John.
+
+> I think this feature is far more useful than:
+>
+> AI05-0146-1 -- Type and Package Invariants
+
+I strongly agree, the invariants stuff is useful only to a subset of programmers
+who want to use this style of programming. The more flexible subtypes will be a
+boon to all Ada programmers.
+
+> because predicates are not restricted to private types, and they work
+> for subtypes.
+
+I do think full case coverage is important as noted by Bob
+
+Also, I have the impression that the intent is to allow dynamic ranges and
+values. I find this 100% useless, and I sure hope that this does not stand in
+the way of the useful case which is a fully static list.
+
+I think this is something that GNAT will probably implement anyway, but it would
+be nice to have it offcial, rather than be an extension requiring the -gnatX
+flag :-)
+
+****************************************************************
+
+From: Robert Dewar
+Date: Monday, April 19, 2010 10:04 AM
+
+By the way, there seems to be some concern here that variables of the subtype may not have valid values. So what? I see that as a problem with formal invariants, but for subtype predicates I don't even see if as a concern.
+
+When I write
+
+subtype RBG is RBGE range R .. G;
+
+I have no guarantee that objects of type R are in this range, so why should I
+care if I say
+
+subtype RBE is RBGE range (R, B, E); -- or wjatever the syntax is
+
+that the same is true.
+
+****************************************************************
+
+From: Randy Brukardt
+Date: Monday, April 19, 2010 2:20 PM
+
+> > Couldn't we generalize this to say
+> > that the subtype is static if it would be in the absence of the
+> > predicate expression, and the predicate expression would be static
+> > if the type name were replaced with a static value?
+>
+> Yes. Good idea. And I suppose the rules for static expressions of
+> the "blah in blah" sort make this work?
+
+I agree that if we do this, this is the way to go.
+
+But I don't agree that this is a good idea *for this particular feature*.
+
+You apparently want predicates that *happen* to occur on an elementary type and
+*happen* to have the form of a static expression to work exactly like a
+first-class constraint, while all other predicates work completely differently
+(and aren't even safe; they're just a automatic assertion).
+
+I think this is bad language design. We have a mostly worked out proposal for
+first-class set constraints, which have all of the properties that you seem to
+want *and* proper syntax and legality rules. The requirements for static set
+constraints and dynamic predicates are different (and could be *very* different
+if we wanted them to be). I don't think that it makes sense to mix them,
+especially given the unsafe nature of dynamic predicates.
+
+> Agreed. So you apparently agree with me that one should not have to
+> put
+>
+> when others => raise Program_Error; -- can't get here
+>
+> or
+>
+> when Orange | ...etc => raise Program_Error; -- can't get here
+>
+> in such case statements! In fact, not allowed to.
+
+I have no objection to such a feature for constraints, but not for predicates
+that could be dynamic (with side-effects!) or on composite types (and not hold
+after checking). If you want static checking, then you need static constraints.
+A predicate is not a constraint! (Surely not for composite types, it's arguable
+for scalar types, but it would be immensely confusing to have something that
+acts as a constraint sometimes but not always).
+
+There is also an implementation concern. For an arbitrary predicate expression
+(unlike the limited static set of the set constraint), the only way to implement
+a coverage check is to try every possible value in the expression and see if it
+is true or false. That would be very expensive for a 64-bit integer type!
+
+A compiler could recognize various patterns and eliminate the problem in some
+special cases, but I don't see any way to do it in general. The result would be
+that some case statements would be uncompilable (even if technically legal).
+
+****************************************************************
+
+From: Robert Dewar
+Date: Monday, April 19, 2010 2:30 PM
+
+> You apparently want predicates that *happen* to occur on an elementary
+> type and *happen* to have the form of a static expression to work
+> exactly like a first-class constraint, while all other predicates work
+> completely differently (and aren't even safe; they're just a automatic assertion).
+>
+> I think this is bad language design. We have a mostly worked out
+> proposal for first-class set constraints, which have all of the
+> properties that you seem to want *and* proper syntax and legality
+> rules. The requirements for static set constraints and dynamic
+> predicates are different (and could be
+> *very* different if we wanted them to be). I don't think that it makes
+> sense to mix them, especially given the unsafe nature of dynamic predicates.
+
+Why don't we allow them ONLY if they are completely static. This is really the
+only useful case anyway. Dynamic ranges are VERY rare on enumeration types, I am
+not sure I have ever written one. It would be a real shame if we let the design
+of a really useful feature (static non-contiguous subsets of enumeration types)
+be kept out because of theoretical concerns about the dynamic case, which is
+totally useless.
+
+I have no objection to allowing the dynamic case if it can be done without compromising the static case, but I *seriously* object to compromising the static case.
+
+> I have no objection to such a feature for constraints, but not for
+> predicates that could be dynamic (with side-effects!)
+
+So disallow them
+
+> There is also an implementation concern. For an arbitrary predicate
+> expression (unlike the limited static set of the set constraint), the
+> only way to implement a coverage check is to try every possible value
+> in the expression and see if it is true or false. That would be very
+> expensive for a 64-bit integer type!
+
+These are really only useful for enumeration types, again, worrying about the
+use on integer types seems bogus.
+
+> A compiler could recognize various patterns and eliminate the problem
+> in some special cases, but I don't see any way to do it in general.
+> The result would be that some case statements would be uncompilable
+> (even if technically legal).
+
+I agree this is horrible, so let's leave it out!
+
+I really think that the business of delicately arranging enumeration types in an
+order that allows all interesting subtypes to be continguous is one of the most
+horrible and unmaintainable features of Ada. It wastes a huge amount of time,
+and is really unpleasant.
+
+We have recently implemented a feature in GNAT that helps with this, which is a
+warning flag that disallows comparisons and subranges of an enumeration type in
+a client, unless a pragma Ordered is given for the enumeration type.
+
+At least now, when you modify an enumeration type, you don't have to worry about
+clients imposing additional buried constraints on the order.
+
+But having a proper way to deal with this would be SUCH an imrpovement and it
+seems like we are very nearly there.
+
+Please don't let absolute-best be the enemy of highly-useful when it comes to
+this feature.
+
+I see language design concerns and implementation concerns in what Randy writes
+with no apparent appreication for the enormous value of a subset of this feature
+(static non-contiguous constraints on enumeration types).
+
+****************************************************************
+
+From: Randy Brukardt
+Date: Monday, April 19, 2010 2:32 PM
+
+> Me too! I agree with you and John.
+
+I think the *goal* here is important, but I'm not convinced this is the right
+way to get to that goal. It's very similar to the situation with instantiating
+containers with private types in a package specification -- everyone agrees it
+is important, but we've never found anything that seems like a understandable,
+useful, and maintainable solution.
+
+...
+> > because predicates are not restricted to private types, and they
+> > work for subtypes.
+>
+> I do think full case coverage is important as noted by Bob
+>
+> Also, I have the impression that the intent is to allow dynamic ranges
+> and values. I find this 100% useless, and I sure hope that this does
+> not stand in the way of the useful case which is a fully static list.
+
+I'm confused here. "A fully static list" and "full case coverage" only makes
+sense for discrete types. The primary intent of this feature (and I can say that
+because it was originally my idea) was to get the effect of user-defined
+constraints on *composite* types (an idea which just doesn't work,
+unfortunately). I've always felt that it was best for discrete types to have
+*real* static set constraints (a-la AI05-0153-2). Indeed, I'd prefer to allow
+predicates only on composite types (but generic contract issues prevent that
+from being possible), given that they aren't air-tight. (There are many, many
+rules about discriminants that exist solely to prevent a discriminant constraint
+from being broken -- none of those will exist for [composite] predicates and
+thus it will be impossible to depend on most predicates -- they could be made
+False in many ways that wouldn't require them to be rechecked.)
+
+Anyway, Robert, could you expand on what you view as important? Are you talking
+about predicates on all types, or just discrete types, or something else? I'd
+like to make sure that I'm thinking about the same things that you are.
+
+****************************************************************
+
+From: Randy Brukardt
+Date: Monday, April 19, 2010 2:40 PM
+
+> By the way, there seems to be some concern here that variables of the
+> subtype may not have valid values. So what?
+
+That's not the concern. The concern is that for composite predicates (by far the
+most important kind), the predicate can be made False on an object for which the
+predicate was previously checked and passed without a further check. That is,
+even though previous checks occurred, the value might still not meet its
+predicate.
+
+With existing Ada constraints, once the check has been made and passes (that is,
+the object is valid), the object will always be within the constraint (excepting
+of course erroneous execution). That is definitely not true for composite
+predicates (no matter what rules for rechecking are used). It probably can be
+made true for scalar predicates, but that is a very minor use case for the
+feature as a whole.
+
+****************************************************************
+
+From: Tucker Taft
+Date: Monday, April 19, 2010 2:54 PM
+
+I had the sense we had chosen to go toward the more general subtype predicates
+rather than the somewhat special case of set constraints, given the natural
+combination of the new membership test and aspect specification constructs.
+
+It is already the case that you can have static scalar subtypes and static
+string subtypes, but not other kinds of static subtypes, so I don't see it odd
+that you can have static scalar predicated subtypes without necessarily having
+static non-scalar predicated subtypes.
+
+And it is true that staticness makes more of a difference for discrete types
+than for other scalar types. Again, that doesn't bother me.
+
+So to me, your objection to allowing these to be static seems mostly in the
+language-design- philosophy realm, but your concerns don't seem to jibe with
+existing Ada differences in staticness.
+
+The set constraints seem like a very special purpose construct, while this
+notion of subtype predicates seems more generally useful, with additional useful
+properties when everything is known statically.
+
+****************************************************************
+
+From: Robert Dewar
+Date: Monday, April 19, 2010 2:58 PM
+
+> I'm confused here. "A fully static list" and "full case coverage" only
+> makes sense for discrete types.
+
+I am only interested in enumeration types, I think this feature is highly
+dubious for other types, and given the difficulties in agreeing on a
+formulation, should be abandoned.
+
+> The primary intent of this feature (and I can say that because it was
+> originally my idea) was to get the effect of user-defined constraints
+> on *composite* types (an idea which just doesn't work, unfortunately).
+> I've always felt that it was best for discrete types to have *real*
+> static set constraints (a-la AI05-0153-2).
+
+That's what we really want I agree
+
+> Indeed, I'd prefer
+> to allow predicates only on composite types (but generic contract
+> issues prevent that from being possible), given that they aren't
+> air-tight. (There are many, many rules about discriminants that exist
+> solely to prevent a discriminant constraint from being broken -- none
+> of those will exist for [composite] predicates and thus it will be
+> impossible to depend on most predicates -- they could be made False in
+> many ways that wouldn't require them to be rechecked.)
+
+Fine but then I think this feature is unimportant and as far as I am concerned
+can be delayed till Ada 2112, when I won't have to worry about it.
+
+> Anyway, Robert, could you expand on what you view as important? Are
+> you talking about predicates on all types, or just discrete types, or
+> something else? I'd like to make sure that I'm thinking about the same
+> things that you are.
+
+I am ONLY interested in static precicates (whether you call them predicates or
+constraints is unimporant to me) on enumeration types, that's the only place I
+see a use for this in the way I code Ada!
+
+So very likely we aren't thinking about the same thing :-)
+
+****************************************************************
+
+From: Robert Dewar
+Date: Monday, April 19, 2010 3:01 PM
+
+>> By the way, there seems to be some concern here that variables of the
+>> subtype may not have valid values. So what?
+>
+> That's not the concern. The concern is that for composite predicates
+> (by far the most important kind), the predicate can be made False on
+> an object for which the predicate was previously checked and passed
+> without a further check. That is, even though previous checks
+> occurred, the value might still not meet its predicate.
+
+Well you see I think these are the LEAST important kind, so I don't care!
+
+> With existing Ada constraints, once the check has been made and passes
+> (that is, the object is valid), the object will always be within the
+> constraint (excepting of course erroneous execution). That is
+> definitely not true for composite predicates (no matter what rules for
+> rechecking are used). It probably can be made true for scalar
+> predicates, but that is a very minor use case for the feature as a whole.
+
+A good reason to leave out composite predicates.
+
+But to me scalar predicates are NOT a "very minor use case", they are a highly
+valuable addition to the language (more important in my opinion than all the
+pre/post condition stuff put together -- How could I say such a thing? Because I
+think nearly all Ada programmers can and will take advantage of non-contiguous
+subtypes of enumeration types, I think only a subset will take advantage of
+pre/post conditions. Of course that subset will find them VERY useful, so I
+agree with their inclusion.
+
+****************************************************************
+
+From: Robert Dewar
+Date: Monday, April 19, 2010 3:07 PM
+
+> I had the sense we had chosen to go toward the more general subtype
+> predicates rather than the somewhat special case of set constraints,
+> given the natural combination of the new membership test and aspect
+> specification constructs.
+
+I don't necessarily mind that generalization as long as it does not turn into a
+classic case of what I call the "system programmer syndrome".
+
+User: I need feature X, should be easy to implement
+
+System Programmer: Great, but that's just a special case of Y which is much more
+general.
+
+User: Fine, I am not sure how much more useful Y will be, but if you want to
+implement Y, go ahead it will give me X and that's what I want.
+
+Time passes .....
+
+User: whatever happened to feature X
+
+System Programmer: Ah, well we found that feature Y was much more complex than
+we thought, so we have postponed it till version 537 three years from now.
+
+> So to me, your objection to allowing these to be static seems mostly
+> in the language-design- philosophy realm, but your concerns don't seem
+> to jibe with existing Ada differences in staticness.
+
+That seems right
+
+> The set constraints seem like a very special purpose construct, while
+> this notion of subtype predicates seems more generally useful, with
+> additional useful properties when everything is known statically.
+
+That also seems right to me, providing it does not lose us the useful spcial
+purpose feature :-)
+
+****************************************************************
+
+From: Randy Brukardt
+Date: Monday, April 19, 2010 3:46 PM
+
+> It is already the case that you can have static scalar subtypes and
+> static string subtypes, but not other kinds of static subtypes, so I
+> don't see it odd that you can have static scalar predicated subtypes
+> without necessarily having static non-scalar predicated subtypes.
+
+Predicates are just a special form of assertions, and I find the notion of
+"static assertions" to be extremely odd (harmful, even).
+
+It's fairly clear that the rules for composite (and access) predicates could and
+probably should be very different from those for elementary types. If we want
+vastly different rules, then I believe that they should *look* different.
+
+> And it is true that staticness makes more of a difference for discrete
+> types than for other scalar types. Again, that doesn't bother me.
+>
+> So to me, your objection to allowing these to be static seems mostly
+> in the language-design- philosophy realm, but your concerns don't seem
+> to jibe with existing Ada differences in staticness.
+
+My point is that I don't like taking arbitrary dynamic expressions and treating
+them as static. The more I think about it, the more I think that you're analogy
+with instances just does not hold true. In the instance case, all of the
+constituents of the expression are known and are known to be static. The effect
+is to evaluate the expression at the point of the instance.
+
+In the case statement case, you have no idea what the value is, only some
+(possibly very little) information about its range. This is much more like the
+state inside the generic template (with an unknown formal object) than it is
+related to the instance (with a known static actual object). The only way to
+determine the result of the expression for a particular value is to try it:
+which means evaluating up to 2**64 static expressions. That's going to take too
+long.
+
+Since we need to restrict the expressions to a form that can be evaluated in a
+reasonable time, it makes much more sense to use a dedicated syntax for it. In
+that case, we get proper static matching (there is no way to match predicate
+expressions, at least without creating a bunch of new rules), use in for loops,
+case statement/variant/aggregate choices, as well as case completeness.
+
+****************************************************************
+
+From: Randy Brukardt
+Date: Monday, April 19, 2010 4:00 PM
+
+> > I had the sense we had chosen to go toward the more general subtype
+> > predicates rather than the somewhat special case of set constraints,
+> > given the natural combination of the new membership test and aspect
+> > specification constructs.
+>
+> I don't necessarily mind that generalization as long as it does not
+> turn into a classic case of what I call the "system programmer
+> syndrome".
+...
+> > The set constraints seem like a very special purpose construct,
+> > while this notion of subtype predicates seems more generally useful,
+> > with additional useful properties when everything is known statically.
+>
+> That also seems right to me, providing it does not lose us the useful
+> spcial purpose feature :-)
+
+I think we're very much at risk of "system programmer syndrome" with predicates.
+The people who voted against "keep it alive" at the last ARG meeting were
+concerned about the holes in the composite model. And tacking staticness and for
+loops and the like onto it is not going to make them feel any better (it is
+getting more and more complex with little additional benefit).
+
+Indeed, the original proposal for "predicates" came about as Steve and I were
+trying to justify the apparently heavier "set constraint" proposal. I created it
+as a sort of straw-man to show that the predicate idea doesn't work without a
+lot of funny restrictions and knick-knacks (and I never *conceived* of making
+them static and essentially using the semantics the set constraints).
+
+My understanding of the reasons we moved on from set constraints (which are very
+different than Tuck's understanding) was that they just looked to be too
+heavyweight for the benefit. Surely putting all of the same semantics into
+predicates is going to make this somehow lighter.
+
+Part of the problem here is that people are trying to use this for two unrelated
+purposes: one is to abstract pre and postconditions on single parameters (and
+make them much more Ada-like), and the other is to provide static set
+functionality. The overlap between these is pretty small, and trying to use the
+same feature for both causes it to get really clunky.
+
+Keep in mind that we don't use the same syntax to describe composite
+(discriminant, index) and scalar (range) constraints. Set constraints are really
+constraints in every reasonable sense, and ought to be described as such
+(especially if you want legality rules to depend on them). Composite predicates
+are constraints in *no* sense -- they don't provide the information needed to
+describe the "shape" (discriminants, bounds) of a value, so they can't be
+constraints. So these are very different things and as such, they ought to look
+different.
+
+****************************************************************
+
+From: Tucker Taft
+Date: Monday, April 19, 2010 4:27 PM
+
+...
+> My point is that I don't like taking arbitrary dynamic expressions and
+> treating them as static. The more I think about it, the more I think
+> that you're analogy with instances just does not hold true. In the
+> instance case, all of the constituents of the expression are known and
+> are known to be static. The effect is to evaluate the expression at
+> the point of the instance.
+>
+
+I am losing you here. I am talking about considering a subtype with a predicate
+as a "static" subtype only if it meets all the usual criteria (constraint is
+static, "parent" subtype is static, etc.), plus the predicate will be static if
+you substitute in a static value for the subtype. So I am confused by the term
+"arbitrary dynamic expression." But perhaps the example I give below
+illustrates your issue?
+
+> In the case statement case, you have no idea what the value is, only
+> some (possibly very little) information about its range. This is much
+> more like the state inside the generic template (with an unknown
+> formal object) than it is related to the instance (with a known static
+> actual object). The only way to determine the result of the expression
+> for a particular value is to try it: which means evaluating up to
+> 2**64 static expressions. That's going to take too long.
+
+So let me see if I understand your concern:
+
+ subtype Very_Even is Long_Long_Integer range 0..2**62;
+ with Predicate => Very_Even mod 2**60 = 0;
+
+ procedure Use_Very_Even(X : Very_Even) is
+ begin
+ case X is
+ when 0 => ...
+ when 2**60 => ...
+ when 2**62 => ...
+ end case;
+ end Use_Very_Even;
+
+The question is, does the above provide complete coverage? Well, to decide
+that, we need to find at least one value that is in Very_Even but not covered by
+the case statement (e.g. 2**61).
+
+So the values that aren't covered in the overall range of Very_Even are:
+{1..2**60-1, 2**60+1..2**62-1} We will have to iterate through this very long
+sequence checking the predicate. If the predicate is False in many cases in
+this range, then we might go through a lot of cases before we found one for
+which Very_Even's predicate evaluated to True. In this case, we might check
+something like 2**61-2 values before discovering that 2**61 is not covered.
+
+That does seem to be an issue, given the age of the universe... ;-).
+
+> Since we need to restrict the expressions to a form that can be
+> evaluated in a reasonable time, it makes much more sense to use a
+> dedicated syntax for it. In that case, we get proper static matching
+> (there is no way to match predicate expressions, at least without
+> creating a bunch of new rules), use in for loops, case
+> statement/variant/aggregate choices, as well as case completeness.
+
+So much for generalization. I guess you have convinced me that checking
+completeness with arbitrary "static" predicates is not feasible. But
+unfortunately we do seem to be going in circles on this idea.
+
+****************************************************************
+
+From: Randy Brukardt
+Date: Monday, April 19, 2010 4:50 PM
+
+> I am losing you here. I am talking about considering a subtype with a
+> predicate as a "static" subtype only if it meets all the usual
+> criteria (constraint is static, "parent"
+> subtype is static, etc.), plus the predicate will be static if you
+> substitute in a static value for the subtype. So I am confused by the
+> term "arbitrary dynamic expression." But perhaps the example I give
+> below illustrates your issue?
+
+Yes, the example below illustrates this point perfectly. I consider the
+expression "dynamic" because it itself is not static (just as an expression that
+depends on a formal object is not static, even though it might be in an
+instance).
+
+...
+> That does seem to be an issue, given the age of the universe... ;-).
+
+Right. And this is worse because the compiler has to do it even if all of needed
+values are given (since it has to check that none are missed). So even case
+statements that are correct have this time penalty.
+
+I can imagine having special cases to prevent this for common cases, but it will
+always be possible to write a more complex predicate that didn't match any of
+the special cases.
+
+> > Since we need to restrict the expressions to a form that can be
+> > evaluated in a reasonable time, it makes much more sense to use a
+> > dedicated syntax for it. In that case, we get proper static matching
+> > (there is no way to match predicate expressions, at least without
+> > creating a bunch of new rules), use in for loops, case
+> > statement/variant/aggregate choices, as well as case completeness.
+>
+> So much for generalization. I guess you have convinced me that
+> checking completeness with arbitrary "static"
+> predicates is not feasible. But unfortunately we do seem to be going
+> in circles on this idea.
+
+I realize that. The "softer" issue of "good" language design is rather
+subjective in any case. But I've always felt since I worked out the initial
+version of the details of these two proposals that the set constraint version
+was preferable for discrete types (because it naturally supported the needed
+legality rules, it automatically gives for loop iteration and case statements,
+it probably could be used to fix the variant problem you noted, etc.).
+
+What I didn't succeed at is finding a decent replacement for the composite
+predicates (you didn't like my restricted discriminant constraints at all). And
+I think that problem deserves a solution as well - as does Bob - which is how we
+ended up back with the predicates. I've personally come to the conclusion that
+these things are different enough that perhaps we ought to solve them
+differently, but I may not win that case.
+
+****************************************************************
+
+From: Bob Duff
+Date: Monday, April 19, 2010 5:56 PM
+
+> I am only interested in enumeration types, I think this feature is
+> highly dubious for other types, and given the difficulties in agreeing
+> on a formulation, should be abandoned.
+
+I think you're confusing two different features, here. In my message about
+case-full-coverage, I combined these two features.
+
+I strongly believe that "subtype predicates" need to be a general purpose
+feature, without arbitrary restrictions. They should be allowed on any subtype,
+and should allow arbitrary expressions.
+
+The other feature is the "X in (Red, Green, Blue)" syntax. I think it's fine
+for that to be restrictive (require X to be discrete, and require Red, etc to be
+static). That's probably already the case.
+
+For subtype predicates, generality simplifies.
+For the "X in ..." thing, removing generality simplifies.
+
+Restricting subtype predicates to static expressions would be a disaster. It
+would disallow the single most important tool for abstraction that has ever been
+invented (the subroutine call, with parameter passing)! I definitely want to be
+able to say "with Predicate => Is_Gnarly (S)".
+
+I am not saying I want to put side effects in assertions. Is_Gnarly probably
+doesn't have any (or only has benign ones). But the compiler can't know that.
+
+Restricting subtype predicates to enum types would also be a disaster.
+They are desperately needed also on discriminated types, and on pointers to
+discriminated types, and on things that behave like those (like Node_Id in the
+GNAT compiler, which is conceptually a pointer-to-record, but is actually
+implemented as an index into a table).
+
+Here's an example:
+
+In GNAT, we have:
+
+ type Node_Id is range Node_Low_Bound .. Node_High_Bound;
+ -- Type used to identify nodes in the tree
+
+ subtype Entity_Id is Node_Id;
+ -- A synonym for node types, used in the Einfo package to refer to nodes
+ -- that are entities (i.e. nodes with an Nkind of N_Defining_xxx). ...
+
+ type Entity_Kind is (...); -- dozens of enum lits
+
+ subtype Access_Subprogram_Kind is Entity_Kind range
+ E_Access_Subprogram_Type ..
+ -- E_Anonymous_Access_Subprogram_Type
+ -- E_Access_Protected_Subprogram_Type
+ E_Anonymous_Access_Protected_Subprogram_Type;
+
+and dozens of subtypes like that.
+
+What I want is:
+
+ subtype Access_Subprogram_Kind is Entity_Kind with
+ predicate =>
+ Access_Subprogram_Kind in
+ (E_Access_Subprogram_Type,
+ E_Anonymous_Access_Subprogram_Type,
+ E_Access_Protected_Subprogram_Type,
+ E_Anonymous_Access_Protected_Subprogram_Type);
+
+ subtype Access_Subprogram_Entity_Id is Entity_Id with
+ predicate =>
+ Ekind (Access_Subprogram_Entity_Id) in Access_Subprogram_Kind;
+ -- Here we have a predicate on a non-enum type, and we are calling
+ -- the function Ekind, so it is not a static expression.
+
+We have thousands of procedures like this:
+
+ procedure Do_Something (N : Entity_Id) is
+ Thing : Node_Id;
+ ...
+
+which could be hugely improved:
+
+ procedure Do_Something (N : Access_Subprogram_Entity_Id) is
+ Thing : Case_Statement_Node_Id;
+ ...
+
+documenting what parameters and locals are supposed to be, and ensuring via
+run-time checks that the documentation is likely correct.
+
+****************************************************************
+
+From: Bob Duff
+Date: Monday, April 19, 2010 5:56 PM
+
+> subtype Very_Even is Long_Long_Integer range 0..2**62;
+> with Predicate => Very_Even mod 2**60 = 0;
+...
+> That does seem to be an issue, given the age of the universe... ;-).
+
+I'm not asking for that much generality!
+
+From my earlier message:
+
+ So I suggest we say that if the predicate is given by "in" of
+ a list of static expressions and subtypes and ranges (and nothing else),
+ that the subtype be considered static.
+
+This seems easy to define, easy to understand, easy to implement, and easy to
+implement efficiently.
+
+But it's just a nice-to-have. I can do without this, but I insist that
+predicates are an important feature, and should not have arbitrary restrictions.
+
+****************************************************************
+
+From: Bob Duff
+Date: Monday, April 19, 2010 5:57 PM
+
+ARG tends to fall into the trap of letting "perfect" be the enemy of "good
+enough"! That's the case here.
+
+I understand the discomfort that Randy and others have with subtype predicates
+-- the predicate could become False in some circumstances, so can't be 100%
+relied upon.
+
+But I think we should focus on comparing what we have now with what subtype
+predicates provide. Right now, we have (from my earlier GNAT example):
+
+ subtype Entity_Id is Node_Id;
+ -- A synonym for node types, used in the Einfo package to refer to nodes
+ -- that are entities (i.e. nodes with an Nkind of N_Defining_xxx). ...
+
+Right now, that predicate ("nodes with an Nkind of N_Defining_xxx") is just a
+comment and is totally unchecked.
+
+With subtype predicates, we get checks sprinkled all over the place, so it
+becomes highly unlikely that an object of subtype Entity_Id will have a wrong
+Nkind. Not impossible, but highly unlikely. And if it happens, it will likely
+be caught soon after.
+
+That seems like a huge benefit. We don't know how to make it impossible (too
+bad). So let's go for "good enough".
+
+****************************************************************
+
+From: Robert Dewar
+Date: Monday, April 19, 2010 6:15 PM
+
+> The other feature is the "X in (Red, Green, Blue)" syntax. I think
+> it's fine for that to be restrictive (require X to be discrete, and
+> require Red, etc to be static). That's probably already the case.
+
+OK, so perhaps I am mixing two features, but then this "other feature" is the
+one I am interested in. I can't get very excited about the more general subtype
+predicates that constitute the other feature. I don't object to them, I just
+don't find them a very important feature to add.
+
+> Restricting subtype predicates to static expressions would be a
+> disaster. It would disallow the single most important tool for
+> abstraction that has ever been invented (the subroutine call, with
+> parameter passing)! I definitely want to be able to say "with Predicate => Is_Gnarly (S)".
+
+I don't object to that, I just don't think I would find it that useful.
+
+> Restricting subtype predicates to enum types would also be a disaster.
+> They are desperately needed also on discriminated types, and on
+> pointers to discriminated types, and on things that behave like those
+> (like Node_Id in the GNAT compiler, which is conceptually a
+> pointer-to-record, but is actually implemented as an index into a table).
+
+OK, well I never felt the desparate need I guess in code that I have written.
+
+...
+> which could be hugely improved:
+>
+> procedure Do_Something (N : Access_Subprogram_Entity_Id) is
+> Thing : Case_Statement_Node_Id;
+
+Sorry I don't see it, how is this a huge improvement over an assertion inside
+Do_Something that says
+
+ Assert (Ekind (N) in Access_Subprogram_Kind);
+
+I see it is a bit neater, but I don't see any huge gain.
+Indeed in this case we can simply have a precondition for Do_Something that does
+this check. Why will the notation you suggest be any improvement, I don't get
+it, I must be missing something. I don't see that your notation allows some kind
+of static checking, it will still result in a test, just like the precondition
+or assertion. ... > documenting what parameters and locals are supposed to be,
+and > ensuring via run-time checks that the documentation is likely correct.
+
+But surely preconditions do this also?
+
+Actually, in many many of the compiler cases, error conditions can lead to
+violations of what you expect anyway, and you don't have assertions, you have
+error tests indicating diagnostics.
+
+Well I am unconvinced. But as long as I end up with a solution to the serious
+problem of not being able to manage any more to deinfe the enumeration type with
+all the subtypes I want, I have no objection to a more general feature. I just
+don't think I will find it very useful, certainly not in the compiler. I know
+Bob postulates a useful use, but I can't say from my experience that this will
+be helpful.
+
+****************************************************************
+
+From: Robert Dewar
+Date: Monday, April 19, 2010 6:17 PM
+
+> Right now, that predicate ("nodes with an Nkind of N_Defining_xxx") is
+> just a comment and is totally unchecked.
+
+That is false to me, in many many places we have explicit or implicit checks. If
+we pass a Node_Id where an Entity_Id is required, then almost always there will
+be a call to a function that contains an assertion that it is being applied to
+an entity. So the "totally unchecked" here is bogus.
+
+> With subtype predicates, we get checks sprinkled all over the place,
+> so it becomes highly unlikely that an object of subtype Entity_Id will
+> have a wrong Nkind. Not impossible, but highly unlikely.
+> And if it happens, it will likely be caught soon after.
+
+It's highly unlikely now!
+>
+> That seems like a huge benefit. We don't know how to make it
+> impossible (too bad). So let's go for "good enough".
+
+I am unconvinced by this example.
+
+****************************************************************
+
+From: Bob Duff
+Date: Monday, April 19, 2010 6:17 PM
+
+You said you were out of the room during part of the discussion if this AI at
+the meeting at SofCheck. I don't remember that, but I believe you. Too bad -- I
+rely on your excellent Minutes to remember what we discussed/decided.
+
+Anyway, I thought I had convinced most ARG members that it's OK for subtype
+predicates to have some loopholes -- they're still useful. The fact that we
+can't plug the loopholes shouldn't kill the whole idea.
+
+By the way, in one of your messages, you said, "A predicate is not a
+constraint!" and some other stuff along those lines. I'm confused by such
+remarks -- when you say such things, could you please explain what you mean by
+"constraint" and the like? I know what a "constraint" is in Ada, but we're
+changing Ada, so we could change the meaning of "constraint", and I don't know
+of any particular constraints on what "constraint" means (or OUGHT to mean).
+
+Let's not get too hung up on terminology. We have (or might have) "constraints"
+(5 kinds), "null exclusions", "invariants", "predicates". For us language
+lawyers, there are important distinctions amongst these things. But let's
+remember the users -- to an Ada programmer, those are all basically the same.
+They all serve basically the same purpose, and the differences are minor
+details.
+
+****************************************************************
+
+From: Randy Brukardt
+Date: Monday, April 19, 2010 6:54 PM
+
+> You said you were out of the room during part of the discussion if
+> this AI at the meeting at SofCheck. I don't remember that, but I
+> believe you.
+> Too bad -- I rely on your excellent Minutes to remember what we
+> discussed/decided.
+
+Well, unfortunately someone else is going to have to remember. When I came back,
+Tucker claimed that "the hole had been plugged", which is an amazing statement
+to me, and I have no idea how that was supposely accomplished.
+
+> Anyway, I thought I had convinced most ARG members that it's OK for
+> subtype predicates to have some loopholes -- they're still useful.
+> The fact that we can't plug the loopholes shouldn't kill the whole
+> idea.
+
+Apparently not all, however, as there was a "no" vote on the "keep alive"
+motion. I don't recall how I voted, but I suspect I abstained given that I was
+out of the room for quite a while.
+
+> By the way, in one of your messages, you said, "A predicate is not a
+> constraint!" and some other stuff along those lines.
+> I'm confused by such remarks -- when you say such things, could you
+> please explain what you mean by "constraint" and the like? I know
+> what a "constraint"
+> is in Ada, but we're changing Ada, so we could change the meaning of
+> "constraint", and I don't know of any particular constraints on what
+> "constraint" means (or OUGHT to mean).
+
+I explained that in another message today. For scalar predicates, there is no
+interesting difference. But a composite predicate is missing a very important
+property of a constraint: it doesn't provide values for the bounds or
+discriminants. That means that one cannot declare an object of a subtype of an
+indefinite type that has a predicate unless it also has a real constraint. Thus
+we need to keep the two things separate.
+
+I sort of worked out how one could have "partial" discriminant constraints (that
+would allow only subsets of discriminants), but (A) people, especially Tucker,
+hated the idea; (B) no extension to index constraints is obvious. So I think it
+remains critical that these aren't constraints (at least in the composite case).
+
+> Let's not get too hung up on terminology. We have (or might
+> have) "constraints" (5 kinds), "null exclusions", "invariants",
+> "predicates".
+> For us language lawyers, there are important distinctions amongst
+> these things. But let's remember the users -- to an Ada programmer,
+> those are all basically the same. They all serve basically the same
+> purpose, and the differences are minor details.
+
+I don't think I'm hung up on terminology. I just don't like the idea of saying
+that:
+
+ subtype Reds is Colors with Predicate => Reds in (Red | Yellow | Orange);
+
+has magic static properties, while
+
+ subtype Blues is Colors with Predicate => (Blues = Blue or Blues = Violet or Blues = Indigo);
+
+does not have the same properties. (And we've already proven that generalizing
+what expressions are static doesn't work in general.)
+
+The set constraint doesn't have this problem because there it is the only syntax
+allowed (period):
+
+ subtype Reds is Colors when Red | Yellow | Orange;
+
+If the most important thing is the static sets (as Robert has said he feels),
+then that is a far better solution (since it doesn't bring in any other problems
+- lack of optimizability, holes for composite types, etc. - and it allows a bit
+more as well -- for loops in particular).
+
+****************************************************************
+
+From: Robert Dewar
+Date: Monday, April 19, 2010 6:55 PM
+
+> You said you were out of the room during part of the discussion if
+> this AI at the meeting at SofCheck. I don't remember that, but I believe you.
+> Too bad -- I rely on your excellent Minutes to remember what we
+> discussed/decided.
+>
+> Anyway, I thought I had convinced most ARG members that it's OK for
+> subtype predicates to have some loopholes -- they're still useful.
+> The fact that we can't plug the loopholes shouldn't kill the whole idea.
+
+I definitely agree with this. After all there are loopholes with ordinary static
+constraints:
+
+ type R is range 1 .. 10;
+ A : R := 5;
+
+No other assignments to A exist
+
+Do we know that A will always be 1 .. 10
+
+Answer: No, there are several ways for A to get messed up. We declare some of
+these to be erroneous, and some to be OK, e,g, overlaying A with a float and
+modifying the float.
+
+But we don't get upset that the range is not a 100% guarantee.
+
+> By the way, in one of your messages, you said, "A predicate is not a
+> constraint!" and some other stuff along those lines. I'm confused by
+> such remarks -- when you say such things, could you please explain
+> what you mean by "constraint" and the like? I know what a "constraint"
+> is in Ada, but we're changing Ada, so we could change the meaning of
+> "constraint", and I don't know of any particular constraints on what
+> "constraint" means (or OUGHT to mean).
+>
+> Let's not get too hung up on terminology. We have (or might have)
+> "constraints" (5 kinds), "null exclusions", "invariants", "predicates".
+> For us language lawyers, there are important distinctions amongst
+> these things. But let's remember the users -- to an Ada programmer,
+> those are all basically the same. They all serve basically the same
+> purpose, and the differences are minor details.
+
+I agree, I don't understand the distinction Randy tries to draw between a
+constraint and a predicate, they seem the same fundamental thing to me.
+
+****************************************************************
+
+From: Randy Brukardt
+Date: Monday, April 19, 2010 7:16 PM
+
+...
+> Sorry I don't see it, how is this a huge improvement over an assertion
+> inside Do_Something that says
+>
+> Assert (Ekind (N) in Access_Subprogram_Kind);
+>
+> I see it is a bit neater, but I don't see any huge gain.
+> Indeed in this case we can simply have a precondition for Do_Something
+> that does this check. Why will the notation you suggest be any
+> improvement, I don't get it, I must be missing something. I don't see
+> that your notation allows some kind of static checking, it will still
+> result in a test, just like the precondition or assertion.
+
+Yes, of course you could write these as assertions or preconditions. But unlike
+assertions or preconditions, these aren't "bolted" on to the language -- they're
+directly taking advantage of an important Ada feature - subtyping. After all,
+one of the most important uses of subtypes in Ada to date is to provide
+preconditions on individual parameters. Predicates were intended to expand this
+well-understood Ada feature to user-written checks.
+
+Also note that there is an improvement in checking, in that the compiler can
+eliminate redundant checks (subject to rules that are still TBD). (This isn't a
+huge deal, but it helps.) In particular, a subtype conversion to the same
+subtype can usually eliminate the check, even if the compiler does not know
+whether the call has side-effects. Doing that with preconditions or assertions
+would be wrong.
+
+As an example (another compilery thing): (Assume Expensive_Function cannot be
+declared Pure.)
+
+ subtype Object_Node is Node with Predicate => Expensive_Function (Object_Node);
+
+ function Get_Object_Node (Symbol : in Node_Access) return Object_Node;
+
+ function Nominal_Subtype (Node : in Object_Node) return Type_Index;
+
+ ... Nominal_Subtype (Get_Object_Node (Some_Symbol)); -- No call on Expensive_Function here.
+
+If this was written as a precondition instead, the compiler could not eliminate
+the call on Expensive_Function.
+
+In addition, reusing this "precondition" on many subprograms becomes trivial.
+OTOH, full preconditions tend to differ on different subprograms (because
+multiple parameters need to be checked, interactions between parameters need to
+be checked, and the like). Thus using preconditions to do the job of subtypes
+makes the code larger, harder to read, and a lot more redundant (meaning harder
+to maintain).
+
+Besides, if Preconditions "are just tests", I don't want them either. I think we
+have to *allow* nasty expressions with side-effects in preconditions and
+predicates, but we must give the compiler the tools to do various sorts of
+static analysis on preconditions and predicates (and to be able to warn about
+ones that it cannot do analysis on, as these are likely to be dangerous). That
+implies (optionally) making side-effects visible in the contracts of functions.
+Pascal has noted that he considered preconditions that don't hold within the
+called subprogram to be actively harmful -- we already have assertions for tests
+that don't hold afterwards, why have more such things?
+
+Anyway, I think it is clear that there are two separate features here, and
+trying to mix them might be a problem. It's better that each stand and fall
+based on their own merits.
+
+****************************************************************
+
+From: Randy Brukardt
+Date: Monday, April 19, 2010 7:22 PM
+
+...
+> I agree, I don't understand the distinction Randy tries to draw
+> between a constraint and a predicate, they seem the same fundamental
+> thing to me.
+
+Please read my earlier responses to you and to Bob.
+
+But keep in mind that predicates are intended for all types. If we're *only*
+talking about discrete types, we've all agreed that we don't want predicates at
+all (the added ability of being able to say "Is_Even (Even)" is not worth it. If
+we're only doing discrete types, we surely would use set constraints as
+described in AI05-0153-2. It's the strong desire for a more general construct
+that forces the difference.
+
+****************************************************************
+
+From: Bob Duff
+Date: Monday, April 19, 2010 7:23 PM
+
+> I definitely agree with this. After all there are loopholes with
+> ordinary static constraints:
+>
+> type R is range 1 .. 10;
+> A : R := 5;
+>
+> No other assignments to A exist
+>
+> Do we know that A will always be 1 .. 10
+>
+> Answer: No, there are several ways for A to get messed up. We declare
+> some of these to be erroneous, and some to be OK, e,g, overlaying A
+> with a float and modifying the float.
+
+Well, that involves a chapter-13-ish feature, which is a different sort of
+loophole, so I think a better example would be:
+
+ Blah : R; -- uninitialized
+ ...
+ A := Blah; -- A might be outside 1..10 now
+
+> But we don't get upset that the range is not a 100% guarantee.
+
+Yes!
+
+We hate such bugs, but we don't throw the baby out with the bathwater, as in
+"then everything should be Integer".
+
+****************************************************************
+
+From: Bob Duff
+Date: Monday, April 19, 2010 7:27 PM
+
+> I agree, I don't understand the distinction Randy tries to draw
+> between a constraint and a predicate, they seem the same fundamental
+> thing to me.
+
+And there's some damage from all this profusion of jaw-breaking terminology.
+I mean, how many Ada programmers understand the subtle distinction between a
+"parent type" and a "progenitor type"?
+
+****************************************************************
+
+From: Robert Dewar
+Date: Monday, April 19, 2010 7:28 PM
+
+> Yes, of course you could write these as assertions or preconditions.
+> But unlike assertions or preconditions, these aren't "bolted" on to
+> the language
+> -- they're directly taking advantage of an important Ada feature -
+> subtyping. After all, one of the most important uses of subtypes in
+> Ada to date is to provide preconditions on individual parameters.
+> Predicates were intended to expand this well-understood Ada feature to user-written checks.
+
+OK, so it's really only an aesthetic issue, not one of any fundamental
+capability.
+
+> Also note that there is an improvement in checking, in that the
+> compiler can eliminate redundant checks (subject to rules that are
+> still TBD). (This isn't a huge deal, but it helps.) In particular, a
+> subtype conversion to the same subtype can usually eliminate the
+> check, even if the compiler does not know whether the call has
+> side-effects. Doing that with preconditions or assertions would be wrong.
+
+Why, you don't have to evaluate a precondition you know will succeed, very often
+the compiler can be sure there are no side effects. Actually I would like to see
+an implementation permission that says
+
+It is not necessary to call a function in a precondition or postcondition or
+assertion, if the only reason for making the call is to execute possible side
+effects. if the value of the assertion can be established without such calls,
+they need not be made.
+
+This is similar to some of the things we say in 11.6, where if you know an
+exception will be raised, you don't have to evaluate things just for the sake of
+side effects.
+
+****************************************************************
+
+From: Robert Dewar
+Date: Monday, April 19, 2010 7:31 PM
+
+> Well, that involves a chapter-13-ish feature, which is a different
+> sort of loophole, so I think a better example would be:
+>
+> Blah : R; -- uninitialized
+> ...
+> A := Blah; -- A might be outside 1..10 now
+
+Well it's a different kind of error indeed, but I don't see chapter 13 as
+somehow different, and the interesting thing about my example is that it can
+happen even if your coding standards require absolutely everything to be
+initialized.
+
+****************************************************************
+
+From: Robert Dewar
+Date: Monday, April 19, 2010 7:33 PM
+
+> And there's some damage from all this profusion of jaw-breaking terminology.
+> I mean, how many Ada programmers understand the subtle distinction
+> between a "parent type" and a "progenitor type"?
+
+As long as compilers don't make the mistake of using obscure technical terms in
+error messages, they don't need to know :-)
+
+****************************************************************
+
+From: Randy Brukardt
+Date: Monday, April 19, 2010 7:44 PM
+
+> > I agree, I don't understand the distinction Randy tries to draw
+> > between a constraint and a predicate, they seem the same fundamental
+> > thing to me.
+>
+> And there's some damage from all this profusion of jaw-breaking
+> terminology.
+> I mean, how many Ada programmers understand the subtle distinction
+> between a "parent type" and a "progenitor type"?
+
+If you can figure out how to define a composite "constraint" that doesn't
+constrain anything, be my guest. I'll let you face the wrath-of-Baird (and
+of-Adam). :-) Rewriting large parts of the standard to shoe-horn in the same
+terminology for something that does not currently exist does not sound appealing
+to me.
+
+****************************************************************
+
+From: Bob Duff
+Date: Monday, April 19, 2010 7:53 PM
+
+> OK, so it's really only an aesthetic issue, not one of any fundamental
+> capability.
+
+But that's like saying "type T is range 1..10;" is just an aesthetic issue.
+After all, you could put "Assert (X in 1..10);" on every assignment or parameter
+passing to every object of that subtype.
+
+The point of pre/post/invariant/predicate/constraint is that the "asserts" get
+sprinkled around in (almost) all relevant places automatically.
+
+> Why, you don't have to evaluate a precondition you know will succeed,
+> very often the compiler can be sure there are no side effects.
+> Actually I would like to see an implementation permission that says
+>
+> It is not necessary to call a function in a precondition or
+> postcondition or assertion, if the only reason for making the call is
+> to execute possible side effects. if the value of the assertion can be
+> established without such calls, they need not be made.
+
+I think I agree with that, but...
+
+> This is similar to some of the things we say in 11.6, where if you
+> know an exception will be raised, you don't have to evaluate things
+> just for the sake of side effects.
+
+...but it's less important in this case, because the compiler doesn't HAVE to do
+anything at all -- there are modes in which assertions are totally unchecked, so
+there can be intermediate modes in which they are somewhat checked according to
+whatever rules the compiler writer likes.
+
+****************************************************************
+
+From: Randy Brukardt
+Date: Monday, April 19, 2010 7:59 PM
+
+> > And there's some damage from all this profusion of jaw-breaking terminology.
+> > I mean, how many Ada programmers understand the subtle distinction
+> > between a "parent type" and a "progenitor type"?
+>
+> If you can figure out how to define a composite "constraint"
+> that doesn't constrain anything, be my guest. I'll let you face the
+> wrath-of-Baird (and of-Adam). :-) Rewriting large parts of the
+> standard to shoe-horn in the same terminology for something that does
+> not currently exist does not sound appealing to me.
+
+This actually makes me angry, because I spent a lot of effort doing precisely
+what you are advocating: define these as user-defined constraints. And my thanks
+for that work was Steve spewing out enough loopholes and problems to make me
+want to jump off of those cliffs in Brest.
+
+So I renamed them "predicates". That wasn't my first choice at all. Now you are
+making the claim that "a constraint can be anything we want it to be". Well,
+maybe: if we're willing to check and change every existing use of the term
+"constraint" in the Standard - 40 clauses have such uses, many have multiple
+uses. What is surely true is that we can't just claim that it is fine to call it
+a "constraint" because it is not by the current definition of "constraint" in
+the standard. And we'd need to change the rules for composite types to allow
+constraints that still leave the subtype indefinite and to allow multiple
+constraints on composite types -- both of which would be major changes to the
+language definition and likely to compilers as well. A whole lot larger change
+than that of the language as a whole.
+
+Anyway, either put up or shut up on this one. Either propose a set of changes to
+allow these to be called constraints (and let the rest of us tear them up), or
+stop griping about the name. You did that for "build-in-place" and succeeded in
+changing the mindset, so it can be done.
+
+P.S. If I wasn't the editor, I would set a kill bit on this thread so I didn't
+have to see any more of it.
+
+****************************************************************
+
+From: Bob Duff
+Date: Monday, April 19, 2010 8:26 PM
+
+> This actually makes me angry, because I spent a lot of effort doing...
+
+Please don't be angry about this stuff. It's not good for you.
+
+> Anyway, either put up or shut up on this one.
+
+OK, fair enough.
+
+****************************************************************
+
+From: Bob Duff
+Date: Monday, April 19, 2010 9:11 PM
+
+> Yes, we can all sing in harmony about how much we love full coverage.
+> While we are at it, I would love to solve the problem some day that
+> nested variants always need a "when others" which is logically
+> unnecessary. It would be nice if the discriminant's subtype, when
+> inside a particular variant, effectively had a Predicate expression
+> added that corresponds to the "when Red | Green =>" that started the
+> variant.
+
+Yeah, that's an annoyance, and I support fixing it.
+
+But it's not very important.
+
+****************************************************************
+
+From: Bob Duff
+Date: Wednesday, April 28, 2010 5:33 PM
+
Here's a new version of AI05-0153-1 (subtype predicates), for tomorrow's
discussion.
@@ -3341,5 +4857,152 @@
to. This one has serious resolution issues and I for one don't think that they
can be solved in the general case currently proposed. I left this as I
originally had it.
+
+****************************************************************
+
+From: Bob Duff
+Date: Monday, May 10, 2010 1:56 PM
+
+New version of AI05-0153-1, Subtype predicates, modified as per the April 29
+telephone meeting.
+
+Randy and Steve were given the following homework:
+
+ AI05-0153-1: Check if there are any rules where dynamically changing value
+ sets breaks the language.
+
+I did your homework. ;-) I ended up deciding to go along with Randy and Steve,
+here. It's kind of unintuitive, but it seemed easiest. See the last part of
+the discussion, about validity, for (rather weak) rationale.
+
+If you want to argue against this decision (I expect Tuck to object!), then
+please address the validity issue.
+
+Steve was given the following homework:
+
+ AI05-0153-1: Explain the problem with "contains" for generics, showing
+ examples.
+
+I think I see what Steve was getting at, but I don't think it's a big problem.
+I added some AARM verbiage to clarify the intent. I don't feel strongly about
+this: feel free to propose wording for the opposite choice.
+
+[Editor's Note: This is version /06 of the AI.]
+
+****************************************************************
+
+From: Steve Baird
+Date: Monday, May 10, 2010 2:16 PM
+
+> > Steve was given the following homework:
+> AI05-0153-1: Explain the problem with "contains" for generics, showing
+> examples.
+>
+> ...
+> AARM To Be Honest: "Contains" means physically contains; instances of
+> generic child packages are not included.
+
+This seems adequate, but we could also consider ignoring generics entirely when
+making this "contains" check. This would, in the following case,
+
+ generic
+ type Index is (<>);
+ package G is
+ generic package Nested is end Nested;
+ end G;
+
+ package body G is
+ package body Nested is
+ type Vec is array (Index) of Integer;
+ end Nested;
+ end G;
+
+mean that no runtime check would fail if G were instantiated with a "predicated"
+subtype, but that an instance of G.Nested would fail the AI's check.
+
+The advantage of treating generics uniformly is that it eliminates the need to
+even mention "sprouted" generics; the rule for this odd corner case just falls
+out as a consequence of the more general rule.
+
+I only feel strongly that the rule ought to be well-defined; I don't much care
+which answer we pick.
+
+P.S. Am I now done with my homework, or is more explaining needed?
+
+****************************************************************
+
+From: Bob Duff
+Date: Monday, May 10, 2010 2:57 PM
+
+> This seems adequate, but we could also consider ignoring generics
+> entirely when making this "contains" check.
+
+You mean, like this:
+
+The elaboration of the declaration or body of an instance of a generic unit
+raises Program_Error if any of the following occurs within that declaration or
+body, but not further nested within a generic unit: an index subtype,
+discrete_range of an index_constraint or slice, or a discrete_subtype_definition
+with a user-specified predicate.
+
+?
+
+> This would, in the following case,
+>
+> generic
+> type Index is (<>);
+> package G is
+> generic package Nested is end Nested;
+> end G;
+>
+> package body G is
+> package body Nested is
+> type Vec is array (Index) of Integer;
+> end Nested;
+> end G;
+>
+> mean that no runtime check would fail if G were instantiated with a
+> "predicated" subtype, but that an instance of G.Nested would fail the
+> AI's check.
+
+I guess that's best. Then the compiler needn't walk Instance_Of_G.Nested for
+this check.
+
+> The advantage of treating generics uniformly is that it eliminates the
+> need to even mention "sprouted" generics; the rule for this odd corner
+> case just falls out as a consequence of the more general rule.
+>
+> I only feel strongly that the rule ought to be well-defined; I don't
+> much care which answer we pick.
+
+I agree with that.
+
+> P.S. Am I now done with my homework, or is more explaining needed?
+
+See above. ;-)
+
+****************************************************************
+
+From: Steve Baird
+Date: Monday, May 10, 2010 4:33 PM
+
+...
+> You mean, like this:
+>
+> The elaboration of the declaration or body of an instance of a generic
+> unit raises Program_Error if any of the following occurs within that
+> declaration or body, but not further nested within a generic unit:
+> an index subtype, discrete_range of an index_constraint or slice, or a
+> discrete_subtype_definition with a user-specified predicate.
+>
+> ?
+
+Looks good to me.
+
+>> P.S. Am I now done with my homework, or is more explaining needed?
+>
+> See above. ;-)
+
+I'll take that as a "yes".
****************************************************************
Questions? Ask the ACAA Technical Agent