!standard 3.2.4(0) 10-06-30 AI05-0153-1/07 !class Amendment 09-05-27 !status No Action (10-0-0) 10-10-29 !status work item 09-05-27 !status received 09-05-27 !priority Medium !difficulty Medium !subject Subtype predicates !summary Add subtype predicates to the language. Predicates are checked on every subtype conversion (which includes assignments, most cases of parameter passing, etc), and on all parameter passing. !problem Ada's constraints are a powerful way to enhance the contract of an object (including formal parameters). But the constraints that can be expressed are limited. For instance, it isn't possible to specify that a record type may have any of several discriminant values - for discriminants we can only specify a single value or allow all discriminants. !proposal (See summary.) !wording This AI depends on AI05-0183-1, which defines a syntax for aspect_specifications, which may be attached to declarations. Informal: We define a new aspect "Predicate", which takes a condition (i.e. a BOOLEAN_expression). The condition can use the defining_identifier of the subtype, to mean the "current instance" of the subtype (that is, the object to test the predicate against), as defined in AI05-0183-1. AARM-3.2(1.b/2) says: 1.b/2 Glossary entry: {Subtype} A subtype is a type together with a constraint or null exclusion, which constrains the values of the subtype to satisfy a certain condition. The values of a subtype are a subset of the values of its type. Change it to: 1.b/2 Glossary entry: {Subtype} A subtype is a type together with optional constraints, null exclusions, and predicates, which constrain the values of the subtype to satisfy a certain condition. The values of a subtype are a subset of the values of its type. Add new section 3.2.4: 3.2.4 Subtype Predicates For any subtype, the following language-defined aspect is defined: Subtype_Predicate This aspect shall be specified by an expression. The expected type for the expression is any boolean type. A Subtype_Predicate may be specified on a type_declaration or a subtype_declaration; if none is given, an implicit "with Subtype_Predicate => True" is assumed. Legality Rules Within the expression of a Subtype_Predicate aspect_specification for a composite type C or an access to a composite type C, the only components of C referenced shall be discriminants, and a name that denotes the current instance of the (sub)type shall be used only as a prefix (including a dereference) of a selected_component for a discriminant, or as a prefix (including a dereference) of an attribute_reference with attribute_designator being Length, First, Last, or Range. Static Semantics The /predicate of a subtype/ is defined as follows: - For a (first) subtype defined by a derived type declaration, the specified Subtype_Predicate, and-ed with the predicate of the parent subtype, and-ed with the predicates of any progenitor subtypes. - For a (first) subtype defined by a non-derived type declaration, the specified Subtype_Predicate. - For a subtype created by a subtype_declaration, the specified Subtype_Predicate, and-ed with the predicate of the subtype denoted by the subtype_mark. - For a subtype created by a subtype_indication that is not that of a subtype_declaration, the predicate of the subtype denoted by the subtype_mark. - For a base subtype, True. [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.] Dynamic Semantics 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. AARM Ramification: Predicates are not checked on object creation for elementary types. For composite types, they are checked only if there are default values, and only if those defaults are used. Also, only for explicit defaults -- the implicit default of null for access types doesn't count. Legality Rules An index subtype, discrete_range of an index_constraint or slice, or a discrete_subtype_definition is illegal if it statically denotes a subtype with a user-specified predicate. Dynamic Semantics 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. 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. 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 matches the nominal subtype of the value being checked. AARM Reason: Well-behaved predicates should not have side effects that matter, so omitting the check is pretty harmless. It is possible to write non-well-behaved predicates, which is why the permission is needed. If the implementation does omit a predicate check, it cannot later assume that the predicate was True. NOTE: A Predicate does not cause a subtype to be considered "constrained". NOTE: A Predicate is not necessarily True for all objects of the subtype at all times. Predicates are checked as specified above, but can become False at other times. For example, the Predicate of a record is not checked when a component is modified. [End of 3.2.4.] 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 AARM Ramification: If S has a predicate, S'First in S may evaluate to False. 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): The tested type is not scalar, and the value of the simple_expression satisfies any constraints of the named subtype, {any predicate of the named subtype evaluated to True,} and: Add at the end of 4.6(51/2): 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, {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): For an access type, the formal parameter is initialized from the value of the 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: - Constraints are restricted to certain particular forms (range constraints, discriminant constraints, and so forth), whereas predicates can be arbitrary conditions. - Constraints can only be violated for invalid values, whereas predicates can be violated in various ways (important side effects in predicates, for example, could cause reevaluation of the predicate to get a different answer). However, it is possible to write well-behaved predicates. We don't know how to FORCE the programmer to write well-behaved predicates without being too restrictive. Predicates are similar to type invariants. The differences are: - A type invariant is a requirement on all values of a type outside of the type's defining package(s). That is, invariants are specifically allowed to become False "within the abstraction". - Therefore, invariants are only allowed for private TYPES, whereas predicates are allowed for any SUBtype. --- 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. --- Note that in general, predicates are only known to be True at the point where the language defines the check, so the compiler can't always assume they are True at some later point in the code. However, there are cases where the compiler can usefully deduce such later truths. For example: type Rec is record A : Natural; end record; subtype Decimal_Rec is Rec with Predicate => Rec.A mod 10 = 0; Obj : Decimal_Rec := (A => 10); -- (1) procedure Do_It (P : in out Rec) is begin P.A := 5; end Do_It; Do_It (Obj); -- (2) Put (Obj in Decimal_Rec); -- (3) The predicate on Decimal_Rec will be checked at (1). However, after the call at (2), the predicate is no longer True for Obj. The call at (3) will print False. Such loopholes are unfortunate, but we really have no choice. There is no way to prevent "bad" predicates without being overly restrictive. Compilers may, of course, give warnings about questionable predicates. Note that predicates are no worse than preconditions in this regard. Consider the alternatives: One can already specify predicates in comments, but of course such predicates can be false. Alternatively, one can sprinkle preconditions and pragmas Assert all over the place, but those can be false, too -- for the same reasons predicates can be false, and for the additional reason that one might forget some places to sprinkle. --- We considered allowing implementations to check predicates at places where such 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. 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. A simplified example: type Entity_Kind is (Proc, Func, A_Type, A_Subtype, A_Package, An_Entry); type Symbol_Record (Entity : Entity_Kind) is record ... type Symbol_Ptr is access all Symbol_Record; subtype Type_Symbol_Ptr is not null Symbol_Ptr with Predicate => Type_Symbol_Ptr.Entity = A_Type; subtype Callable_Symbol_Ptr is not null Symbol_Ptr with Predicate => Callable_Symbol_Ptr.Entity = Proc or Callable_Symbol_Ptr.Entity = Func or Callable_Symbol_Ptr.Entity = An_Entry; function Type_Size (A_Type : Type_Symbol_Ptr) return Size_Type; procedure Generate_Call_Parameters (Callee : Callable_Symbol_Ptr; ...); 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. Other examples of useful predicates: If you plan to divide by X, its subtype should exclude zero. An OS interface requires a size-in-bytes, but it must be a multiple of the page size. Ada measures sizes in bits, but it's sometimes necessary to measure in storage units. "Predicate => Blah mod System.Storage_Unit = 0" might come in handy. A Sort function produces an array (or other sequence) of subtype Sorted_Sequence. Binary_Search takes a parameter of that subtype. Very useful to keep track of which objects have been sorted (can I pass this to Binary_Search, or must I sort it first?). To prevent SQL injection bugs, keep track of which data is "tainted" and which is "trusted", using predicates. In a program that processes objects through multiple phases, you want to keep track of which phase(s) have been applied to each object, via subtypes. Temporal logic: you can't land the airplane until the wheels are down. So Land_Airplane takes a parameter of subtype Airplane_That_Is_Ready_To_Land, which is a subtype of Airplane. --!corrigendum 3.2.2(2) !ACATS test Add ACATS B and C tests for this feature. !appendix This AI was created after discussion at the Tallahassee ARG meeting; it is partially based on an old idea found in AC-0157. From the Tallahassee minutes about type Invariants: Randy asks whether the user-defined constraint idea is worth looking at (either as an alternative or replacement). After discussion, we decide that it seems to solve a somewhat different problem - it allows adding contracts to particular parameters, objects, etc. User-defined constraints would be a way to deal with non-contiguous sets of discriminants, one-sided array constraints, and so on. There is sufficient interest to have that written up (it previously was discussed on Ada-Comment and filed as AC-0157). It's not very necessary on scalar types, so if the rules get too messy for them, don't allow them. (Randy notes when writing up these minutes that that would probably be a generic contract problem.) Steve notes that it would need a bounded error if the expression does not return the same value when called with the same value (we would want to be able to eliminate duplicate checks) -- the bounds are that the check is either made or not. **************************************************************** From: Randy Brukardt Date: Wednesday, May 20, 2009 5:28 PM At the last meeting, I was directed to write a proposal about user-defined constraints. I was told to try to restrict them only to composite types, because the "satisfability" rules would be hard to make work for scalar types, while they are pretty much right for composite types already. To do that brings up a generic contract model issue. We would need to use an assume-the-worst rule for generic bodies. Essentially, any subtype that is of a generic formal type (or a type derived from such a type) could not have a user-defined constraint (since we don't allow reconstraining or use on types that might not be composite). It would be possible to move those constraints to the private part, however. Is the latter workaround enough? It seems like it would be to me (it is the same workaround we suggest for 'Access, for instance), but I wanted to get other people's opinions on that before I spend a lot of effort writing up the proposal. (I was going to ask the accessibility subcommittee in one of our periodic calls, but we never got to it.) **************************************************************** From: Randy Brukardt Date: Wednesday, May 27, 2009 11:59 PM Here is a more fundamental question about user-defined constraints: Do they act like real constraints (that is, they apply to the view during the entire time of its existence) or do they only apply at the point that the language defines subtype conversions? If they act like real constraints, then they can only depend on bounds and discriminants; that seems very limiting. (Only bounds and discriminants have the necessary rules to prevent changes between checks.) If they are just checks applied at particular points, then we have anomalies where "constrained" values does not satisfy the constraint. Moreover, whether or not Constraint_Error is raised can depend on the parameter passing mode: type Rec is record A : Natural; end record; subtype Decimal_Rec is Rec when Rec.A mod 10 = 0; Obj : Decimal_Rec := (A => 10); procedure Do_It (P : in out Decimal_Rec) is begin P.A := 5; end Do_It; Do_It (Obj); -- (1) The call at (1) will raise Constraint_Error if Obj is passed by copy: the copy back will fail the subtype conversion back to the original object. But if Obj is passed by reference, the view conversion will succeed and there will not be any check after the call. I was considering only allowing these constraints on private types, but that is uncomfortable for two reasons (1) you lose capability when you see the full type [note however that this is the same rule implied for type invariants: they can only be given for a private type]; (2) it still allows the body (anywhere in the scope of the full declaration, in fact) to break the constraint. package Pack is type Priv is private; function Is_Decimal (P : Priv) return Boolean; function Decimal (N : Natural) return Priv; procedure Half (P : in out Priv); private type Priv is record A : Natural; end record; end Pack; package body Pack is function Is_Decimal (P : Priv) return Boolean is begin return P.A mod 10 = 0; end Is_Decimal; function Decimal (N : Natural) return Priv is begin return (A => N*10); end Decimal; procedure Half (P : in out Priv) is begin P.A := P.A / 2; end Half; end Pack; with Pack; procedure Test2 is subtype Decimal_Priv is Pack.Priv when Pack.Is_Decimal (Decimal_Priv); Obj : Decimal_Priv := Pack.Decimal(1); begin Pack.Half (Obj); -- (2) end Test2; (2) is very much like (1); the user constraint is only checked on return if Priv is passed by copy. So Obj most likely does not meet its constraint after the call to Pack.Half. We could probably fix this particular problem with some additional checking rule on "in out" and "out" parameters, but I worry that this is just the camel's nose -- it might turn into a mess of creeping additional run-time checks (especially once Steve starting thinking about it). I originally ran across this issue thinking about the limitations of access types constrained by user-defined constraints. But eventually I realized that the issue was pretty general -- it's not just a problem with designated objects of access types. So what do you all think? Should I write this up: (1) Allowing these to apply only to bounds and discriminants? (The issues with those are well-understood, of course.) (2) Allowing these to apply only to private types, with suitable additional checks defined on the return from the "defining subsystem" (the package containing the private type and its subsystem). The constraints would not meaningfully apply within the defining subsystem (it would be easy to change an object after the check). (3) Combining (1) and (2). (4) Neither (1) nor (2). (a) I've got a better idea; (b) don't bother. **************************************************************** From: Micronian Date: Tuesday, June 9, 2009 7:13 PM I just read this AI and think it is an interesting proposal. One minor thing I was wondering about is what was the reason for deciding on using "when" rather than something like "requiring"? Personally, I find a keyword such as "requiring" to be much more clearer and gives a stronger emphasis than a strange use of "when". Example: subtype My_Int is Integer when (My_Int mod 2 = 0); versus subtype My_Int is Integer requiring (My_Int mod 2 = 0); When I see "requiring" I immediately get that unmistakable "ok I should be careful how I use this" feeling. Just curious. **************************************************************** From: Martin Dowie Date: Wednesday, June 17, 2009 2:10 PM Probably because it's an existing keyword => no one will be using it as an identifier => no upwards compatibility issues. E.g. procedure Was_Valid is Requiring : Boolean := ...; -- oops!! begin if Requiring then ... **************************************************************** From: Adam Beneschan Date: Wednesday, June 17, 2009 2:34 PM Yuck! Requiring *what*? This name (a present participle with a missing object) seems like a ghastly name for a variable, worse even than Overriding. I understand the compatibility issue, but the language designers have seen fit to add keywords after convincing themselves that the words are unlikely enough to be used as identifiers that it won't cause any problems---and I'd guess that Requiring is a much less likely name for an identifier than any of Overriding, Synchronized, or Interface. I think Micronian has a good point here. **************************************************************** From: Martin Dowie Date: Wednesday, June 17, 2009 2:48 PM Yup, it would be a horrible choice of name in that situation. You could come up with examples where it might made more sense, e.g. perhaps as the discriminant in a variant record indicating what variant is required. Not matter - it was just a suggestion as to why 'when' might have been picked over a new keyword. Personally, I have no objections to new keywords - if I make the decision to 'upgrade' to a new language standard with a new keyword then that's my choice. Find/Replace tools are two-a-penny these days. **************************************************************** From: Bob Duff Date: Wednesday, June 17, 2009 2:47 PM > Probably because it's an existing keyword => no one will be using it > as an identifier => no upwards compatibility issues. Exactly. It is possible to add new reserved words in really important cases, but we should not do so lightly. In this case, "when" works OK -- it means "when X is true, the value is in this subtype". Any language-change proposal that adds a new reserved word is harder to get approved. And that's as it should be. **************************************************************** From: Randy Brukardt Date: Wednesday, June 17, 2009 2:52 PM Guys, we don't have a clue at this point if we can even get the semantics of this to work out (initial returns don't look good); arguing about the syntax is wildly premature. For now, we are not planning to add any new keywords in Amendment 2. That could change of course, but this is supposed to be a modest update, and loads of new syntax would look more than "modest". **************************************************************** From: Stephen Leake Date: Wednesday, June 17, 2009 4:03 PM > It is possible to add new reserved words in really important cases, > but we should not do so lightly. In this case, "when" works OK -- it > means "when X is true, the value is in this subtype". I'd rather see 'with': subtype My_Int is Integer with (My_Int mod 2 = 0); as in "with this additional constraint". > Any language-change proposal that adds a new reserved word is harder > to get approved. And that's as it should be. Yes. And I get Randy's point about getting the semantics right first, but I just couldn't resist :). **************************************************************** From: Christoph Grein Date: Thursday, June 18, 2009 5:01 AM > and I'd guess that Requiring is a much less likely name for an > identifier than any of Overriding, Synchronized, or Interface. I was bitten by Interface. But not a big deal to invent new names (eg. ABC_Interface for some ABC equipment). **************************************************************** From: Dmitry A. Kazakov Date: Thursday, June 18, 2009 5:28 AM It is unclear to me what is the reason to introduce reserved keywords when there is no syntactic necessity. In fact, only few reserved keywords are really need to be reserved. **************************************************************** From: Bob Duff Date: Thursday, June 18, 2009 7:38 AM The ARG has considered several times the idea of having non-reserved keywords in the syntax. I think it's a good idea, but many people think it's an abomination. **************************************************************** From: Steve Baird Date: Friday, June 19, 2009 7:15 PM At the Brest meeting, Randy and I were tasked with exploring two different approaches to this AI. The difference was only in finding the appropriate wording to capture the intention of the AI. Irrelevant detail for those who are curious: As I understand it (Randy - speak up if I am incorrectly stating your position), Randy advocates viewing the user-defined predicate as a "constraint" in the technical sense of the word; I felt that too much RM upheaval would result if a subtype such as subtype Nul_Terminated_String is String when (String'Length/= 0 and then String (String'Last) = Character'First); were defined to have a constraint. It was reminiscent of the idea introduced in AI05-57 that "an unconstrained type may have a non-null constraint". After thinking about this problem a little bit, I would like to back up and reexamine the intention of the AI before diving into the details of wording. The generality of the mechanism described in the AI leads to implementation problems. I would like to consider adding a restriction that the predicate may only reference discriminants and array bounds, at least if the type in question is not scalar. Consider the Nul_Terminated_String example given above (and let's not worry at this point about whether the reference to String'Last is confusing). We pass an actual of this subtype (by reference) to a procedure which takes an in-out mode formal parameter of subtype String; the procedure assigns the character 'X' to the last element of the array. A constraint check after the procedure returns might discover the problem, but it is too late: the object has been corrupted. If subcomponent modification is allowed, things get messy fairly quickly. An approach which was discussed in Brest would be to require that all objects of this subtype must be constant. This eliminates the problem of subcomponent modification, but it means that attempting the use of of these subtypes as either a component subtype or as an actual parameter in an instantiation would have to be either illegal or subject to some ugly restrictions. The current language design works because array bounds are never mutable and discriminant values are never mutable for a constrained object. Similarly, a user-defined constraint which only depends on array bounds and discriminant values could be made to work. I think we should give up on the generality of the Nul_Terminated_String example and impose these restrictions in order to get to something that we know how to implement. This would still allow the two most important uses for this construct: non-contiguous discriminant constraints and low-bound-only constraints for arrays. Does this seem reasonable? Other questions include: 1) What about scalars? Do we want to support something like subtype Power_Of_Two is Positive when Positive = 1 or else (Positive mod 2 = 0 and then Positive / 2 in Power_Of_Two); 2) Do we really want to use the name of the subtype being "constrained" to denote the value in the predicate as the AI suggests, or would it be better to use the name of the subtype being defined? That would complicate recursive membership tests as in the Power_Of_Two example above. Perhaps Subtype_Name'Some_Attribute? 3) If someone doesn't play by the rules, as in subtype Future is Calendar.Day_Duration when Day_Duration > Calendar.Seconds (Calendar.Clock); , must this be rejected at compile time, or is this just erroneous? 4) Is there a constraint check associated with object initialization for an object of one of these subtypes? Perhaps only for non-scalars? For the following example, X : Some_Subtype; Y : Boolean := X in Some_Subtype; the current language design ensures that Y is True if Some_Subtype is non-scalar (ignoring privacy). I'd like to get these questions resolved before I worry about wording. **************************************************************** From: Steve Baird Date: Sunday, June 21, 2009 1:01 PM > 1) What about scalars? Do we want to support something like > subtype Power_Of_Two is Positive when Positive = 1 > or else > (Positive mod 2 = 0 and then Positive / 2 in > Power_Of_Two); > Answering my own question, I don't see a good approach for scalars. First and Last attribute values, for-loops (for discretes), and array indexing (for discretes) would all pose problems. Assuming Standard.Integer is is a 32-bit type, would X : array (Power_Of_Two) of My_Task_Type; declare 31 tasks? Would Power_Of_Two'Last equal 2 ** 30? This does not sound like a good idea. **************************************************************** From: Tucker Taft Date: Sunday, June 21, 2009 4:25 PM My recommended syntax would be: subtype Even is Integer with Predicate => Even mod 2 = 0; I don't see the need to invent yet another syntax now that we have begun to get comfortable with the "aspect specification" syntax: with => {, => }; I think we should avoid the term "constraint" because it already has too many connotations in Ada. I think if we see this as the "Predicate aspect" of the subtype, then we can piggy-back on the syntax and a lot of the semantics for aspects. I think we clearly want to use the newly defined subtype rather than the old subtype in the expression to represent the value. Your point about allowing the "predicate" to depend only on the bounds/discriminants of a composite type seems reasonable. Our idea of restricting it to constants does seem to create significant generic contract problems. For a scalar type, there seems no harm in having it depend on the value. The checking only need be performed on assignment or similar operations, and seems to impose no contract model problems. For access types, there are the usual problems if we allow it to depend on the pointed-to value, since that could be changed through some other access path, so I wouldn't allow a Predicate as part of an access subtype declaration, or we have to make all the same restrictions as we have now for access subtype constraints, and it would only be for access-to-composite. If we are going to enforce a requirement that the predicate for a composite type depend only on its discriminants/bounds, I would think we could also require that it involve only constants and pure functions. I would certainly require a predicate check when a composite object is initialized, by default or by an initial expression. **************************************************************** From: Tucker Taft Date: Sunday, June 21, 2009 4:32 PM I'm not really convinced by these concerns. We already have subtypes, albeit weird ones, where 'Last is not an element of the subtype. Even "not null" has some weirdness, given that the default value of the [sub]type doesn't satisfy the null exclusion. By the way, I would not allow recursion in these Predicates. I think a reasonable freezing rule should prevent it, especially if the subtype being defined refers to the current instance, rather than to itself. **************************************************************** From: Steve Baird Date: Monday, June 22, 2009 9:46 AM > My recommended syntax would be: > > subtype Even is Integer > with Predicate => Even mod 2 = 0; > > I don't see the need to invent yet another syntax now that we have > begun to get comfortable with the "aspect specification" syntax: > > with => {, => }; Good point. I agree. > I think we should avoid the term "constraint" > because it already has too many connotations in Ada. I think if we > see this as the "Predicate aspect" of the subtype, then we can > piggy-back on the syntax and a lot of the semantics for aspects. Agreed. > I think we clearly want to use the newly defined subtype rather than > the old subtype in the expression to represent the value. Agreed. > Your point about allowing the "predicate" to > depend only on the bounds/discriminants of a > composite type seems reasonable. Our idea of > restricting it to constants does seem to > create significant generic contract problems. Agreed. > For a scalar type, there seems no harm in having > it depend on the value. The checking only need > be performed on assignment or similar operations, > and seems to impose no contract model problems. What rules do you suggest for the problematic cases that I mentioned: 'First, 'Last, 'Succ, 'Pred, etc. use of the subtype in a for-loop use of the subtype as an array index subtype ? One possible answer is that the predicate is ignored in these cases. It participates in subtype conversion constraint checking and in membership tests and is ignored elsewhere (dynamically - statically it would participate at least in conformance checking and probably in the definition of a static subtype). I think this would be too confusing; simply disallowing predicates for scalars would be preferable to this solution. Given the following example for I in S loop if I not in S then Foo; end if; end if; , I think it would be very odd if Foo were called. Allowing an array element which is effectively unnameable (because attempts to index it fail a subtype conversions constraint check) also seems like a bad idea to me. > For access types, there are the usual problems > if we allow it to depend on the pointed-to value, > since that could be changed through some other > access path, so I wouldn't allow a Predicate > as part of an access subtype declaration, or > we have to make all the same restrictions as > we have now for access subtype constraints, > and it would only be for access-to-composite. Agreed. > If we are going to enforce a requirement that > the predicate for a composite type depend only > on its discriminants/bounds, I would think we > could also require that it involve only > constants and pure functions. Sounds good to me. Anytime you have a rule that depends on constancy, you have to give some thought to the case of a constant that ends up being modified (e.g., via a finalization routine), but let's ignore that for now. > I would certainly require a predicate check > when a composite object is initialized, > by default or by an initial expression. Agreed. We can discuss the rules for scalars in this case after we have decided whether predicates for scalar subtypes should be completely abandoned. > By the way, I would not allow recursion in these > Predicates. I think a reasonable freezing rule > should prevent it, especially if the subtype being > defined refers to the current instance, rather than > to itself. Right. If the name of the subtype denotes the current instance, then there is no way to use it as a subtype name, so that problem goes away. If a pure function is called in the predicate expression, that function could, of course, be recursive. **************************************************************** From: Tucker Taft Date: Monday, June 22, 2009 10:21 AM > What rules do you suggest for the problematic cases that I mentioned: > 'First, 'Last, 'Succ, 'Pred, etc. > use of the subtype in a for-loop > use of the subtype as an array index subtype All good questions. 'Succ and 'Pred are unrelated to subtypes in general, and S'Succ can be applied to any value of the underlying type. 'First and 'Last are more interesting. One possibility would be to require that S'First and S'Last satisfy the predicate. That would at least help a bit. > One possible answer is that the predicate is ignored in these cases. > It participates in subtype conversion constraint checking and in > membership tests and is ignored elsewhere (dynamically - statically it > would participate at least in conformance checking and probably in the > definition of a static subtype). > > I think this would be too confusing; simply disallowing predicates for > scalars would be preferable to this solution. > > Given the following example > for I in S loop > if I not in S then > Foo; > end if; > end if; > , I think it would be very odd if Foo were called. Perhaps. But what about "for I in S'Range loop"? Would that be different? And what about "for I in S range S'Range loop"? We could limit where these subtypes are used, and use the old "raise Program_Error" trick to avoid generic contract model problems. Alternatively, we could disallow such subtypes as generic actual subtypes, unless the formal has, say, "with Predicate => <>". And then, of course, the formal would face the same restrictions as any subtype with a Predicate. Clearly the main goal would be to use them in parameter and result subtypes. For example, I could imagine something like: subtype Non_Zero is Integer with Predicate => Non_Zero /= 0; and use that for parameters when you are going to be using them as a divisor. It seems a lot nicer to simply use "Non_Zero" or "Non_Zero range -5..5" rather than having to add preconditions and/or postconditions on subprograms just for this relatively common restriction. If I can't use these in "for loops" and for array index subtypes, I don't see that as a big limitation. I do think it makes sense to require 'First and 'Last of a subtype to satisfy the subtype's predicate. > Allowing an array element which is effectively unnameable (because > attempts to index it fail a subtype conversions constraint check) also > seems like a bad idea to me. You have convinced me we should disallow them as index subtypes and in for loops. I don't want to get into the holey-enumeration pain with these. **************************************************************** From: Tucker Taft Date: Monday, June 22, 2009 10:39 AM We also should disallow such subtypes as a choice in a case/variant alternative, to avoid any confusion. **************************************************************** From: Jean-Pierre Rosen Date: Monday, June 22, 2009 11:02 AM >>> I think this would be too confusing; simply disallowing predicates >>> for scalars would be preferable to this solution. Totally disallowing predicates for scalar subtype would disapoint many people, but we could maybe allow them only for variables: Even : Integer with Even/2 = 0; (OK, we should slightly change the rule about where the variable's name becomes available). **************************************************************** From: Bob Duff Date: Monday, June 22, 2009 11:10 AM > I think this would be too confusing; simply disallowing predicates for > scalars would be preferable to this solution. I'll reply to the various e-mails in more detail later, but right now I want to say: It would be a real shame to disallow scalars! I think the primary use of this feature will be for making arbitrary subsets of enumeration types. And use these for parameter subtypes, function returns, local vars, discriminants, and record components. Letting 'for' loop oddities get in the way of these would be a shame. It's so frustrating when a programmer says "How come I can't add 2 plus 2 in Ada", and as a language lawyer, I'm forced to say, "Because in a generic discriminanted select statement, a requeue might blah blah blah." And the programmer says, I don't WANT no stinkin' discriminated requeue blah... -- I just want to add 2+2! For example, in GNAT we have (some comments removed): type Entity_Kind is ( E_Void, E_Component, E_Constant, E_Discriminant, E_Loop_Parameter, E_Variable, ... -- dozens more ); ... subtype Overloadable_Kind is Entity_Kind range E_Enumeration_Literal .. -- E_Function -- E_Operator -- E_Procedure E_Entry; ...many similar subtypes It's a kludge that (e.g.) Overloadable_Kind has to be defined partly in comments, because Entity_Kind is conceptually unordered. And it's a maintenance hazard. More importantly, we can't define arbitrary subsets of Entity_Kind. I also very badly want to be able to say things like: type Entity (Kind : Entity_Kind) is private; subtype Overloadable_Entity is new Entity with Predicate => Overloadable_Entity.Kind in Overloadable_Kind; These are the uses I have in mind. Things like Prime_Integer and Even_Integer are nothing but interesting curiosities by comparison. Nonzero_Integer might be useful occassionally, but I don't divide that often, so ... ("I'm a uniter, not a divider." ;-) ) If we drop scalars, I'm (almost?) inclined to drop the whole proposal -- not sure about that. **************************************************************** From: Bob Duff Date: Monday, June 22, 2009 11:14 AM > We also should disallow such subtypes as a choice in a case/variant > alternative, to avoid any confusion. I see what you mean, but it seems a shame. Hmm... **************************************************************** From: Robert Dewar Date: Monday, June 22, 2009 11:21 AM > It would be a real shame to disallow scalars! > > I think the primary use of this feature will be for making arbitrary > subsets of enumeration types. And use these for parameter subtypes, > function returns, local vars, discriminants, and record components. I agree entirely on both points > Letting 'for' loop oddities get in the way of these would be a shame. > It's so frustrating when a programmer says "How come I can't add 2 > plus 2 in Ada", and as a language lawyer, I'm forced to say, "Because > in a generic discriminanted select statement, a requeue might blah > blah blah." And the programmer says, I don't WANT no stinkin' > discriminated requeue blah... -- I just want to add 2+2! > > For example, in GNAT we have (some comments removed): > > type Entity_Kind is ( > E_Void, > > E_Component, > E_Constant, > E_Discriminant, > E_Loop_Parameter, > E_Variable, > > ... -- dozens more > ); > > ... > subtype Overloadable_Kind is Entity_Kind range > E_Enumeration_Literal .. > -- E_Function > -- E_Operator > -- E_Procedure > E_Entry; > > ...many similar subtypes > > It's a kludge that (e.g.) Overloadable_Kind has to be defined partly > in comments, because Entity_Kind is conceptually unordered. And it's > a maintenance hazard. More importantly, we can't define arbitrary > subsets of Entity_Kind. > > I also very badly want to be able to say things like: > > type Entity (Kind : Entity_Kind) is private; > > subtype Overloadable_Entity is new Entity > with Predicate => Overloadable_Entity.Kind in Overloadable_Kind; > > These are the uses I have in mind. Things like Prime_Integer and > Even_Integer are nothing but interesting curiosities by comparison. > Nonzero_Integer might be useful occassionally, but I don't divide that > often, so ... ("I'm a uniter, not a divider." ;-) ) I agree, basically my only interest in this feature is for scalars for the type of programming I do! **************************************************************** From: Robert Dewar Date: Monday, June 22, 2009 11:22 AM > I see what you mean, but it seems a shame. Hmm... Indeed, a real shame, enough for me to think, back to square 1 to rethink! **************************************************************** From: Steve Baird Date: Monday, June 22, 2009 11:50 AM >> What rules do you suggest for the problematic cases that I mentioned: >> 'First, 'Last, 'Succ, 'Pred, etc. >> use of the subtype in a for-loop >> use of the subtype as an array index subtype > > All good questions. 'Succ and 'Pred are unrelated to subtypes in > general, and S'Succ can be applied to any value of the underlying > type. Good point. > 'First and 'Last > are more interesting. One possibility would be to require that > S'First and S'Last satisfy the predicate. That would at least help a > bit. >> ? Do you mean a runtime check at the point of the subtype declaration? This would mean that your earlier example subtype Even is Integer with Predicate => Even mod 2 = 0; would not elaborate successfully. Or do you mean that the implementation generates a loop when evaluating S'First or S'Last at some point, looking for the least/greatest value in the subtype being constrained (i.e., the subtype named by the subtype_mark in the declaration of S) which satisfies the predicate (with appropriate rules to cope with the case where no such value is found)? >> Given the following example >> for I in S loop >> if I not in S then >> Foo; >> end if; >> end if; >> , I think it would be very odd if Foo were called. > > Perhaps. But what about "for I in S'Range loop"? > Would that be different? And what about "for I in S range S'Range > loop"? Let's ignore reals for a moment and focus on discretes. (Although subtype Positive_Float is Float range 0.0 .. Float'Last with predicate Positive_Float /= 0.0; does make me wonder about the value of Positive_Float'First). A subtype defines a subset of the set of values of the basetype. If an existing subtype is referenced via the subtype_mark in a subtype_indication, then the set of values associated with the subtype defined by the subtype_indication is a subset of the set of values associated with that existing subtype. This can lead to a conjunction of multiple predicates. The same ideas apply for reals, but specifying the set of values associated with a real subtype requires a bit more care. Thus, I would think that if S is a subtype with an associated predicate, then S'Range might include values that are not in S (i.e. values for which the predicate is False). On the other hand, S range S'Range would, I imagine, be synonymous with S. > We could limit where these subtypes are used, and use the old "raise > Program_Error" trick to avoid generic contract model problems. > Alternatively, we could disallow such subtypes as generic actual > subtypes, unless the formal has, say, "with Predicate => <>". > And then, of course, the formal would face the same restrictions as > any subtype with a Predicate. I agree that either of these approaches would work. I prefer the latter. This is only an issue for Formal_Discrete, Formal_Signed_Integer, and Formal_Modular types, right? I'm not aware of any problems in the float or fixed cases. > Clearly the main goal would be to use them in parameter and result > subtypes. I completely agree that scalar subtypes with predicates could be very useful. You don't have to convince me of that. I'm just concerned about some of the language interactions that have nothing to do with the primary motivation that you mentioned, but that would nonetheless be introduced. Disallowing these subtypes in contexts where we really rely on having a contiguous range (don't forget entry families!), sounds like a promising approach. > You have convinced me we should disallow them as index subtypes and in > for loops. I don't want to get into the holey-enumeration pain with > these. Agreed. These subtypes are somewhat like what you would get if dynamic expressions in enumeration representation clauses were allowed. **************************************************************** From: Steve Baird Date: Monday, June 22, 2009 12:09 PM > We also should disallow such subtypes as a choice in a case/variant > alternative, to avoid any confusion. Agreed. We haven't discussed how this feature interacts with the definition of "static subtype", but I was assuming that a subtype with an associated predicate is never a static subtype. That would address this issue, right? **************************************************************** From: Steve Baird Date: Monday, June 22, 2009 11:56 AM > If we drop scalars, I'm (almost?) inclined to drop the whole proposal > -- not sure about that. I completely agree that scalars are an important case. It's just a question of whether we can get them to work. It sounds like Tuck's "just don't allow these guys where they cause problems" approach may get us out of the woods here. **************************************************************** From: Stephen Michell Date: Monday, June 22, 2009 12:13 PM I am concerned that this proposal is further complicating the language by effectively adding another complete set of per-object constraints for elementary types. Why are we considering putting it on an arbitrary subtype, and not just the first named subtype (i.e. type T is new TT? **************************************************************** From: Steve Baird Date: Monday, June 22, 2009 12:52 PM > We also should disallow such subtypes as a choice in a case/variant > alternative, to avoid any confusion. Ditto for cases where staticness is not required? I'm thinking of a one-choice array aggregate and slice bounds. **************************************************************** From: Edmond Schonberg Date: Monday, June 22, 2009 12:52 PM >I think the primary use of this feature will be for making arbitrary subsets of >enumeration types. And use these for parameter subtypes, function returns, >local vars, discriminants, and record components. A natural way of expressing such constraints would be with our new membership test: subype Overloadable_Kind is Entity_Kind with predicate => Overloadable_Kind in (E_Enumeration_Literal, E_Function, E_Procedure, E_Entry) **************************************************************** From: Steve Baird Date: Monday, June 22, 2009 1:19 PM I said earlier that I was assuming that a subtype with an associated predicate would never be a static subtype. It sounds like that assumption may need to be revisited, and that noncontiguous static subtypes may need to be a fundamental part of this feature. Without getting into the details of how this might be accomplished, does it seem like this approach might salvage the situation? **************************************************************** From: Steve Baird Date: Monday, June 22, 2009 1:40 PM > I am concerned that this proposal is further complicating the language > by effectively adding another complete set of per-object constraints > for elementary types. Why are we considering putting it on an > arbitrary subtype, and not just the first named subtype (i.e. type T is new TT? I don't see the motivation for this; what problem would this restriction solve? If a user wants to write something like subtype Speckled_Foo is Foo with Predicate => Is_Speckled (Speckled_Foo); function Make_Speckled_Record (Kind : Speckled_Foo) return Some_Record; , it seems that a requirement that Speckled_Foo must be declared as a derived type rather than a subtype would only make things a bit more awkward. **************************************************************** From: Bob Duff Date: Monday, June 22, 2009 1:56 PM > I am concerned that this proposal is further complicating the language > by effectively adding another complete set of per-object constraints > for elementary types. Why are we considering putting it on an > arbitrary subtype, and not just the first named subtype (i.e. type T is new TT? Did you see my Entity_Kind example? And then how I used that to constrain a discriminant? (I'm not sure if my message got sent out yet.) I think that example illustrates why you want these "predicates" on pretty-much any subtype. It would be next to useless otherwise. Anyway, if "predicates" are analogous to "constraints", then clearly they belong in the same places -- the whole point of this feature is to generalize the concept of "constraint" to allow arbitrary Boolean expressions, instead of the meager range constraints and discrim constraints we already have. (Constraining discriminants to a single value instead of a subrange (or better, arbitrary subset) has always seemed like an annoying restriction to me). Example: Natural makes sense as a subtype of Integer. So of course Non_Zero makes sense as a subtype of Integer -- it would be annoying to require a new type. **************************************************************** From: Tucker Taft Date: Monday, June 22, 2009 2:05 PM Allowing such a predicate only on a first subtype defeats the purpose of it representing a *subset* of some type. We have a separate proposal for a type "invariant" which is true for *all* values of the type, but that is for private types, and is only true *outside* the package. The idea of a "predicate" is that different subtypes of the same type have different predicates, and thereby represent different subsets of the same type. **************************************************************** From: Bob Duff Date: Monday, June 22, 2009 2:03 PM > , it seems that a requirement that Speckled_Foo must be declared as a > derived type rather than a subtype would only make things a bit more > awkward. Right. As an aside, you'd want "return Speckled_Record" above, so the information doesn't get lost across calls -- could be helpful in proofs. **************************************************************** From: Steve Baird Date: Monday, June 22, 2009 2:39 PM I thought of that, but I wanted to keep the size of the example down. **************************************************************** From: Tucker Taft Date: Monday, June 22, 2009 1:57 PM >> 'First and 'Last >> are more interesting. One possibility would be to require that >> S'First and S'Last satisfy the predicate. That would at least help a >> bit. >>> ? > > Do you mean a runtime check at the point of the subtype declaration? Yes. > > This would mean that your earlier example > subtype Even is Integer > with Predicate => Even mod 2 = 0; would not elaborate > successfully. Good point, so it would have to be: subtype Even is Integer range -2**31 .. +2**31-2 with Predicate => Even mod 2 = 0; > > Or do you mean that the implementation generates a loop when > evaluating S'First or S'Last at some point, looking for the > least/greatest value in the subtype being constrained (i.e., the > subtype named by the subtype_mark in the declaration of S) which > satisfies the predicate (with appropriate rules to cope with the case > where no such value is found)? Heaven forbid. I would hope that the dynamic semantics are identical to those for the underlying subtype except for some addition checks performed at strategic points. I really don't want any fancy new dynamic semantics that imply adding implicit loops or other kinds of control flow. >>> Given the following example >>> for I in S loop >>> if I not in S then >>> Foo; >>> end if; >>> end if; >>> , I think it would be very odd if Foo were called. >> >> Perhaps. But what about "for I in S'Range loop"? >> Would that be different? And what about "for I in S range S'Range >> loop"? >> > > Let's ignore reals for a moment and focus on discretes. > (Although > subtype Positive_Float is Float range 0.0 .. Float'Last > with predicate Positive_Float /= 0.0; does make me wonder about > the value of Positive_Float'First). This would raise Constraint_Error based on the suggested rule that you check that 'First satisfies the predicate. > A subtype defines a subset of the set of values of the basetype. > > If an existing subtype is referenced via the subtype_mark in a > subtype_indication, then the set of values associated with the subtype > defined by the subtype_indication is a subset of the set of values > associated with that existing subtype. > This can lead to a conjunction of multiple predicates. > > The same ideas apply for reals, but specifying the set of values > associated with a real subtype requires a bit more care. I don't see the problem if you don't try to magically figure out 'First or 'Last, but simply require that you get a Constraint_Error if they don't satisfy the predicate. > Thus, I would think that if S is a subtype with an associated > predicate, then S'Range might include values that are not in S (i.e. > values for which the predicate is False). > > On the other hand, > S range S'Range > would, I imagine, be synonymous with S. Agreed, though admittedly a bit confusing. **************************************************************** From: Bob Duff Date: Monday, June 22, 2009 2:00 PM > Indeed, a real shame, enough for me to think, back to square 1 to > rethink! Yeah, that's what I meant by "Hmm...". ;-) > A natural way of expressing such constraints would be with our new > membership test: > > subype Overloadable_Kind is Entity_Kind with > predicate => Overloadable_Kind in (E_Enumeration_Literal, > E_Function, E_Procedure, E_Entry) Yeah, maybe that's part of the solution. Can somebody remind me which AI that is, s'il vous plait? **************************************************************** From: Tucker Taft Date: Monday, June 22, 2009 2:02 PM Good point -- these guys are non-static. I suppose we could go further and allow a very specific form to be static: subtype S is [range ] with Predicate => S in ; where "" is whatever syntax we adopt for representing a sequence of values (e.g. "(3|5|7..9)"). These would still be verboten at least for index subtypes. Using in "for loops" is a separate discussion, but clearly you would want to allow them in case statements if static, since that is the point. **************************************************************** From: Steve Baird Date: Monday, June 22, 2009 2:25 PM > Heaven forbid. I would hope that the dynamic semantics are identical > to those for the underlying subtype except for some addition checks > performed at strategic points. > I really don't want any fancy new dynamic semantics that imply adding > implicit loops or other kinds of control flow. I completely agree. I was just trying to come up with a rule that I could reconcile with the successful elaboration of the original "Even" example. **************************************************************** From: Edmond Schonberg Date: Monday, June 22, 2009 2:41 PM > Yeah, maybe that's part of the solution. Can somebody remind me which > AI that is, s'il vous plait? Its AI05-0158: Generalizing membership tests. Much discussion about syntax at the ARG meeting, no consensus on whether it should be usable in loops, but agreement about intent. **************************************************************** From: Tucker Taft Date: Monday, June 22, 2009 2:42 PM It sounds like we are moving toward some kind of common view here, thanks in part to your throwing up some scary straw men along the way... ;-) **************************************************************** From: Robert Dewar Date: Monday, June 22, 2009 3:13 PM > These would still be verboten at least for index subtypes. > Using in "for loops" is a separate discussion, but clearly you would > want to allow them in case statements if static, since that is the > point. Yes indeed, they really must work in case statements if all the choices are static. **************************************************************** From: Bob Duff Date: Monday, June 22, 2009 4:52 PM > Its AI05-0158: Generalizing membership tests. Thanks. I'll read it when I'm done with my current high-prio AdaCore ticket (or while I'm waiting for builds). >...Much discussion about > syntax at the ARG meeting, no consensus on whether it should be usable >in loops, but agreement about intent. Good to know -- I like the "intent", too. I think I think it should be allowed in loops. Seems very useful for enums. I just did this at a 'csh' prompt: foreach i (blha indf a) ? echo $i ? end blha indf a Don't tell anybody I said a good word about 'csh' or any other Unix "shell" language, but I must say that particular feature is very useful. And "I think I think" is not a typo. ;-) **************************************************************** From: Tucker Taft Date: Monday, June 22, 2009 5:07 PM I'll admit to being of two minds. I would really like to see a generalized iteration mechanism where one could "program" this kind of loop, rather than adding yet more special looping syntax. On the other hand, if we do add this general sequence notation, then allowing it for loops does seem like a natural extension. As an implementation strategy, I presume one would either create an implicit array of individual values, if the total sequence (including any ranges) is relatively short, or an implicit array of low/high pairs, to handle arbitrarily large ranges. Then the iteration "for I in loop" becomes essentially either: for index in implicit_array'Range loop declare I : constant := implicit_array(index); begin end; end loop; or for index in implicit_array_of_pairs'Range loop for I in implicit_array_of_pairs(index).first .. implicit_array_of_pairs(index).last loop end loop; end loop; Definitely not rocket science, though definitely some new dynamic semantics expansion routines. **************************************************************** From: Robert Dewar Date: Monday, June 22, 2009 8:41 PM > I think I think it should be allowed in loops. Seems very useful for > enums. I just did this at a 'csh' prompt: Seems useful, but greatly increases the implementation burden I would say! **************************************************************** From: Randy Brukardt Date: Monday, June 22, 2009 3:49 PM > It sounds like we are moving toward some kind of common view here, > thanks in part to your throwing up some scary straw men along the > way... ;-) So many messages have come in here that I haven't been able to get a word in edgewise. So let me just throw out my thoughts without any attempt to relate them to the previous mail. (1) The proposed rules here are so different for scalar and composite types that we are really talking about two different features. That doesn't seem likely to help understanding, they probably ought to be separated with different names. (2) The restrictions on use for scalar "predicates" are likely to cause annoying generic contract issues -- or they will have to be illegal to use as generic actuals, which of course will cause annoying generic usage issues. (3) I can't see the benefit of trying to provide static versions of these; the predicate is can contain anything, after all. If we really wanted static versions, then we should support first-class discontinuous scalar subtypes. (It appears that we have the syntax for that.) That seems to be Bob's thinking as to the most likely usage in practice. In that case, we don't need scalar predicates at all - the extra complication of having both is not worth it. (Do we really need subtype Even or subtype Power_of_Two??) (4) I don't think it makes sense to try to check for inappropriate usage in composite predicates. Just make it a bounded error to write anything or read anything other than bounds or discriminants. The suggestion that they be checked to only depend on bounds, discriminants, constants, and pure functions is laudable, but problematic: We don't have a formal definition of pure functions for one thing (surely we'd want to include predefined operators, but those are rarely declared in a pure package). In the past, we couldn't come to agreement on such a concept, and everytime I've suggested it I've been shot down. The GNAT definition of a pure function is essentially to make it a bounded error (or erroneous??) if it is not one; I think that is the most that we could agree to here. But we don't need to agree to that at all, because all we need to do is say it as I described above (no mention of functions is needed). Let's not waste our time arguing about what is a pure function since t isn't important for this concept. (5) Steve's proposal (as best as I understand it) seems to disallow using any such predicates on access types. That seems to eliminate my original usage case as a possibility (of course, it could still be written as preconditions). That seems bad. Similarly, restricting these to discriminants is going to eliminate many other usage cases. That makes me wonder if the whole thing is worth it (at this point, I would say no - based on the discussion here, we should simply (and completely) define discontiguous discrete subtypes and forget the rest). **************************************************************** From: Steve Baird Date: Monday, June 22, 2009 4:59 PM > (1) The proposed rules here are so different for scalar and composite > types that we are really talking about two different features. That > doesn't seem likely to help understanding, they probably ought to be > separated with different names. They seem similar to me. In both cases, we are using a predicate in restricting the elements of a subtype. > (2) The restrictions on use for scalar "predicates" are likely to > cause annoying generic contract issues -- or they will have to be > illegal to use as generic actuals, which of course will cause annoying > generic usage issues. The latter, and you are right. It is annoying that you can't pass one of these types to a generic that takes a formal discrete unless the formal also has an associated (formal) predicate. The problems with for-loops, arrays, etc. prevented a completely satisfactory solution. As Bob and others pointed out, users want to use this construct to define parameter and result subtypes. They won't be happy with an explanation that they can't have these subtypes because we couldn't figure out how they should work when used as an entry family index. > (3) I can't see the benefit of trying to provide static versions of > these; the predicate is can contain anything, after all. If we really > wanted static versions, then we should support first-class discontinuous scalar subtypes. In some sense that is what we are doing. If the predicate meets certain restrictions and the subtype meets the other conditions for a static subtype, then you get a discontinuous scalar subtype. What about it is 2nd-class? We are following the existing structure of the language here - a static subtype is just a "normal" subtype that happens to meet some additional restrictions. > (It appears that we have the syntax for that.) That seems to be Bob's > thinking as to the most likely usage in practice. In that case, we > don't need scalar predicates at all - the extra complication of having > both is not worth it. (Do we really need subtype Even or subtype > Power_of_Two??) I'm not sure I understand you. Are you saying that we should only support static scalar subtypes with predicates and give up on the non-static case? That is an interesting idea because it would allow us to eliminate the restrictions on for-loops, array-indexing, etc. A noncontiguous static subtype is not essentially different than a holey enumeration type and can use essentially the same implementation model. Perhaps we can come close to getting the best of both worlds my making the restrictions less stringent. A "static choice list"-predicate wouldn't have to trigger the rules disallowing uses in arrays, for-loops, instances, etc. > (4) I don't think it makes sense to try to check for inappropriate > usage in composite predicates. Just make it a bounded error to write > anything or read anything other than bounds or discriminants. The > suggestion that they be checked to only depend on bounds, > discriminants, constants, and pure functions is laudable, but > problematic: We don't have a formal definition of pure functions for > one thing (surely we'd want to include predefined operators, but those > are rarely declared in a pure package). In the past, we couldn't come > to agreement on such a concept, and everytime I've suggested it I've > been shot down. The GNAT definition of a pure function is essentially > to make it a bounded error (or erroneous??) if it is not one; I think > that is the most that we could agree to here. But we don't need to > agree to that at all, because all we need to do is say it as I > described above (no mention of functions is needed). Let's not waste our > time arguing about what is a pure function since it isn't important for > this concept. We haven't talked much about this point yet. > (5) Steve's proposal (as best as I understand it) seems to disallow > using any such predicates on access types. True. > That seems to eliminate my original > usage case as a possibility (of course, it could still be written as > preconditions). That seems bad. I agree. I didn't see how to make it work without introducing the possibility of an object going from valid to invalid in very dangerous ways. If we want to put more of the burden on the user and simply say that misuse of these predicates is erroneous, then we could support predicates on access types and I could revive my Nul_Terminated_String example. I don't think we should do that. If you have another approach, I'd like to hear about it. > Similarly, restricting these to > discriminants is going to eliminate many other usage cases. That makes > me wonder if the whole thing is worth it (at this point, I would say > no - based on the discussion here, we should simply (and completely) > define discontiguous discrete subtypes and forget the rest). Predicates for scalar types and for discriminated types do seem to work very nicely together. **************************************************************** From: Randy Brukardt Date: Monday, June 22, 2009 5:34 PM > > (1) The proposed rules here are so different for scalar and > > composite types that we are really talking about two different > > features. That doesn't seem likely to help understanding, they > > probably ought to be separated with different names. > > They seem similar to me. In both cases, we are using a predicate in > restricting the elements of a subtype. That's a very high level view. But the details are completely different: - A scalar predicate subtype can't be used in array indexes or loops or (most likely) case statements. A scalar predicate subtype doesn't match a generic formal. But the expression can be any Boolean expression (bounded error if it has side effects or depends on non-constant globals, I hope) - in particular, it can reference the object value. - A composite predicate subtype can't be used in most access types (echoing the rules for composite constraints). But it does match generic formals. The expression cannot reference anything other than bounds and discriminants. (What this means is TBD.) > > (2) The restrictions on use for scalar "predicates" are likely to > > cause annoying generic contract issues -- or they will have to be > > illegal to use as generic actuals, which of course will cause > > annoying generic usage issues. > > > > The latter, and you are right. It is annoying that you can't pass one > of these types to a generic that takes a formal discrete unless the > formal also has an associated (formal) predicate. > The problems with for-loops, arrays, etc. prevented a completely > satisfactory solution. > As Bob and others pointed out, users want to use this construct to > define parameter and result subtypes. They won't be happy with an > explanation that they can't have these subtypes because we couldn't > figure out how they should work when used as an entry family index. Right, but for scalar types, I don't see much use to the general power of this concept. Rather, we really want discontiguous "sets" of values. Why not just define that for real?? > > (3) I can't see the benefit of trying to provide static versions of > > these; the predicate is can contain anything, after all. If we > > really wanted static versions, then we should support first-class > discontinuous scalar subtypes. > > In some sense that is what we are doing. If the predicate meets > certain restrictions and the subtype meets the other conditions for a > static subtype, then you get a discontinuous scalar subtype. What > about it is 2nd-class? We are following the existing structure of the > language here - a static subtype is just a "normal" subtype that > happens to meet some additional restrictions. This still makes no sense to me. A predicate is just a Boolean expression (no restrictions), and it would never be static (a current instance is never static, is it?) So you are saying that some special form of a non-static Boolean expression makes a static subtype? That is just too weird for words. > > (It appears that we have the syntax for that.) That seems to be > > Bob's thinking as to the most likely usage in practice. In that > > case, we don't need scalar predicates at all - the extra > > complication of having both is not worth it. (Do we really need > > subtype Even or subtype > > Power_of_Two??) > > I'm not sure I understand you. Are you saying that we should only > support static scalar subtypes with predicates and give up on the > non-static case? No, I'm saying we should completely give up on the idea of scalar predicates and support non-contiguous subtype constraints instead. (Perhaps they ought to be required to be static, I'd have to think about that.) Something like: subtype Foo is new Integer range (1 | 3 | 7 .. 11); or more generally: subtype Identifier is new Subtype_Mark range Sequence; > That is an interesting idea because it would allow us to eliminate the > restrictions on for-loops, array-indexing, etc. > A noncontiguous static subtype is not essentially different than a > holey enumeration type and can use essentially the same implementation > model. Exactly. But they are no longer predicates at that point, they're just non-contiguous discrete (or scalar?) type constraints. They work everywhere, and have the same semantics as any other constraint (for scalar types). Predicates for composite types are a very different beast with a very different set of rules (and they are *not* constraints). > Perhaps we can come close to getting the best of both worlds my making > the restrictions less stringent. A "static choice list"-predicate > wouldn't have to trigger the rules disallowing uses in arrays, > for-loops, instances, etc. Right. They'd be completely normal scalar (or discrete?) constraints. Little new wording required (but more work for implementors because they appear everywhere). > > (4) I don't think it makes sense to try to check for inappropriate > > usage in composite predicates. Just make it a bounded error to write > > anything or read anything other than bounds or discriminants. The > > suggestion that they be checked to only depend on bounds, > > discriminants, constants, and pure functions is laudable, but > > problematic: We don't have a formal definition of pure functions for > > one thing (surely we'd want to include predefined operators, but > > those are rarely declared in a pure package). In the past, we > > couldn't come to agreement on such a concept, and everytime I've > > suggested it I've been shot down. The GNAT definition of a pure > > function is essentially to make it a bounded error (or erroneous??) > > if it is not one; I think that is the most that we could agree to > > here. But we don't need to agree to that at all, because all we need > > to do is say it as I described above (no mention of functions is > > needed). Let's not waste our time arguing about what is a pure > > function since it isn't important for this concept. > > We haven't talked much about this point yet. Well, we need to do so. It's very important to determining if composite predicates are even worth having. > > (5) Steve's proposal (as best as I understand it) seems to disallow > > using any such predicates on access types. > > True. > > > That seems to eliminate my original > > usage case as a possibility (of course, it could still be written as > > preconditions). That seems bad. > > I agree. I didn't see how to make it work without introducing the > possibility of an object going from valid to invalid in very dangerous > ways. If we want to put more of the burden on the user and simply say > that misuse of these predicates is erroneous, then we could support > predicates on access types and I could revive my Nul_Terminated_String > example. I don't think we should do that. > If you have another approach, I'd like to hear about it. My proposal is pretty much making any misuse (or surprising use) into a bounded error. Erroneous is not acceptable to me (this is supposed to *increase* safety, but the possible errors seem bounded (since these don't affect object shapes at all): either a check is made, or it is not, or (of course) Program_Error is raised. Seems harmless (if not as portable as I would like). As Bob said, it would be annoying that you couldn't write a predicate on an access type to use in a formal parameter, because of some language lawyer reason, in this case that a renaming that depends on a discriminant could be blown up because of some change of a discriminant -- none of which has anything to do with checking the precondition of a formal parameter of an access type! Indeed, if these *aren't* constraints, I don't see why we care about them changing in this case. It would mean that a compiler could not presume them to be true in some cases (such as dereferencing of access types), but that doesn't seem very important, since it is unlikely that a compiler is going to be able to eliminate these very dynamic checks anyway. So I'm suggesting that we make all misuse a bounded error and pretty much allow anything goes with them. Static checkers could complain if they want, but the language doesn't have the mechanisms needed. (If we want to add them, that would be OK by me, but I don't see much point if it just moves the bounded error from the predicate to some function it calls.) > > Similarly, restricting these to > > discriminants is going to eliminate many other usage cases. That > > makes me wonder if the whole thing is worth it (at this point, I > > would say no - based on the discussion here, we should simply (and > > completely) define discontiguous discrete subtypes and forget the rest). > > Predicates for scalar types and for discriminated types do seem to > work very nicely together. Except that you can't actually use the latter (unless you've managed to eliminate all access types from your program, a pretty unlikely scenario). Anyway, lots more thought is needed here. **************************************************************** From: Bob Duff Date: Monday, June 22, 2009 6:28 PM > > It sounds like we are moving toward some kind of common view here, > > thanks in part to your throwing up some scary straw men along the > > way... ;-) > > So many messages have come in here that I haven't been able to get a > word in edgewise. Yeah. Me, too. ;-) >...So let me just throw out my thoughts without any attempt to relate >them to the previous mail. Wise thoughts from Randy, here, but getting up to speed on these e-mails is a quadratic algorithm, like when you append strings to nul-terminated strings... I need to go back to the start and read until the end (repeatedly?) :-( > (1) The proposed rules here are so different for scalar and composite > types that we are really talking about two different features. That > doesn't seem likely to help understanding, they probably ought to be > separated with different names. But: subtype S10 is Integer range 1..10; subtype S4 is S10 range 1..4; -- OK subtype Str10 is String (1..10); subtype Str4 is Str10 (1..4); -- Wrong! So they're different. Too bad. > (2) The restrictions on use for scalar "predicates" are likely to > cause annoying generic contract issues -- or they will have to be > illegal to use as generic actuals, which of course will cause annoying > generic usage issues. Yes, but we have two ideas: Tuck suggested a contract-retaining syntax. There's always the "raise Program_Error" hack, also suggested by Tuck. > (3) I can't see the benefit of trying to provide static versions of > these; the predicate is can contain anything, after all. If we really > wanted static versions, then we should support first-class discontinuous scalar subtypes. > (It appears that we have the syntax for that.) That seems to be Bob's > thinking as to the most likely usage in practice. In that case, we > don't need scalar predicates at all - the extra complication of having > both is not worth it. (Do we really need subtype Even or subtype > Power_of_Two??) I thought I wanted arbitrary predicates, like even/power-of-two, but now I'm leaning toward your idea -- I really want arbitrary _static_ enumerated subtypes of enumerated types. Usable in case stms. But I also want those for discriminants (of enum types, especially). > (4) I don't think it makes sense to try to check for inappropriate > usage in composite predicates. Just make it a bounded error ... Yes, or something like that. >...to write anything or read > anything other than bounds or discriminants. The suggestion that they >be checked to only depend on bounds, discriminants, constants, and >pure functions is laudable, but problematic: We don't have a formal >definition of pure functions for one thing (surely we'd want to >include predefined operators, but those are rarely declared in a pure >package). In the past, we couldn't come to agreement on such a >concept, and everytime I've suggested it I've been shot down. The GNAT >definition of a pure function is essentially to make it a bounded >error (or erroneous??) if it is not one; The GNAT Ref Man says: It specifies that the function `Entity' is to be considered pure for the purposes of code generation. This means that the compiler can assume that there are no side effects, and in particular that two calls with identical arguments produce the same result. To me, "assume" here implies "erroneous", but I'm not sure that's what it really means. >... I > think that is the most that we could agree to here. But we don't need >to agree to that at all, because all we need to do is say it as I >described above (no mention of functions is needed). Let's not waste >our time arguing about what is a pure function since it isn't important for this concept. I agree with the "not waste time" part, and I agree that this concept need not involve "pure functions", whatever that might mean. > (5) Steve's proposal (as best as I understand it) seems to disallow > using any such predicates on access types. That seems to eliminate my > original usage case as a possibility (of course, it could still be > written as preconditions). That seems bad. Similarly, restricting > these to discriminants is going to eliminate many other usage cases. > That makes me wonder if the whole thing is worth it (at this point, I > would say no - based on the discussion here, we should simply (and > completely) define discontiguous discrete subtypes and forget the rest). I agree, I want to be able to say something about access types. And if I can't, why not just static scalar stuff? But what about discriminants? If I can say "subtype Speckled_Enum is.." then I also want to assert something about Speckled_Records, and access thereto. **************************************************************** From: Steve Baird Date: Monday, June 22, 2009 6:48 PM > But what about discriminants? If I can say "subtype Speckled_Enum is.." > then I also want to assert something about Speckled_Records, and > access thereto. If we are talking about a case where the object designated by an access value is guaranteed to be constrained for one reason or another, then it would be safe to allow a predicate for an access subtype to refer to the discriminant value of the designated object. And it would always be safe to refer to the bounds of a designated array object. Should this be included? **************************************************************** From: Tucker Taft Date: Monday, June 22, 2009 8:22 PM Known to be constrained? **************************************************************** From: Steve Baird Date: Tuesday, June 23, 2009 8:32 AM Right. **************************************************************** From: Bob Duff Date: Wednesday, February 24, 2010 3:29 PM I like this AI a lot. My homework assignment says "Examples for AI05-0153-1 (subtype predicates)". I don't understand what I'm supposed to do, because this AI already has a nice example. So instead I'm commenting on some details. > !standard 3.2.2(2) 10-02-11 AI05-0153-1/04 ... > The actual predicate is the given expression anded with the predicate > (if any) of the parent subtype. (The predicate of any subtype that > does not have one can be assumed to be the boolean literal True.) Parent subtype doesn't mean what you want it to mean: 8.d/2 To be honest: {AI95-00442-01} Any name of a category of types (such as "discrete", "real", or "limited") is also used to qualify its subtypes, as well as its objects, values, declarations, and definitions, such as an "integer type declaration" or an "integer value." In addition, if a term such as "parent subtype" or "index subtype" is defined, then the corresponding term for the type of the subtype is "parent type" or "index type." 3/2 {AI95-00251-01} {AI95-00401-01} {AI95-00419-01} {parent subtype} {parent type} The parent_subtype_indication defines the parent subtype; its type is the parent type. The interface_list defines the progenitor types (see 3.9.4). A derived type has one parent type and zero or more progenitor types. ... > [Editor's note: We allow Program_Error because all bounded errors can > raise Program_Error. There is one exception to that, which I'm too lazy to look up right now. I think it's related to controlled types. I don't see any value to the user in allowing more than one exception. >... The "proceeds normally" wording is the same as 4.8(11.1/2).] > > AARM Ramification: An implementation can evaluate a predicate any time > an object is accessed in any way, if it desires. We have to say this > so that any side-effects of the predicate (bad practice, but surely > allowed) cannot be depended upon. Note that this isn't the same as > being allowed to check the predicate anywhere at all; there has to be > some use of a value or object that has the subtype. That's necessary > so that it is possible to write the predicate without an evaluation of itself > being triggered. I don't understand that last sentence. But I agree we can't allow "anywhere at all" -- that would mean the compiler could insert race conditions at will, and other bad things. My understanding is that implementations are REQUIRED to check predicates in many cases, such as parameter passing (because that depends on subtype conversion). Is that correct? It might be easier to understand if we said that first, because otherwise my first impression is "this feature is totally optional". > Add to the end of 3.3.1(18/2) (which describes the meaning of > "initialized by default"): > > If the nominal subtype has a predicate, the predicate is applied to > the object and Assertions.Predicate_Error is raised if the result is False. > > [Editor's note: We need to check that default initialized objects > don't violate their predicate.] I don't think I agree with this. At least not in all cases. E.g., for integers: X : T; -- (1) ... if Flag then X := 123; end if; ... if Flag then X := X + 1; end if; I don't think I want the possibly-invalid value checked at (1). > Modify 3.4(18-22/2): > > Informally, the predicate of the corresponding subtype is that of the > subtype of the parent/progenitor type anded with the predicate of the > derived type. The new (sub)type is considered to have a predicate > (even if none is explicitly given). > > AARM Reason: If a subprogram has parameter(s) whose subtype(s) have > defined predicate(s), the generated code of subprogram body may depend > on ^ the > those predicates being checked. (A compile could assume that they had > been compileR > checked at the point of a call.) If the predicates did not compose, a > call of the derived subprogram might not actually check the > predicates, and that would cause big trouble. > > Add as the last sentence of 3.6(9): > > An index subtype shall not statically denote a subtype with a predicate. "statically denote"? Why "statically"? Why not just "be"? > checked at the point of a call.) If the predicates did not compose, a > call of the derived subprogram might not actually check the > predicates, and that would cause big trouble. > > Add as the last sentence of 3.6(9): > > An index subtype shall not statically denote a subtype with a predicate. "statically denote"? Why "statically"? Why not just "be"? > Add as the last sentence of 3.6(21): > > The elaboration of an array_type_definition raises Program_Error if > the index subtype has a predicate. > > AARM Reason: We don't want to create "holey" array types; it is very > confusing as to whether the values for which the predicate returns > False have associated elements. By raising Program_Error, we prevent > generic contract problems. But we also have a legality rule so when it > is statically known (outside of a generic) we detect the problem at > compile-time.] Ah, I see. This is inconsistent with similar cases, where we just make it a run time error, and trust compilers to give warnings when statically known. > Add after 3.6.1(5): > > The discrete_range of an index_constraint shall not statically denote > a subtype with a predicate. > > Add as the last sentence of 3.6.1(8): > > The elaboration of an index_constraint raises Program_Error if any > discrete_range is a subtype with a predicate. > > AARM Reason: We don't want to create "holey" array subtypes. By > raising Program_Error, we prevent generic contract problems. But we > also have a legality rule so when it is statically known (outside of a > generic) we detect the problem at compile-time.] You don't need to repeat this. Just refer to the earlier comment. > Add after 4.1.2(4): > > Legality Rules > > The discrete_range of a slice shall not statically denote a subtype > with a predicate. > > Add as the last sentence of 4.1.2(7): > > The evaluation of a slice raises Program_Error if any discrete_range > is a subtype with a predicate. > > AARM Reason: We don't want to create "holey" slices, especially as > slices can be required to be passed by reference (for by-reference > component types), and ignoring the predicate would be very confusing. > By raising Program_Error, we prevent generic contract problems. But we > also have a legality rule so when it is statically known (outside of a > generic) we detect the problem at compile-time.] Same here. ... > Add after 4.6(58): > > Implementation Permissions > > If the target subtype of a conversion has a predicate, and the nominal > subtype of the operand is that same subtype, an implementation may > omit the application of a predicate to the operand. We might need to define "same subtype". Or use "statically matching"? ... > !discussion > > This proposal seems similar to type invariants on the surface. > However, these two constructs solve different problems. ... I think this philosophical discussion is rubbish, but so long as we can agree on the language rules (we're very close!), we don't need to hash that out. >...A type invariant is a > requirement on all values of a type outside of the type's defining >package(s). In particular, it does not vary depending on the view of >an object. A constraint and/or predicate is a requirement on a >particular view of an object. It can be different on different views >of the same object (as in a formal parameter). Thus it can be used to >specify temporary or transient requirements on an object. > > --- > > 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 applies to an applieD > unconstrained subtype, the resulting subtype is unconstrained. And so on. > > This mirrors the semantics of null exclusions (which also are not constraints). ...for reasons only language lawyers can grok. Sigh. > Note that this can lead to some unusual circumstances: > > subtype Even is Integer range 1 .. 10 when Predicate => Even mod > 2 = 0; WITH > type Evens is array (Even) of Boolean; -- 5 or 10 elements? But you outlawed this above. Maybe you're trying to explain why, but the wording says "can", not "could (if it were legal)" and so forth. > Obj : Evens; > Obj(1) := False; -- Would Raise Predicate_Error. > > Type Evens has length 10. Evens'range goes from 1 .. 10. However, > attempting to index component 1 will raise Predicate_Error. (That's > because 1 will be converted to subtype Even, as noted in 4.1.1(7), and > that will trigger a predicate check.) However, the situation gets > nastier still when arrays are sliced by subtypes with a > predicate: > > Str : String := "1234567890"; > > Put(Str(Even)); > > One might expect to have "24680" printed, but since the constraints > are unchanged, "1234567890" would actually be printed. Because of this > weird behavior, we do not allow predicates on index subtypes. In order > to avoid breaking the contract model, we raise Program_Error in generic > bodies if the subtype has a predicate. Here's a radical notion: Raise P_E when an instance is elaborated, if it contains any such evil things, even in unreachable/unreached code. > --- > > Originally, this proposal made predicates "user-defined constraints". > This does not work, however, for a number of reasons: Bah! We can call them whatever we like, it doesn't make any difference to the rules. ... > For example: > > type Rec is record > A : Natural; > end record; > subtype Decimal_Rec is Rec with Predicate => Rec.A mod 10 = 0; > > Obj : Decimal_Rec := (A => 10); -- (1) > > procedure Do_It (P : in out Rec) is > begin > P.A := 5; > end Do_It; > > Do_It (Obj); -- (2) > Put (Obj in Decimal_Rec); -- (3) > > The predicate on Decimal_Rec will be checked on the aggregate at (1). > However, after the call at (2), the predicate is no longer true for Obj. > The call at (3) will print False. Implementations are allowed to check So why don't we require a predicate check on the way out? That's the one common case where subtype conversion doesn't cover it. **************************************************************** From: Randy Brukardt Date: Wednesday, February 24, 2010 8:15 PM ... > My homework assignment says "Examples for AI05-0153-1 (subtype > predicates)". > I don't understand what I'm supposed to do, because this AI already > has a nice example. My recollection is that you said something to the effect that you had "many examples" of how this would help. Steve said that he wanted to see some of them. Thus you got an action item. Essentially, the one example doesn't seem to have been enough to sway others. If you want to keep this AI alive, I think you need to find some additional examples of usage. (In e-mail, you've typically used variations of this particular compiler example that I used in the original AI; I guess the feeling is that not enough Ada users are writing compilers to matter.) **************************************************************** From: Randy Brukardt Date: Wednesday, February 24, 2010 8:52 PM ... > > The actual predicate is the given expression anded with the > > predicate (if any) of the parent subtype. (The predicate of any > > subtype that does not have one can be assumed to be the boolean > > literal True.) > > Parent subtype doesn't mean what you want it to mean: ... OK, but at this point, you have to propose wording that *does* mean the right thing. Nothing at all comes to mind. ... > > [Editor's note: We allow Program_Error because all bounded errors > > can raise Program_Error. > > There is one exception to that, which I'm too lazy to look up right now. > I think it's related to controlled types. If there is, it would violate 1.1.5(8): "...but in any case one possible effect of a bounded error is the raising of the exception Program_Error.". > I don't see any value to the user in allowing more than one exception. I'm not going to try to ignore 1.1.5(8); it would allow raising Program_Error even if we didn't say that. ... > > AARM Ramification: An implementation can evaluate a predicate any > > time an object is accessed in any way, if it desires. We have to say > > this so that any side-effects of the predicate (bad practice, but > > surely > > allowed) cannot be depended upon. Note that this isn't the same as > > being allowed to check the predicate anywhere at all; there has to > > be some use of a value or object that has the subtype. That's > > necessary so that it is possible to write the predicate without an > > evaluation of itself being triggered. > > I don't understand that last sentence. If we allowed evaluation of the predicate *anywhere*, that would include during the evaluation of the predicate. Which wouldn't work very well. :-) I can imagine implementations that might do that. Beyond that, there is the tasking issues of evaluating these anywhere; I didn't want to talk about those specifically because its hard to define what shouldn't be allowed. If you can word this better, suggest away. > But I agree we can't allow "anywhere at all" -- that would mean the > compiler could insert race conditions at will, and other bad things. > > My understanding is that implementations are REQUIRED to check > predicates in many cases, such as parameter passing (because that > depends on subtype conversion). Is that correct? It might be easier > to understand if we said that first, because otherwise my first > impression is "this feature is totally optional". The requirement to write wording in RM order often leads to non-optimal orders. In this case, though, I simply have no idea where this text belongs. I suggested perhaps in 13.9.1, which would avoid the problem as it would be buried in the back of the RM. > > Add to the end of 3.3.1(18/2) (which describes the meaning of > > "initialized by default"): > > > > If the nominal subtype has a predicate, the predicate is applied to > > the object and Assertions.Predicate_Error is raised if the > result is False. > > > > [Editor's note: We need to check that default initialized objects > > don't violate their predicate.] > > I don't think I agree with this. At least not in all cases. > E.g., for integers: > > X : T; -- (1) > ... > if Flag then > X := 123; > end if; > ... > if Flag then > X := X + 1; > end if; > > I don't think I want the possibly-invalid value checked at (1). That's not the case I was thinking of. I was thinking of a record type: type Foo with Predicate (B*2 = C) is record B : Natural := 10; C : Natural := 15; end record X : Foo; -- Violates the predicate. In this case, there is no reason to ever check this (given the permission to skip checks when the subtype doesn't change). So it would never be required to be detected, which is nasty. ... > > AARM Reason: We don't want to create "holey" array types; it is very > > confusing as to whether the values for which the predicate returns > > False have associated elements. By raising Program_Error, we prevent > > generic contract problems. But we also have a legality rule so when > > it is statically known (outside of a generic) we detect the problem > > at compile-time.] > > Ah, I see. > > This is inconsistent with similar cases, where we just make it a run > time error, and trust compilers to give warnings when statically > known. It's consistent with accessibility checks. In most other cases, we've made the body cases always illegal. I don't know of any cases where we make such things runtime errors. > > Add after 3.6.1(5): > > > > The discrete_range of an index_constraint shall not > statically denote > > a subtype with a predicate. > > > > Add as the last sentence of 3.6.1(8): > > > > The elaboration of an index_constraint raises Program_Error if any > > discrete_range is a subtype with a predicate. > > > > AARM Reason: We don't want to create "holey" array subtypes. By > > raising Program_Error, we prevent generic contract problems. But we > > also have a legality rule so when it is statically known > (outside of a > > generic) we detect the problem at compile-time.] > > You don't need to repeat this. Just refer to the earlier comment. Yes I do, it's in a different clause, and I want the RM to be reasonable useful as a reference. This particular case is iffy, but the others (like the 4.1.2) are much more valuable - no one reading 4.1.2 is going to go read 3.6 to figure out why the rules are the way they are. > > This proposal seems similar to type invariants on the surface. > > However, these two constructs solve different problems. ... > > I think this philosophical discussion is rubbish, but so long as we > can agree on the language rules (we're very close!), we don't need to > hash that out. Well, if you disagree with this, then you are saying that you don't want both AI-146 and AI-153-1. And in that case, it's this AI that is likely to disappear. So we need to be able to explain the difference, or prepare to drop one. > > subtype Even is Integer range 1 .. 10 when Predicate > => Even mod > > 2 = 0; > WITH > > > type Evens is array (Even) of Boolean; -- 5 or 10 elements? > > But you outlawed this above. Maybe you're trying to explain why, but > the wording says "can", not "could (if it were legal)" and so forth. It wasn't illegal when this was written, and the rewrite was very simple and quick, as this AI was left on life-support. ... > > Originally, this proposal made predicates "user-defined constraints". > > This does not work, however, for a number of reasons: > > Bah! We can call them whatever we like, it doesn't make any > difference to the rules. Only if you are willing to abandon the current model of constraints in the language. I don't know of anyone (other than you, perhaps) that's willing to do that. ... > > The predicate on Decimal_Rec will be checked on the aggregate at (1). > > However, after the call at (2), the predicate is no longer true for Obj. > > The call at (3) will print False. Implementations are allowed to > > check > > So why don't we require a predicate check on the way out? > That's the one common case where subtype conversion doesn't cover it. Don't copy-backs use subtype conversion? (At least for by-copy types). For by-reference types, it would be a completely new check in a place where none currently exists. That seems bad, at least for this feature (which was designed to be minimum cost). Anyway, you've done a pretty good job of reminding me why, while I'd like some way to do this, it really doesn't work very well. I'm probably going to vote to kill this in the absense of new examples of use. **************************************************************** From: Bob Duff Date: Thursday, February 25, 2010 2:31 PM One other comment: This AI says you can put a predicate on a subtype_declaration. But we should also allow it on a type_declaration, because type_decls declare subtypes. As in: type T is range A..B with Predicate => Is_Good(T); It would be really annoying to force that to be split in two, with two different names for the same thing. > ... > > > The actual predicate is the given expression anded with the > > > predicate (if any) of the parent subtype. (The predicate of any > > > subtype that does not have one can be assumed to be the boolean > > > literal True.) > > > > Parent subtype doesn't mean what you want it to mean: > ... > > OK, but at this point, you have to propose wording that *does* mean > the right thing. Nothing at all comes to mind. I thought that was your job. ;-) I don't think it's all that hard. It might take some time to track down all the places where subtypes are created. For a subtype created by a subtype_declaration, the predicate is the given expression and-ed with the predicate (if any) of the subtype denoted by the subtype_mark. For a subtype created by a subtype_indication that is not that of a subtype_declaration, the predicate is that (if any) of the subtype denoted by the subtype_mark. Maybe we need to say something about ranges and/or discrete_ranges, etc. I think if you say: type Page_Count is range 0..Max_Int with Predicate => Page_Count mod Page_Size = 0; for X in Page_Count'(0) .. 10*Page_Size loop We don't want any predicate on X's subtype. Or maybe you already forbid that. (I'm getting tired of the Even example, which people have scorned as being silly. But multiple-of-page-size does come up in real code.) > ... > > > [Editor's note: We allow Program_Error because all bounded errors > > > can raise Program_Error. > > > > There is one exception to that, which I'm too lazy to look up right now. > > I think it's related to controlled types. > > If there is, it would violate 1.1.5(8): "...but in any case one > possible effect of a bounded error is the raising of the exception Program_Error.". Yup. Since you don't (yet) see the light, I've tracked down the case (see 7.6.1): 20 * For a Finalize invoked by a transfer of control due to an abort or selection of a terminate alternative, the exception is ignored; any other finalizations due to be performed are performed. ... 20.b To be honest: {Program_Error (raised by failure of run-time check)} This violates the general principle that it is always possible for a bounded error to raise Program_Error (see 1.1.5, "Classification of Errors"). > > I don't see any value to the user in allowing more than one exception. > > I'm not going to try to ignore 1.1.5(8); it would allow raising > Program_Error even if we didn't say that. This seems like language-lawyering run amok! Foolish consistency, hobgoblins. We made up the meta-rule in 1.1.5(8), and we can break it (or modify it). In this case, there is no benefit (and some harm) caused by allowing two different exceptions to be raised. > ... > > > AARM Ramification: An implementation can evaluate a predicate any > > > time an object is accessed in any way, if it desires. We have to > > > say this so that any side-effects of the predicate (bad practice, > > > but surely > > > allowed) cannot be depended upon. Note that this isn't the same as > > > being allowed to check the predicate anywhere at all; there has to > > > be some use of a value or object that has the subtype. That's > > > necessary so that it is possible to write the predicate without an > > > evaluation of itself being triggered. > > > > I don't understand that last sentence. > > If we allowed evaluation of the predicate *anywhere*, that would > include during the evaluation of the predicate. Which wouldn't work > very well. :-) I'm still not sure I understand. Suppose we have: subtype S is Integer with Predicate => Is_Good(S); X : S; X := 123; As I understand it, we require Is_Good(123) to be evaluated here. Are you suggesting that somewhere in the body of Is_Good, the compiler could insert a call Is_Good(X) -- or for that matter, Is_Good(Some_Other_Object)? Yes, that would be bad. It would be at least as bad to insert a call Is_Good(X) before X has been elaborated! But these seem like oddities. >...I > can imagine implementations that might do that. I can't. ;-) >...Beyond that, there is the > tasking issues of evaluating these anywhere; I didn't want to talk > about those specifically because its hard to define what shouldn't be allowed. I think the tasking issue should be mentioned -- it's the most obvious and compelling reason. I don't think it's hard to define what shouldn't be allowed -- in fact you have already defined it perfectly well. In particular, the compiler is allowed to insert a check on any use of the object, and nowhere else. (And it is _required_ to insert a check on certain uses -- implicit subtype conversions, most importantly.) > If you can word this better, suggest away. Your normative wording is fine. The AARM wording could be to replace the "That's necessary ..." sentence with "Otherwise, the compiler could insert arbitrary race conditions, for example." > > But I agree we can't allow "anywhere at all" -- that would mean the > > compiler could insert race conditions at will, and other bad things. > > > > My understanding is that implementations are REQUIRED to check > > predicates in many cases, such as parameter passing (because that > > depends on subtype conversion). Is that correct? It might be > > easier to understand if we said that first, because otherwise my > > first impression is "this feature is totally optional". > > The requirement to write wording in RM order often leads to > non-optimal orders. In this case, though, I simply have no idea where this > text belongs. I suggested perhaps in 13.9.1, which would avoid the problem > as it would be buried in the back of the RM. Sounds good. I take it your answer to "Is that correct?" above is "Yes." > > > Add to the end of 3.3.1(18/2) (which describes the meaning of > > > "initialized by default"): > > > > > > If the nominal subtype has a predicate, the predicate is applied > > > to the object and Assertions.Predicate_Error is raised if the > > result is False. > > > > > > [Editor's note: We need to check that default initialized objects > > > don't violate their predicate.] > > > > I don't think I agree with this. At least not in all cases. > > E.g., for integers: > > > > X : T; -- (1) > > ... > > if Flag then > > X := 123; > > end if; > > ... > > if Flag then > > X := X + 1; > > end if; > > > > I don't think I want the possibly-invalid value checked at (1). > > That's not the case I was thinking of. I was thinking of a record type: > > type Foo with Predicate (B*2 = C) is record > B : Natural := 10; > C : Natural := 15; > end record > > X : Foo; -- Violates the predicate. > > In this case, there is no reason to ever check this (given the > permission to skip checks when the subtype doesn't change). So it > would never be required to be detected, which is nasty. Hmm. Deserves more thought. Maybe it's analogous to parameter passing: We could check if the type has discriminants or defaulted components (parts?). So uninitialized scalars would not be checked. Consider also the case of 'out' params of access type -- they get passed 'in', but without any constraint check (and I think without any null exclusion check). > ... > > > AARM Reason: We don't want to create "holey" array types; it is > > > very confusing as to whether the values for which the predicate > > > returns False have associated elements. By raising Program_Error, > > > we prevent generic contract problems. But we also have a legality > > > rule so when it is statically known (outside of a generic) we > > > detect the problem at compile-time.] > > > > Ah, I see. > > > > This is inconsistent with similar cases, where we just make it a run > > time error, and trust compilers to give warnings when statically > > known. > > It's consistent with accessibility checks. In most other cases, we've > made the body cases always illegal. I don't know of any cases where we > make such things runtime errors. Maybe I'm wrong. I can't find any cases to back me up just now. > > > Add after 3.6.1(5): > > > > > > The discrete_range of an index_constraint shall not > > statically denote > > > a subtype with a predicate. > > > > > > Add as the last sentence of 3.6.1(8): > > > > > > The elaboration of an index_constraint raises Program_Error if any > > > discrete_range is a subtype with a predicate. > > > > > > AARM Reason: We don't want to create "holey" array subtypes. By > > > raising Program_Error, we prevent generic contract problems. But > > > we also have a legality rule so when it is statically known > > (outside of a > > > generic) we detect the problem at compile-time.] > > > > You don't need to repeat this. Just refer to the earlier comment. > > Yes I do, it's in a different clause, and I want the RM to be > reasonable useful as a reference. This particular case is iffy, but > the others (like the 4.1.2) are much more valuable - no one reading > 4.1.2 is going to go read > 3.6 to figure out why the rules are the way they are. This is the AARM. I think it's perfectly fine to say "see 3.6 for why". > > > This proposal seems similar to type invariants on the surface. > > > However, these two constructs solve different problems. ... > > > > I think this philosophical discussion is rubbish, but so long as we > > can agree on the language rules (we're very close!), we don't need > > to hash that out. > > Well, if you disagree with this, then you are saying that you don't > want both AI-146 and AI-153-1. No, I'm saying nothing of the kind. I think it's OK to have both features. I think "subtype predicates" are far more useful than "type invariants" (as currently defined), and I would therefore strongly object to passing AI-146 but not AI-153-1; I'd vote against AI-146 in that case. I also think that with some work, we might be able to combine these two things into one coherent feature. I'm not sure about that, and I haven't had time to think it through. >...And in that case, it's this AI that is likely to disappear. So we >need to be able to explain the difference, or prepare to drop one. I can explain the difference between the two features (as currently defined) just fine: type invariants allow the invariant to be temporarily violated, whereas predicates do not. I think you agree with that, but you think that difference is somehow FUNDAMENTAL, whereas I think it's a minor point. I'm trying to think like a user, here, not a language lawyer. Analogy: You (with your language lawyer hat on) probably think "parent type" and "progenitor type" are fundamentally different. To normal Ada users, they're roughly the same thing. Likewise, "null exclusion" and "constraint" are not the same -- but they're roughly the same to normal users. > > > subtype Even is Integer range 1 .. 10 when Predicate > > => Even mod > > > 2 = 0; > > WITH > > > > > type Evens is array (Even) of Boolean; -- 5 or 10 elements? > > > > But you outlawed this above. Maybe you're trying to explain why, > > but the wording says "can", not "could (if it were legal)" and so > > forth. > > It wasn't illegal when this was written, and the rewrite was very > simple and quick, as this AI was left on life-support. > > ... > > > Originally, this proposal made predicates "user-defined constraints". > > > This does not work, however, for a number of reasons: > > > > Bah! We can call them whatever we like, it doesn't make any > > difference to the rules. > > Only if you are willing to abandon the current model of constraints in > the language. I don't know of anyone (other than you, perhaps) that's > willing to do that. OK, never mind. This is part of the "philosophy" that I said we can safely agree to disagree on. > ... > > > The predicate on Decimal_Rec will be checked on the aggregate at (1). > > > However, after the call at (2), the predicate is no longer true for Obj. > > > The call at (3) will print False. Implementations are allowed to > > > check > > > > So why don't we require a predicate check on the way out? > > That's the one common case where subtype conversion doesn't cover it. > > Don't copy-backs use subtype conversion? (At least for by-copy types). Yes, I think so. >...For > by-reference types, it would be a completely new check in a place >where none currently exists. That seems bad, at least for this feature >(which was designed to be minimum cost). Yes, it's new in the by-ref case. So what? It's extremely useful, and not hard to implement. Furthermore, for many types, the compiler can choose by-copy or by-ref, and it seems bad to make it implementation dependent whether or not the check is required on the way out. All I'm asking for here is that for a by-ref parameter of mode 'out' or 'in out', a predicate check is required after returning from the body. > Anyway, you've done a pretty good job of reminding me why, while I'd > like some way to do this, it really doesn't work very well. I think it works just fine, and you've done a good job of writing it up. We just need to work out the details. I think you are confusing the complexity of the discussion with the complexity of the final result, which is easy to do, because we haven't seen the final result yet. I think you may also be expecting too much: if you expect predicates to always be 100% guaranteed true, then you will be disappointed, because there are many loopholes (predicates with side effects, predicates that become false via "X.all.Blah := ...;", etc). But if you see that it's just a bunch of checks sprinkled around the place, that are 98% likely to be true, then you won't be disappointed. **************************************************************** From: Bob Duff Date: Thursday, February 25, 2010 2:53 PM > My recollection is that you said something to the effect that you had > "many examples" of how this would help. Steve said that he wanted to > see some of them. Thus you got an action item. > > Essentially, the one example doesn't seem to have been enough to sway > others. If you want to keep this AI alive, I think you need to find > some additional examples of usage. (In e-mail, you've typically used > variations of this particular compiler example that I used in the > original AI; I guess the feeling is that not enough Ada users are > writing compilers to matter.) Well, unfortunately, I'm a compiler writer, so most examples that pop into my head are compiler examples, or similar tools. I don't think the general principle of these examples is compiler specific, though. The general class of examples is an unordered enumeration type, and you want arbitrary subsets for subtypes of that enum, and also for records whose discriminant is that enum, and also for access types pointing to such records. It's a kludge to say: type Color is (Red, Green, Blue, Yellow, Orange, Purple); subtype Primary_Color is Color range Red..Blue; because you're depending on the order. And it's a maintenance hazard that has come up many times. Much better to say: subtype Primary_Color is Color with Predicate => Primary_Color in (Red, Green, Blue); or something. And of course it's impossible to use subranges when the predicate is noncontiguous. Other examples (not necessarily compiler specific): If you plan to divide by X, its subtype should exclude zero. An OS interface requires a size-in-bytes, but it must be a multiple of the page size. Ada measures sizes in bits, but it's sometimes necessary to measure in bytes (or storage units, if you prefer). "Predicate => Blah mod 8 = 0" might come in handy. A Sort function produces an array (or other sequence) of subtype Sorted_Sequence. Binary_Search takes a parameter of that subtype. Very useful to keep track of which objects have been sorted (can I pass this to Binary_Search, or must I sort it first?). To prevent SQL injection bugs, keep track of which data is "tainted" and which is "trusted", using predicates. See here: http://xkcd.com/327/ In a program that processes objects through multiple phases (could be a compiler!), you want to keep track of which phase(s) have been applied to each object, via subtypes. Temporal logic: you can't land the airplane until the wheels are down. So Land_Airplane takes a parameter of subtype Airplane_That_Is_Ready_To_Land, which is a subtype of Airplane. This is such a general feature that it seems hard to believe it's restricted to compiler-like programs in any way. It's just like constraints, except you can do more than just subranges of scalars, and single-values for discrims, etc. (And it's not quite as airtight as those, but oh, well.) **************************************************************** From: Bob Duff 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. We might want to decide that this stuff is too immature to include in Ada 2012. If so, I think GNAT will experiment with implementing this stuff, and using it. That might be a better approach than standardizing something that we're not sure is 100% right. If this AI is not included in Ada 2012, I am strongly opposed to including type invariants, for reasons I've already stated. In that case, perhaps compiler writers can experiment with invariants, too. I did a lot of rewriting. One thing I should mention: I removed the philosophical ramblings that I found objectionable, and replaced them with an objective (I hope) list of differences between predicates and invariants (and between predicates and constraints). Hopefully, we can all agree on what the differences are, even if I think those differences are minor, whereas Randy and others think they are major. [Following is version /05 of the AI.] **************************************************************** From: Randy Brukardt Date: Wednesday, April 28, 2010 11:15 PM > Here's a new version of AI05-0153-1 (subtype predicates), for > tomorrow's discussion. A few comments. ... > 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. Here is where we disagree. I don't think a predicate can or should have any effect on the values of a subtype, because that changes all of the rules involving validity, how iterations work, and the like. If we're doing those things, we need to greatly restrict the forms of the predicates, and I think that is a very bad idea (this "looks" general). If we're *not* doing those things, then lots of rewording is needed. > Add new section 3.2.4: > > 3.2.4 Subtype Predicates ... > 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. Rules about subtype conversions belong in 4.6. We've been *very* careful to maintain that up to this point, and I don't think we should start distributing those (especially only in a few cases). ... > An index subtype, discrete_range of an index_constraint or slice, or a > discrete_subtype_definition is illegal if it statically denotes a > subtype with a user-specified predicate. All of these forward references need section references. (That's why I put those rules in the appropriate clauses: to avoid the forward references.) ... > > 6.4.1(13) says: > > 13 * For an access type, the formal parameter is initialized from the > value of the actual, without a constraint check; > > Change it to: > > 13 * For an access type, the formal parameter is initialized from the > value of the actual, without any constraint, null-exclusion, or > predicate checks; We changed this wording in AI05-0196-1, approved in Burlington. Moreover this is out of order in the AI (clauses are supposed to come in order). The current wording is: For an access type, the formal parameter is initialized from the value of the actual, without checking that the value satisfies any constraint or any exclusion of the null value; because what a "constraint check" is not well-defined. ... > 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.Predicate_Error is raised if the result is False. I think you mean Assertion_Error here. I changed it. > !discussion > > Predicates are similar to constraints. The differences are: > > - Constraints are restricted to certain particular forms (range > constraints, discriminant constraints, and so forth), whereas predicates > can be arbitrary conditions. > > - Constraints can only be violated for invalid values, whereas predicates > can be violated in various ways (important side effects in predicates, > for example, could cause reevaluation of the predicate to get a different > answer). However, it is possible to write well-behaved predicates. We > don't know how to FORCE the programmer to write well-behaved predicates > without being too restrictive. On this bullet, I think our only difference is a matter of degree. It's unlikely that anyone will write well-behaved predicates for composite types. The only ones that could qualify only involve bounds or discriminants (directly, no dereferencing). It's easy to see that: all of the fancy rules that keep access to constrained discriminated types from causing problems aren't going to be enforced for predicates. So depending on anything other than discriminants will not be "well-behaved". The other major difference between a predicate and a constraint is that the predicate cannot affect the value set for the type. If it did, then validity would depend on the predicate, and since that cannot be trusted in general, it would be impossible to do any reasoning about validity of objects. Which would make any check elimination (not just predicate checks, but any check) technically wrong - a result we surely don't want. We had a HUGE amount of trouble with the value set for null exclusions, and this would be many times worse. I really don't even want to think about it -- you would have to do the careful research to prove that there is no problem (and explain why you think that) before I'd even consider voting to abstain on a proposal changing the value set based on arbitrary expressions potentially with side-effects. ... > ???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. They *should* use Precondition_Error and Postcondition_Error; they're not assertions (not in my world anyway; I don't want them at all if they are "just" assertions). > 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. That's true; it really depends on whether you use the names of the exceptions as debugging information or you just want to use one and assume your IDE+runtime bails you out as to the cause of the problem. With Claw, we used a set of different exceptions for different causes, but not one for every possible error (about the same level as IO_Exceptions). I think the same would be appropriate here. So I could see using the same exception for Preconditions and Postconditions (and maybe even predicates), but I don't think those should be shared with anything else. This is something we could literally argue forever. Not a big deal in any case. ... > subtype Callable_Symbol_Ptr is not null Symbol_Ptr with > Predicate => Callable_Symbol_Ptr.Entity in (Proc, Func, An_Entry); I'd prefer that you don't use unapproved AIs in examples, unless you really need 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". ****************************************************************