Re: Seeking for papers about tagged types vs access to subprograms

[Niklas Holsti <niklas.holsti@tidorum.invalid>]

On 13-05-11 03:18 , Randy Brukardt wrote:
> "Niklas Holsti" <niklas.holsti@tidorum.invalid> wrote in message 
> news:av4r5qFitfiU1@mid.individual.net...
>> On 13-05-10 06:29 , Yannick Duch�ne (Hibou57) wrote:
>>> Le Fri, 10 May 2013 00:19:14 +0200, Randy Brukardt
>> ...
>>>> Yes, because we need to move beyond typing to other forms of static 
>>>> error
>>>> detection. Typing is too rigid to do a good job -- you need to include
>>>> statically known information about the contents of variables and
>>>> parameters,
>>>> which can change from line-to-line in a program.
>>>
>>> I feel the same. I often though typing can't do everything if it comes
>>> with value type checking, while in some occasions, I tried to express
>>> each validity condition with types and then type checking (that ends to
>>> be crazy, indeed). A simple example, is paired invocation, where
>>> whenever a sub-program is is invoked, sooner or later, another
>>> sub-program must be invoked too on the same argument, ex. like `Open`
>>> and later `Close`. This cannot be expressed with types and indeed
>>> requires assertions.
>>
>> Are you familiar with the "typestate" concept? As I understand it, the
>> intent is to check state-sequence rules such as Open-followed-by-Close.
>> See http://en.wikipedia.org/wiki/Typestate_analysis.
> 
> Thanks for the reference. I doubted that the idea was new (there are no new 
> ideas), but I hadn't heard of it before.

I'm not sure if "typestate" matches all of what you were describing or
thinking of -- I meant it only as a pointer to Yannick for things like
the Open-Close protocol example. But if it resonates with your thinking,
good.

> I don't like the name much, because 
> it feeds into the "type is everything" madness that Dmitry exhibits so 
> clearly. This clearly (just like constraints and predicates) is something 
> that's added in addition to type analysis; it's not part of it at all.

I haven't studied typestate analysis at all deeply. I had a look at the
"Plaid" language referenced from the Wikipedia article, at
http://www.cs.cmu.edu/~aldrich/plaid/, and was a bit surprised to
understand that Ada subtypes come rather close to it, in particular
subtypes of discriminated record types with variants. The value of the
discriminant represents the state, with certain components of the record
(= attributes of the object or type) existing or not existing depending
on the variant selected by the discriminant.

For the Open-Close example:

   type File_State is (Is_Closed, Is_Open);

   type File_Object (State : File_State := Is_Closed) is
   record
      case State is
      when Is_Closed => null;
      when Is_Open   => Handle : System.IO.File_Handle;
      end case;
   end record;

   subtype Closed_File is File_Object (State => Is_Closed);
   subtype Open_File   is File_Object (State => Is_Open  );

By using subtypes on formal parameters, we can indicate that the
available operations on a File_Object depend on the actual subtype
(i.e. the state), except for one deficiency, on which more below.

First, reading and writing is possible only for open files:

   procedure Read  (File : in Open_File; ...)
   procedure Write (File : in Open_File; ...)

Second, a Closed file can be Opened, and an Open file can be Closed:

   procedure Open  (File : in out Closed_File);
   procedure Close (File : in out Open_File  );

The problem here is that these operations should change the subtype of
the "in out" parameter: Open changes the File from Closed_File to
Open_File, and Close changes it from Open_File to Closed_File. However,
Ada does not let us specify such changes, in the subprogram profile.
(This can of course be specified with pre- and post-conditions, but I'm
looking for a closer connection between the subprogram profile and the
subtypes.)

Well, why is Ada limited in this way? There is no real reason why an "in
out" parameter should have the same constraints on input and on output.
So let us extend Ada to allow different "in" and "out" subtypes:

   -- Extended Ada:
   procedure Open  (File : in Closed_File out Open_File  ; ...);
   procedure Close (File : in Open_File   out Closed_File; ...);

This gives us exactly the open/close typestate example. A compiler with
strong value-range analysis should then be able to deduce, for example,
that the "in" constraint check on a particular call of Open, Close,
Read, or Write always succeeds (= typestate correctness) or may or must
fail (various degrees of typestate incorrectness). I believe that many
current compilers could do such value-range analysis, and thus Ada could
support this kind of typestate concept with rather small language changes.

(You may ask: if an "in out" parameter has different "in" and "out"
subtypes, what subtype is applied when the formal parameter is used or
assigned within the subprogram body? I think the logical answer would be
the "disjunctive subtype" that represents the union of the "in" and
"out" subtypes, which unfortunately could be a subtype with "holes". But
I think that would be manageable, since this disjunctive subtype would
have at most two separate components, i.e. at most one hole.)

-- 
Niklas Holsti
Tidorum Ltd
niklas holsti tidorum fi
      .      @       .