Re: Ada requires too much typing!

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

Le Thu, 10 Jun 2010 10:07:17 +0200, Dmitry A. Kazakov  
<mailbox@dmitry-kazakov.de> a écrit:
>> What would become formal parameters, like type parameters ?
>
> Base types, class-wide types.
>
>> Overloading
>> functions returning type derived from that of the ancestor one ? OK. So,
>> this will require an original bas type in the root definition which  
>> could
>> be wide enough to reach actual capabilities of generics. An “ANY” type
>> (like in QBasic) ?
>
> Nope. The element of a stack is not just any type. It is a copyable type
> (the class "private" in terms of Ada generics).
>
>> An abstract base type ? OK. So, now, we will need to be
>> able to declare abstract base type, that is, abstract discrete types,  
>> etc.
>> Is that what's in your mind ?
>
> Yes. These are abstract interfaces to be defined. This is an easy part  
> BTW.
What about “not every thing in the same bag” philosophy ? (many others  
failed in this trap) Moving generics to dynamic polymorphism... would be  
dynamic polymorphism where there was a kind of static polymorphism. And  
this is not the same from the point of view of program proof you like so  
much (me too, I like).

Is there some kind of meta-class in you idea of a new modal ? (generics  
can define new types and thus can initiate new class of types, you will  
meta-class to achieve the same).

-- 
There is even better than a pragma Assert: a SPARK --# check.
--# check C and WhoKnowWhat and YouKnowWho;
--# assert Ada;
--  i.e. forget about previous premises which leads to conclusion
--  and start with new conclusion as premise.