Version 1.6 of ai12s/ai12-0243-1.txt

Unformatted version of ai12s/ai12-0243-1.txt version 1.6
Other versions for file ai12s/ai12-0243-1.txt

!standard 3.9.2(10/2)          20-03-25 AI12-0243-1/03
!standard 3.9.2(20.4/3)
!class Amendment 18-01-11
!status work item 18-05-07
!status Hold by Letter Ballot failed (8-3-0) - 18-05-07
!status work item 18-01-11
!status received 17-10-20
!priority Very_Low
!difficulty Medium
!subject Subtypes as primitive arguments
!summary
Allow non-first subtypes for controlling parameters and controlling results.
!problem
The use of subtypes with dynamic predicates can be used to factor out common checks from the preconditions of an interface. This reduces code duplication and reduces the chance of forgetting a check.
The technique is important enough that an example was provided in the Standard, in the examples for subclause 3.2.4. It shows a hypothetical update to Text_IO using subtypes with dynamic predicates to provide most of the precondition checks needed.
However, if the type in question is tagged, Ada does not allow controlling operands to have non-first subtypes. This means that the technique cannot be used on the primitive operations of a tagged type.
!proposal
(See Wording.)
!wording
Replace 3.9.2(10/2):
In the declaration of a dispatching operation of a tagged type, everywhere a subtype of the tagged type appears as a subtype of the profile (see 6.1), it shall statically match the first subtype of the tagged type. If the dispatching operation overrides an inherited subprogram, it shall be subtype conformant with the inherited subprogram. The convention of an inherited dispatching operation is the convention of the corresponding primitive operation of the parent or progenitor type. The default convention of a dispatching operation that overrides an inherited primitive operation is the convention of the inherited operation; if the operation overrides multiple inherited operations, then they shall all have the same convention. An explicitly declared dispatching operation shall not be of convention Intrinsic.
with
If a dispatching operation of a tagged type overrides an inherited subprogram, it shall be subtype conformant with the inherited subprogram, except where a subtype of the tagged type appears as a subtype of the profile (see 6.1), in which case any subtype of the tagged type is permitted [Redundant: (including as the designated subtype of an access parameter or access result)]. The convention of an inherited dispatching operation is the convention of the corresponding primitive operation of the parent or progenitor type. The default convention of a dispatching operation that overrides an inherited primitive operation is the convention of the inherited operation; if the operation overrides multiple inherited operations, then they shall all have the same convention. An explicitly declared dispatching operation shall not be of convention Intrinsic.
Add after 3.9.2 (20.4/3) - not as part of the bulleted list:
In a dispatching call, the subtype of each formal parameter of the call and the result subtype (if any) of the call are determined by the subprogram body that is executed [Redundant: , not by the subprogram declaration denoted by the name or prefix of the call.]
AARM Discussion: This distinction matters in the case of a controlling parameter or a controlling result, where "any subtype of the tagged type is permitted" for overriding (see above). This implies, for example, that when the dynamic semantics rules for parameter passing in 6.4.1 state that "a view conversion of the actual parameter to the nominal subtype of the formal parameter is evaluated", the "formal parameter" in question is that of the subprogram whose body is executed.
AARM Implementation note: In the case of a dispatching call, this means that any constraint checking involving the subtype of a controlling parameter or a controlling result typically cannot be performed at the call site.
!discussion
The existing model was chosen because of the need to perform constraint checks at a call site. This is true for dispatching operations just as for other kinds of calls -- the checks are performed before dispatching to the chosen body. In order to allow dispatching operations with non-first-subtypes for parameter subtypes, then you have to be sure that the parameter's subtypes in an overriding of a dispatching routine have exactly the same checks required at the point of call, or you have to abandon the model that the checks are done at the call site.
We first looked at a more restrictive "corresponding subtype" model, where given a type T1, a descendant type T2, and a subtype S1 of T1, we would be able to define a "corresponding" subtype S2 of T2 which is subject to constraints and predicates which "correspond", in some sense, to those which apply to S1. This would allow continuing to have the checks made at the call site.
For example, given
package Pkg1 is type File is tagged private;
subtype Open_File is File with Dynamic_Predicate => Is_Open (Open_File);
function Is_Open (F : File) return Boolean;
function Read_Line (F : Open_File) return String; end;
this approach might allow something like
with Pkg1; package Pkg2 is type My_File is new Pkg1.File with ...; overriding function Read_Line (F : My_File'Corresponding_Subtype (Pkg1.Open_File)) return String; end Pkg2;
But it was decided that the wording for this approach was becoming too complex. So the current approach, in which no matching is required, was adopted. This approach is considerably simpler and requires substantially less new wording.
The major drawback of this approach is that the contract of a dispatching call becomes less precise because the subtypes of the controlling parameters and/or result are not known statically. And the checks have to be performed in the subprogram body.
This is OK, however, as a subtype predicate is defined and acts much like Pre (which is not part of the contract of a dispatching call) rather than Pre'Class (which is part of that contract). In order for a predicate to be part of the contract, we would need a much more complex mechanism that follows rules similar to Pre'Class for dispatching and static binding.
!example
package Pkg1 is type Parent is tagged ... ; function Is_Wonderful (X : Parent) return Boolean; subtype S is Parent with Dynamic_Predicate => Is_Wonderful (S);
procedure Op (Y : in out S); -- Previously illegal, now legal. end Pkg1;
with Pkg1; package Pkg2 is type Ext is new Pkg1.Parent with ... ;
overriding procedure Op (Y : in out Ext); -- No predicate required here. end Pkg2;
!ASIS
None needed.
!ACATS test
An ACATS C-Test is needed to check that the new capabilities are supported.
!appendix

!topic Subtypes as primitive arguments
!reference Ada 2012 RM
!from Victor Porton 17-10-21
!keywords subtype subprogram argument primitive subprogram
!discussion

I propose to allow subtypes (for example subtypes with predicates) as
controlling primitive subprogram arguments.

A subtype ST of type T for argument A should work as the base type T, but with
checking if "T(A) in ST" before doing dispatch (and raising an exception
otherwise).

This is probably especially useful with predicates.

Now as a workaround I replace ST with ST'Class in my code.

****************************************************************

From: Tucker Taft
Sent: Friday, October 20, 2017  4:28 PM

There are some technical reasons why dispatching operations were restricted
to having "first" subtypes for their controlling operands.  Can you give some
concrete examples where using (non-first) subtypes, perhaps with predicates,
would be necessary to implement a given abstraction?

****************************************************************

From: Randy Brukardt
Sent: Friday, October 20, 2017  8:58 PM

It might help if you explained the technical reasons, since the reason you
would want predicates seems obvious. Consider Text_IO. If File_Type was
tagged (which it might have been if defined in Ada 95), then the preferable
definition is as described in the RM, 3.2.4(41-51/4):

with Ada.IO_Exceptions;
package Ada.Text_IO is

   type File_Type is [tagged] limited private;

   subtype Open_File_Type is File_Type
      with Dynamic_Predicate => Is_Open (Open_File_Type),
           Predicate_Failure => raise Status_Error with "File not open";
   subtype Input_File_Type is Open_File_Type
      with Dynamic_Predicate => Mode (Input_File_Type) = In_File,
           Predicate_Failure => raise Mode_Error with "Cannot read file: " &
              Name (Input_File_Type);
   subtype Output_File_Type is Open_File_Type
      with Dynamic_Predicate => Mode (Output_File_Type) /= In_File,
           Predicate_Failure => raise Mode_Error with "Cannot write file: " &
              Name (Output_File_Type);

   ...

   function Mode (File : in Open_File_Type) return File_Mode;
   function Name (File : in Open_File_Type) return String;
   function Form (File : in Open_File_Type) return String;

   ...

   procedure Get (File : in Input_File_Type; Item : out Character);

   procedure Put (File : in Output_File_Type; Item : in Character);

   ...

   -- Similarly for all of the other input and output subprograms.

If tagged is in the declaration of File_Type, this is illegal.

One can always use preconditions instead, but that's a lot of extra work and
easy to omit in large interfaces.

So it would be useful to hear more about the "semantic difficulties" (I
remember there were some, but not the details). Especially as you can force
constraint checks on derived types, just not on subtypes. (So the
implementation work exists, it just isn't useful.)

****************************************************************

From: Tucker Taft
Sent: Saturday, October 21, 2017  10:00 AM

The "technical reasons" relate to the need to perform constraint checks at a
call site. This is true for dispatching operations as well -- the checks are
performed *before* dispatching to the chosen body. If we start having
dispatching operations with non-first-subtypes for parameter subtypes, then
you have to be sure that the parameters subtypes in an overriding of a
dispatching routine have exactly the same checks required at the point of
call.  This would imply defining statically matching subtypes of different
types, which seemed more of a challenge than we were prepared for when Ada 95
was designed.  Now that we have pre/postconditions, etc., we have accepted
that wrappers may be necessary in any case.  If we are willing to require
wrappers due to parameter subtype mismatches, we could probably do that, but
it could pose further efficiency challenges for implementations to avoid
wrappers when not necessary.

****************************************************************

From: Victor Porton
Sent: Saturday, October 21, 2017  11:59 AM

> Can you give some concrete examples where using (non-
> first) subtypes, perhaps with predicates, would be necessary to
> implement a given abstraction?

https://github.com/vporton/redland-bindings/blob/ada2012/ada/src/rdf-rasqal-query_results.ads

Here I define for example:

function Get_Binding_Value
  (Results: Bindings_Query_Results_Type_Without_Finalize'Class;
   Offset: Natural)
   return Literal_Type_Without_Finalize;

Here Bindings_Query_Results_Type_Without_Finalize is a subtype (with a
dynamic predicate) of Query_Results_Type_Without_Finalize. Bindings_* subtype
specializes on results which contain so called "bindings".

I would like the freedom to write instead:

function Get_Binding_Value
  (Results: Bindings_Query_Results_Type_Without_Finalize;
   Offset: Natural)
   return Literal_Type_Without_Finalize;

(without 'Class, but with a controlled argument).

Honestly speaking, this particular problems seems to be solved by using a
class-wide argument instead of a controlling argument. But in other tasks
this may probably be not a good solution.

****************************************************************

From: Steve Baird
Sent: Thursday, June 14, 2018  2:23 PM

This AI is about relaxing (in some way) the 3.9.2 rule

   In the declaration of a dispatching operation of a tagged type,
   everywhere a subtype of the tagged type appears as a subtype of
   the profile (see 6.1), it shall statically match the first subtype
   of the tagged type.

We'd like to allow something like the following example (provided by Randy):

     type File_Type is tagged limited private;

     subtype Open_File_Type is File_Type
       with Dynamic_Predicate => Is_Open (Open_File_Type);
     subtype Writable_File_Type is Open_File_Type
       with Dynamic_Predicate => Mode (Open_File_Type) = Out_File;

     procedure Put (File : Writable_File_Type; Item : String);

In order to allow this sort of thing, we have to answer (at least) two
related questions:

    1) What is the corresponding parameter subtype for the
       corresponding inherited subprogram associated with an
       extension of this type.

    2) What are the "subtype conformance" rules for overriding
       such an inherited subprogram?

More generally, if we are going to allow

      type T1 (...) is tagged ... ;
      subtype S1 is T1 ... ;
        -- may impose either constraints or predicates
      procedure Prim (X1 : S1);
        -- a dispatching operation


      type T2 (...) is new T1 with ... ;
      subtype S2 is T2 ... ;
        -- may impose either constraints or predicates
      overriding procedure Prim (X2 : S2);

then the property we want to ensure (via some appropriate compile-time rules)
is that for any value X2 of type T2,

     (X2 in S2) = (T1 (X2) in S1)

. Consider the case which is legal today, where S1 statically matches T1 and
S2 statically matches T2. The desired property certainly holds in that case
because both sides of the equation are always True.

An inelegant, but effective, way to do this is to require that S2 must be
declared as

     subtype S2 is T2 with Dynamic_Predicate => (T1 (S2) in S1);

Something like this is probably the right approach to take if we just want to
minimize complexity (both for the language definition and for compilers and
related tools). [Although we'd probably at least want to allow a subtype which
statically matches a subtype whose declaration has the prescribed form.] This
is a bare-bones solution.

However, this doesn't seem very Ada-ish. It would disallow some cases that it
would be nice to allow, such as:

      type T1 (Flag : Boolean) is tagged null record;
      subtype S1 is T1 (True);
      procedure Prim (X1 : S1);

      type T2 is new T1 with null record;
      subtype S2 is T2 (True);
      overriding procedure Prim (X2 : S2);

We could instead introduce the notion of a "statically matching descendant
subtype", defined in such a way that S2 in the above example would be a
statically matching descendant subtype of S1. The idea is that if S1 is a
subtype of a tagged type T1 and S2 is a subtype of a type T2, then "statically
matching descendant subtype" would be defined in such a way that the desired
    (X2 in S2) = (T1 (X2) in S1)
property always holds for any X2 in T2.

This could be done, but there are a lot of interactions with discriminants
that would need to be ironed out. It would get messy because there are a lot
of cases to consider; it is not clear that this is worth the effort.

For example, consider

      type T1 (D1, D2 : Integer) is tagged null record;
      subtype S1 is T1 (123, 456);
      procedure Prim (X1 : S1);

      type Intermediate (D3 : Integer) is new T1 (D1 => D3, D2 => 456);
      type T2 is new Intermediate  with null record;
      subtype S2 is T2 (D3 => 123);
      overriding procedure Prim (X2 : S2); -- legal?

In some discussions with Randy a while back I started looking at what a
definition of "statically matching descendant subtype" might look like. A
version which didn't talk about private extensions, formal types, or
predicates was already fairly complicated. We also discussed the question of
what should be done with something like

    type T1 (D : Boolean) is tagged null record;
    subtype S1 is T1 (True);
    procedure Prim (X : S1);

    type T2 is new T1 (False);

If this example is legal, then what is the subtype of the formal parameter of
T2's inherited Prim procedure?

It would be nice to avoid all this discriminant-related complexity.

This suggests an intermediate approach: relax the current
3.9.2 restriction as it applies to predicates, but not as it applies to
discriminants.

I believe that this might be the right approach to take, but I'd like to get
some feedback from the group before fleshing out the details.

****************************************************************

From: Randy Brukardt
Sent: Thursday, June 14, 2018  4:56 PM

> I believe that this might be the right approach to take, but I'd like
> to get some feedback from the group before fleshing out the details.

This sounds like a plan to me. One can (almost?) always write a discriminant
constraint as a predicate in a pinch.

Of course, that suggests that you can't quite eliminate discriminant headaches
this way. Although we might simply not care about cases like the ones you gave
above:

   type T1 (D1, D2 : Integer) is tagged null record;
   subtype S1 is T1 with
      Dynamic_Predicate => S1.D1 = 123 and S1.D2 = 456;
   procedure Prim (X1 : S1);

   type Intermediate (D3 : Integer) is new T1 (D1 => D3, D2 => 456);
   type T2 is new Intermediate  with null record;
   subtype S2 is T2 with
      Dynamic_Predicate => S2.D3 = 123;
   overriding procedure Prim (X2 : S2); -- legal?

Probably wouldn't allow this, and it wouldn't be much of a loss.

and the biggie:

   type T1 (D : Boolean) is tagged null record;
   subtype S1 is T1 with
      Dynamic_Predicate => T1.D = True;
   procedure Prim (X : S1);

   type T2 is new T1 (False);

It appears that this latter would work, but the predicate would always be
False. Not the most useful thing, but at least no semantic problem.

****************************************************************

From: Steve Baird
Sent: Friday, October 5, 2018  4:56 PM

The attached is a new, less ambitious attempt at this AI. [This is version /02
of this AI - Editor.]

Recall that Ada currently requires that if a primitive operation of a tagged
type has a parameter or function result of that tagged type, then the
parameter/result subtype must match the first subtype of the tagged type.

In particular, it cannot be subject to any discriminant constraints or
predicates that the first subtype is not subject to.

We initially looked at simply eliminating this restriction.

The interactions with discriminants turned out to be complicated.

So this latest attempt retains the restriction on discriminant constraints but
relaxes the restriction as it applies to predicates.

It also introduces a new subtype-valued attribute, Corresponding_Subtype.

This allows accepting Randy's example (which was discussed earlier)

      type File_Type is tagged limited private;

      subtype Open_File_Type is File_Type
        with Dynamic_Predicate => Is_Open (Open_File_Type);
      subtype Writable_File_Type is Open_File_Type
        with Dynamic_Predicate => Mode (Open_File_Type) = Out_File;

      procedure Put (File : Writable_File_Type; Item : String);

where an extension of File_Type which overrides the inherited Put procedure
might look like

      type My_File_Type is new File_Type with  ... ;

      overriding
      procedure Put
        (File : My_File_Type'Corresponding_Subtype (Writeable_File_Type);
         Item : String);

Thanks to Randy for some preliminary review, but (as usual) don't blame him if
you think the idea stinks or has big holes in it.

****************************************************************


Questions? Ask the ACAA Technical Agent