!standard 3.2.2(2) 09-10-26 AI05-0153-1/03 !class Amendment 09-05-27 !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. !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 [Author's note: This very simple proposal is closest to my original intent. It is likely to be cheap to implement and fairly powerful, but could create some anomolies. A less powerful proposal better integrated into the language (but far more expensive to implement is given in AI05-0153-2)]. Replace 3.2.2(2) with: subtype_declaration ::= subtype defining_identifier is subtype_indication [predicate_clause]; [Editor's note: "predicate_clause" is intended to be similar/identical to that used for types and subprograms. But Tucker hasn't made a formal proposal on that yet, so I will explain the rules needed here.] predicate_clause ::= with aspect_identifier => Boolean_expression Informal: The only aspect_identifier supported here is "Predicate". The Boolean_expression could use the defining_identifier of the subtype, to mean the "current instance" of the subtype (that is, the object to test the predicate against). [Editor's note: I'll leave the formal wording of this to Tucker's proposal. No sense in beating my head on a wall to figure this out!] Most likely, the formal proposal for clauses will require an associated operational attribute. In this case that would be S'Predicate, a function with a parameter of type S'Base returning Boolean. The definition of that attribute is not currently shown here. 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.) [Editor's note: The predicate has no effect on the static or dynamic semantics of the subtype indication except as noted here.] 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. AARM Reason: If a subprogram has parameter(s) whose subtype(s) have defined predicate(s), the generated code of subprogram body may depend on those predicates being checked. (A compile could assume that they had been 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. 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. 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, the predicate is applied to the value and Assertions.Predicate_Error is raised if the result is False. Modify 4.9.1(2/2): A subtype statically matches another subtype of the same type if they have statically matching constraints, {neither has a predicate or both predicates come from the same predicate_clause, }and, for access subtypes, either both or neither exclude null. ... Add after 11.4.2(13/2): Predicate_Error : exception; -- See 4.6 !discussion This proposal seems similar to type invariants on the surface. However, these two constructs solve different problems. 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 unconstrained subtype, the resulting subtype is unconstrained. And so on. This mirrors the semantics of null exclusions (which also are not constraints). Note that this can lead to some unusual circumstances: subtype Even is Integer range 1 .. 10 when Predicate => Even mod 2 = 0; type Evens is array (Even) of Boolean; -- 5 or 10 elements? Obj : Evens; Obj(1) := False; -- Raises 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.) This is a bit annoying, but it again is similar to the behavior of null exclusions: type Acc_Int is not null access Integer; Ptr : Acc_Int; -- Raises Constraint_Error In both cases, doing something stupid creates trouble. But there is no good reason to write either of these examples, and compilers can provide warnings in both cases. So it does not appear to be a significant issue. --- Originally, this proposal made predicates "user-defined constraints". This does not work, however, for a number of reasons: (1) A predicate does not provide a unique value for bounds or discriminants, thus it is impossible to declare a composite object using such a constraint. We then have to define partially constrained subtypes. (2) A predicate does not clearly define 'First or 'Last values, so calling it a constraint on a scalar subtype brings up many nasty questions. For instance, subtype Even is Integer range 1 .. 10 when Predicate => Even mod 2 = 0; type Evens is array (Even) of Boolean; -- 5 or 10 elements? (3) A predicate can depend on components other than discriminants. If a component is modified, the predicate can become false. This can happen at arbitrary points in the program. It is especially bad when the predicate is applied to an access type; it is easy to see how it could be violated. These problems can be worked around by adding various restrictions, but that just makes predicates less useful and far more complex. --- We define predicates to be part of static matching, so that subtypes with different predicates are not considered identical. --- An alternative way of looking at predicates is to assume that all subtypes have a predicate of True by default, and a predicate_clause just replaces that with something user-defined. --- 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). --- Note that predicates are only true at the point where the language does a subtype conversion into the subtype. Depending on the predicate, later operations can make the predicate False. This is not a major problem for the primary intended use of predicates (on formal subprogram parameters), but could be an issue if they are used on subtypes in other contexts. 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 put 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. --!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. ****************************************************************