CVS difference for ai05s/ai05-0153-1.txt
--- ai05s/ai05-0153-1.txt 2010/02/25 05:01:43 1.6
+++ ai05s/ai05-0153-1.txt 2010/04/08 02:00:07 1.7
@@ -2673,3 +2673,436 @@
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.)
+
+****************************************************************
Questions? Ask the ACAA Technical Agent