Re: Why no Ada.Wide_Directories?

["Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de>]

On Thu, 20 Oct 2011 17:54:28 +0200, Yannick Duch�ne (Hibou57) wrote:

> Le Thu, 20 Oct 2011 16:31:59 +0200, Dmitry A. Kazakov  
> <mailbox@dmitry-kazakov.de> a �crit:

>> What I know is that the decomposition shall go along the types.
> You use to say you don't feel FP good, but I sware, I am sure you would  
> enjoy some part of it ;)

No, FP is just too low level: procedural decomposition. Type systems
correspond to the categories - a better and more capable mathematics =>
safer design. Another fundamental problem of FP is a wrong premise about
being stateless. Computing is solely about states. You run a program to
have its side effects, there is no other reason for doing that.

>> Implementation must be absolutely free too
>> choose. There shall be no procedures but operations on types. All types
>> shall have classes.

> What's missing from Interface type introduced with Ada 2005 ?

1. Most Ada types do not have interfaces
2. Ada interface cannot be inherited from a concrete type
3. Ada interface cannot have implementation
4. Ada interface does not support ad-hoc supertypes

> Doesn't it  
> fulfill the above expectations ? (also keep in mind sometime efficiency is  
> required, and if you want place formalism over efficiency, then you have  
> to sacrifice efficiency, conscientiously).

Not an issue. Scalar types may have interfaces at zero time/space cost. You
don't need to embed tag into by-value types.

>> Any syntax sugar (prefix notation, infix operations,
>> assignments, indexing, member extraction, aggregates, entries,  
>> attributes) shall be operations.
> Are you sure you are not confused between concrete syntax and abstract  
> syntax ?

I don't understand this. The problem is that, for example, for the record
type T and its member A, the ".A" is not the operation of T, because record
is not an interface. A'First is not an operation of array. ":=" is not an
operation (doubly dispatching) of its left and right sides etc.

>> Construction model must be type safe (in particular,
>> each type must have constructors, including class-wide types). The type
>> system shall support both specialization and generalization.

> Could you provide an example case of generalization you have in mind ?

Examples are:

1. Type extension (e.g. upon derivation, present in Ada)
2. Expansion of enumeration types
3. Cartesian product of types, e.g. Real x Real -> Complex
4. Lifting constraints, e.g. Float -> IEEE Float (number + NaN + +Inf ...)
5. Ad-hoc supertypes, e.g. String U Unbounded_String -> General_String,
creating new classes from existing ones by union.
 
>> The programmer should be able to enforce static type and constraint checks, in  
>> particular, to convert any potentially dynamic checks into compile-time errors. All
>> exceptions must be typed, contracted and statically checked.

> This is not a language topic, instead, a technology level topic. I feel  
> runtime check is a reasonable fall-back for what cannot be statically  
> checked in th actual state of the technology.

No, it is inconsistent and unreasonable. Static checks are meant to detect
bugs. Bug is either there or not, independently on whether the program is
running, not running, will ever run. It is just not a function of the
execution state. Bug is a property of the program and all its possible
sates as a whole. A program cannot be both correct and incorrect. A program
checking itself as wrong is a Cretan Liar.

> If you really require static  
> check, then you must restrict yourself to what can be statically checked.

Yes, and I want a firewall between static and dynamic checks. If some
proposition is declared statically true or false, while the compiler is
unable to prove it, that should make the program illegal. The programmer
must be forced to chose, and if it decides for a static check he must be
sure that the compiler indeed verified his assumption or else have to
change the program.

> If Ada 2012 defines some Design by Contract checks as runtime check, this  
> is not a language flaw, a pragmatic choice.

Yet another generator of arbitrary exceptions. Lessons from accessibility
checks not learned...

> Along with that, if a compiler  
> is able to statically check what Ada 2012 designate as runtime check, then  
> nothing in the language definition disallows the compiler to apply all  
> static checks it is able to.

See above, it is the difference between an illegal program and a program
raising exceptions, nothing in common.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de