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

["Yannick Duchêne (Hibou57)" <yannick_duchene@yahoo.fr>]

Le Wed, 08 May 2013 12:23:06 +0200, Dmitry A. Kazakov  
<mailbox@dmitry-kazakov.de> a écrit:

> On Wed, 08 May 2013 11:39:23 +0200, Yannick Duchêne (Hibou57) wrote:
>
>> But then, an example such as the above would present challenge with
>> derived types.
>
> That is the main question about parallel hierarchies: if you derive or
> constrain one type in the cloud, what happens with other types? Does this
> produce new types, related or unrelated, constrained or not.

I would say there is no general answer without additional informations  
about what the whole means, and no language or its compiler can tell it in  
place of the author (or else, you decide in place of the author, and are  
back to what it actually is). And that additional informations is may be  
what needs to be provided (and the basic type system, as it is actually,  
does not allow it), ex. kind of basic axiomatization describing what the  
relations must preserve for the whole to be valid. This axiomatization  
could answer two questions, directly: is the system with its new  
parameters still valid? indirectly: is the the new system compatible with  
other similar systems or the one from which it is derived? Whether or not  
this axiomatization would be sound, would be the author's responsibility  
(that's why it should be simple, like based on basic relations on discrete  
types and interfaces). Any way, lack of soundness may ends in failure to  
check.

A basic idea (more easy to say than to do): reuse things like  
pre/post/pragma‑assert, but whose purpose is to be statically checked (if  
it's too complicated to be checked, it means it fails, and it is not  
deferred to a run‑time check). The author would decide what he/she wish to  
put in these. The language could impose some minimal constraints with base  
predefined types (like it already do rather well) so there could be no way  
to relax everything.

This may looks going too far, but I believe minimal axiomatization  
(statically checked) would be nice; not necessarily to prove a program  
(another story), but at least to ensure what it is based on (the types and  
use of their instances) is valid in some regards. What the program would  
do with it at runtime may be another story and still be a job for SPARK  
and others  (too much constraints here, would defeat any achievement).

Also to digress but still in some way related, more control on what can be  
done of an instance of a type, toward restricting, permitting to deny the  
use of some part of an interface, would help to make valid assertions (ex.  
with my issue where I'm lacking a limited access type, if I could restrict  
to limited access type, I could not only ensure no access is made to a  
deallocated storage, but could even have some assertions about aliasing).

-- 
“Syntactic sugar causes cancer of the semi-colons.” [1]
“Structured Programming supports the law of the excluded muddle.” [1]
[1]: Epigrams on Programming — Alan J. — P. Yale University