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

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

On 13-05-12 09:44 , Yannick Duchêne (Hibou57) wrote:
> Le Sat, 11 May 2013 23:06:25 +0200, Niklas Holsti
> <niklas.holsti@tidorum.invalid> a écrit:
> 
>>    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.
> 
> Additionally to the idea you suggested, that may also suggest to use a
> function instead of a procedure with in/out parameter, with a new
> declaration for each of the important state changes which would become
> clearly visible (still what if this already was a function already
> returning something… Ada functions can return only one single element).

You mean like this:

   function Open  (File : in Closed_File) return Open_File;
   function Close (File : in Open_File  ) return Closed_File;

I agree that this is a possible approach. This would work, but at the
cost of writing the parameter/object name twice in each call:

   File : File_Object;
   ...
   File := Open (File);
   File := Close (File);

But this code seems to cause a problem:

   File1, File2 : File_Object;
   ...
   File1 := Open (File1);
   File2 := Close (File1);

Now File2 is a clone of File1, and the underlying system file is closed,
but File1 still considers it open. (This may of course be acceptable to
the specific underlying system and not lead to an error, but in general
I believe that such side-effects could be problematic.)

The "function" approach thus tends to clone objects, and to lose the
"object identity".

If we want to preserve object identity under that approach, I think we
need a "linear type system"
(http://en.wikipedia.org/wiki/Linear_type_system) in which each variable
can be used exactly once. However, every use (e.g. as a parameter to a
function) can produce a new incarnation of the object (the function
return value), which can be assigned to a new variable, so the object
lives on. However, this would be a BIG change to the language.

> There is now the question about compilers: are compilers clever enough
> to statically catch subtype miss‑match in such a use cases and give
> warnings (I believe no),

I think that if this issue of subtype matching comes to be considered
important, compiler writers could give it more attention, and
conservative (but incomplete) static-analysis solutions could be
implemented with current technology.

> and are compilers clever enough to optimize out
> multiple object declaration into a single one, changing its subtype (I
> believe no, too),

Those problems are solved by a linear type system. But I agree with you
that it is too much to expect that the compiler would automatically
implement an Ada-like program using linear typing behind the scenes.

> Another issue with subtype, is that it requires the `File_Object` full
> definition to be public, or else, there is no way to define a subtype of
> it as the example do (no opaque type).

Yes, that could be a problem. The language might allow the declaration
of subtypes of opaque types, with opaque constraints. That does not seem
too hard to implement if the type and subtypes are fully defined in the
private part of a package, but it seems more difficult if the full type
declaration is deferred (through an access type) to the package body.

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