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

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

Le Mon, 06 May 2013 16:16:02 +0200, Dmitry A. Kazakov  
<mailbox@dmitry-kazakov.de> a écrit:
>> Theoretically. In practice, GNAT don't agree (*). It has a pragma for
>> that, `pragma Restrictions (No_Dispatching_Calls)` which should even
>> enforce it in a whole application, but seems even with this active, it
>> still requires the whole part of the runtime dedicated to it, a part  
>> which
>> depends on this part,
>
> I suppose it would be difficult to implement this so that the code used  
> to
> maintain dispatching tables and tags could be removed. It may require two
> versions of the compiler. Furthermore there are packages defining
> operations on tags which could require some of the stuff.
>
> Why do you bother? Especially, because dispatching calls are  
> deterministic
> and could be done time bounded, unless you manipulate tags. (Not  
> everything
> in people write in their guidelines for RT projects makes sense.)

That's not real‑time, that's just saving dependencies (have to be static)  
and memory (static linking easily make it big) and to be sure to know  
what's running beneath (no implicit heap allocation, no secondary stack,  
bounded stack, no output to standard I/O streams except if the program do  
it explicitly, and so on). Initially I just wanted to get ride of function  
returning unconstrained types and the exceptions runtime (I don't like  
exceptions used to return the status of an operation anyway) and keep only  
the last‑chance handler, but it appears the high level parts of the  
runtime depends on the exceptions support (ex. direct or indirect  
dependencies to Ada.Exceptions and al.). There is surely a way to get ride  
of exceptions without loosing all of the rest in the while, but I don't  
want to spend time diving in the runtime nor want to make uncertain/unsafe  
modifications, I have something else to do which can be done without  
tagging types (at the cost of some useful facilities like  
initialization/finalization).

>> However and in the large, I
>> agree with you and share the same understanding of the topic, at least
>> theoretically.
>
> There are far reaching consequences of having classes for all types.

Interfaces for all types :-D

>> (*) Don't know if SPARK agree and believe something can be proved about
>> such a system, it's a too long time I didn't use it. A quick search on  
>> the
>> web seems to show it may be possible.
>
> Yes, through global analysis. Though I would prefer a much finer approach
> when time constraints could be imposed on the interface rather than  
> checked afterwards.

SPARK is often said to be used for application with time and memory bounds  
requirement, but I don't know any way to prove timing bounds in SPARK.

> What is in the interface cannot be decided before you have
> interfaces properly articulated. Thus type system overhaul is the first
> step to make.

Saying “overhaul”, you will always get this reply: “no way, don't break  
compatibility” (something which in the meanwhile is easily understood).  
May be there would be a hope to do something similar to what SPARK did,  
just with bigger consequences, re‑factoring Ada outside of Ada (which is  
unavoidable to go ahead without fears to break compatibility).

> Without doing that you get only mess.
> See Ada 2012 dynamic
> pre-/postconditions as an example.

I did not encountered any real mess so far with dynamic pre/post  
condition. The only grief I have with it, is that it makes no distinction  
between sub‑program used for pre/post conditions and sub‑programs used for  
the program. Occasionally, that may lead to contradictions or impossible  
design. I would like a way to permit to restrict some sub‑programs for use  
with pre/post conditions only and disallow their use from the program  
proper (just like you have to separate meta‑language and object‑language,  
even when both shares the same vocabulary and grammar). At least, and  
external language like SPARK annotations is, does not suffers from this  
confusion: a predicate may be expressed in terms of Ada entities, but is  
not imposed to be entirely expressed in these terms and never injects  
anything into the program (sorry for digressing (red‑face)).


-- 
“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