Seeking for papers about tagged types vs access to subprograms

[Yannick Duchêne (Hibou57)]

Hi people,

As the thread's title tells, I'm seeking for papers exposing thoughts
about the compared use of tagged types and access to sub‑programs. I know
the page from the Ada 95 Style Guide [1], but it's not verbose enough to
me. I already have some opinions on the topic, however also believe I have
not enough background.

I welcome any other pointers if anyone know ones, preferably with real
life use‑cases where both options were compared, as well as formal
analysis.

As an additional aside but related question, I'm also interested in the
question in the particular context of storage‑pools, which use tagged
types instead of simple sub‑program designated by some attributes or
operator overloading (I imagine simple sub‑programs could have been an
option for the `new` operator, just like for the other operators).

[1]:
http://www.adaic.org/resources/add_content/docs/95style/html/sec_5/5-3-4.html

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

[Yannick Duchêne (Hibou57)]

Le Sun, 28 Apr 2013 07:14:15 +0200, Yannick Duchêne (Hibou57)
<yannick...@yahoo.fr> a écrit:

> As an additional aside but related question, I'm also interested in the
> question in the particular context of storage‑pools, which use tagged
> types instead of simple sub‑program designated by some attributes or
> operator overloading (I imagine simple sub‑programs could have been an
> option for the `new` operator, just like for the other operators).

Same question in the context of `Ada.Finalization`. Similar semantic could
have been made available without requiring tagged types.

[Shark8]

On Monday, April 29, 2013 6:31:37 PM UTC-6, Hibou57 (Yannick Duchêne) wrote:
>
> Same question in the context of `Ada.Finalization`. Similar semantic could
> have been made available without requiring tagged types.

This is true; but it's likely that tagged-types were the easiest method to implement it.

[Yannick Duchêne (Hibou57)]

Le Tue, 30 Apr 2013 02:41:35 +0200, Shark8 <onewing...@gmail.com> a
écrit:

I don't know if this was the easiest, but I personally feel this may be
was the option offering the biggest use‑case coverage.

I though relying on tagged type allowed to be the most general as
possible. Defining an `Ada.Finalization` applicable to tagged types,
obviously requires tagged types. On the other hand, as what's not using
tagged type, may be redefined with little modification, to use tagged
types, using tagged types was the best option to cover the most general
case, even the ones not using tagged types in the first place.

However, tagged types may be excluded (ex. if there are proof
requirements) or not available (ex. the runtime in use does not support
it). That's a bit a pity to not be able to use something like
`Ada.Finalization` for applications not using tagged types. I even believe
`Ada.Finalization` is harder to avoid than tagged types
(`Ada.Finalization` looks more fundamental to me), especially that it
comes with added safety (as much as strong typing and ability to return
unconstrained types are).

[Randy Brukardt]

"Yannick Duch�ne (Hibou57)" <yannick...@yahoo.fr> wrote in message
news:op.wv8jh1c1ule2fv@cardamome...
...

>As an additional aside but related question, I'm also interested in the

>question in the particular context of storage-pools, which use tagged
>types instead of simple sub-program designated by some attributes or
>operator overloading (I imagine simple sub-programs could have been an

>option for the `new` operator, just like for the other operators).

Nitpick: "new" is not an operator, it is an *operation*, things whose
behavior cannot be modified directly. Like membership, it would be hard to
make "new" an operator because one of the arguments can be a type (rather
than an object or value), and it's hard to see how that could be mapped to
an Ada function. (Adding type parameters seems over the top.)

Randy.

[Randy Brukardt]

"Yannick Duch�ne (Hibou57)" <yannick...@yahoo.fr> wrote in message

news:op.wwbw2ho9ule2fv@cardamome...
...

>However, tagged types may be excluded (ex. if there are proof
>requirements) or not available (ex. the runtime in use does not support
>it). That's a bit a pity to not be able to use something like
>`Ada.Finalization` for applications not using tagged types. I even believe
>`Ada.Finalization` is harder to avoid than tagged types
>(`Ada.Finalization` looks more fundamental to me), especially that it
>comes with added safety (as much as strong typing and ability to return
>unconstrained types are).

My understanding is that safety-critical people are scared of anything that
has implicit behavior (like Finalization or dispatching). As such, there
isn't much value to having them separated as the people that can't use the
one probably can't use the other as well. And outside of such restricted
environments, there's not value to avoiding tagged types.

It should be noted that finalization on all types had some semantic problems
(such as finalization on by-copy parameter passing - which would make it
hard to call a procedure Finalize without infinite regress) which were
solved by limiting the capability to tagged types. Whether there was a
better solution is hard to say at this distance -- keep in mind that the
prevailing feeling among the reviewers was that the general finalization you
are talking about was too complex for the Ada 95 definition. A small group
of die-hards (which I somehow got the reputation of being the leader of),
convinced Tucker to try again with a simpler model -- which turned into the
tagged model we have today.

So my point is the that the question is not whether general finalization
would have been better than tagged-type only finalization. It was whether
tagged-type only finalization was better than nothing, because there was no
chance of the general finalization being in Ada 95. Finalization is far too
important for us to have waited another 12 years to get it, so what we've
got is the best that we could have gotten.

Randy.

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

[Jeffrey Carter]

On 05/01/2013 06:18 PM, Randy Brukardt wrote:
>
> So my point is the that the question is not whether general finalization
> would have been better than tagged-type only finalization. It was whether
> tagged-type only finalization was better than nothing, because there was no
> chance of the general finalization being in Ada 95. Finalization is far too
> important for us to have waited another 12 years to get it, so what we've
> got is the best that we could have gotten.

To my mind, since in Ada 83 records were the only types with user-defined
default initialization, it made sense for them also to be the only types with
user-defined finalization. So I think that limiting finalization to record types
should have been a 3rd option.

--
Jeff Carter
"I would never want to belong to any club that
would have someone like me for a member."
Annie Hall
41

[Dmitry A. Kazakov]

On Wed, 1 May 2013 20:09:46 -0500, Randy Brukardt wrote:

> "Yannick Duch魥 (Hibou57)" <yannick...@yahoo.fr> wrote in message

type Root_Access_Type is interface ...;
function "new" return Root_Access_Type is abstract;

If access types were "untagged" class, "new" would be a plain primitive
operation.

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

[Randy Brukardt]

"Dmitry A. Kazakov" <mai...@dmitry-kazakov.de> wrote in message
news:1d73jn954z90t.ze60axadntyr$.dlg@40tude.net...

> On Wed, 1 May 2013 20:09:46 -0500, Randy Brukardt wrote:

...

>> Nitpick: "new" is not an operator, it is an *operation*, things whose
>> behavior cannot be modified directly. Like membership, it would be hard
>> to
>> make "new" an operator because one of the arguments can be a type (rather
>> than an object or value), and it's hard to see how that could be mapped
>> to
>> an Ada function. (Adding type parameters seems over the top.)
>
> type Root_Access_Type is interface ...;
> function "new" return Root_Access_Type is abstract;
>
> If access types were "untagged" class, "new" would be a plain primitive
> operation.

You're missing something here, and that's the information about the
designated type/object. If you have:

Ptr := new Piece (Color => Black);

that information about the discriminant has to be transmitted somehow as it
can controls the size of the allocated object. The same is true of initial
values. In a strongly-typed system, these things can't be separated (you
could of course pass the size as a parameter but that would be untyped, as
there would be no way to ensure that the correct size is passed for the
initial value). Besides, if you wanted that, you could use storage pools;
the point was that there is no way to directly model an allocator as an
operator call (which is necessarily a normal function call). Using some
other form of call is not how operators work (we have the term "operation"
for that).

Similar thoughts apply to memberships like "obj in T'Class". One might be
able to write a function to implement that, but you'd have to pass tags to
do so, which would bear no resemblance to normal subprogram call (it would
be much more like the relationship of a storage pool to an allocator).

Randy.

[Dmitry A. Kazakov]

On Thu, 2 May 2013 16:49:18 -0500, Randy Brukardt wrote:

> "Dmitry A. Kazakov" <mai...@dmitry-kazakov.de> wrote in message
> news:1d73jn954z90t.ze60axadntyr$.dlg@40tude.net...
>> On Wed, 1 May 2013 20:09:46 -0500, Randy Brukardt wrote:
> ...
>>> Nitpick: "new" is not an operator, it is an *operation*, things whose
>>> behavior cannot be modified directly. Like membership, it would be hard to
>>> make "new" an operator because one of the arguments can be a type (rather
>>> than an object or value), and it's hard to see how that could be mapped to
>>> an Ada function. (Adding type parameters seems over the top.)
>>
>> type Root_Access_Type is interface ...;
>> function "new" return Root_Access_Type is abstract;
>>
>> If access types were "untagged" class, "new" would be a plain primitive
>> operation.
>
> You're missing something here, and that's the information about the
> designated type/object. If you have:
>
> Ptr := new Piece (Color => Black);
>
> that information about the discriminant has to be transmitted somehow as it
> can controls the size of the allocated object.

Yes, but my response was to your point about the object's type. You don't
need explicit types with primitive operations, provided, the result is
properly typed. In all cases where Ada 83 used [sub]type specification:

T'Image (X)
new T (X)
T (X)

etc, this was because of lack of typing.

Regarding discriminants, this is not a problem, because the signature of
the predefined "new" would be generated by the compiler, which could
include necessary parameters as it does now.

BTW, for constructors and allocators, there could a [sub]type attribute
T'Constraints which would yield a null record type with the discriminants
of T. E.g. let

type Foo (X : Integer; Y : Boolean) is record
I : Integer
end record;

then Foo'Constraints is

type Foo'Constraints (X : Integer; Y : Boolean) is null record;

This type + a mechanism to flatten tuples would give the signature you
wanted for "new" without compiler magic.

> Similar thoughts apply to memberships like "obj in T'Class". One might be
> able to write a function to implement that, but you'd have to pass tags to
> do so, which would bear no resemblance to normal subprogram call (it would
> be much more like the relationship of a storage pool to an allocator).

To me X in T and X in T'Class are syntax sugar for operations on tags:

X in T <=> X'Tag = T'Tag
X in T'Class <=> X'Tag <= T'Tag (tree order)

[Yannick Duchêne (Hibou57)]

Le Tue, 30 Apr 2013 02:31:37 +0200, Yannick Duchêne (Hibou57)

<yannick...@yahoo.fr> a écrit:

> Le Sun, 28 Apr 2013 07:14:15 +0200, Yannick Duchêne (Hibou57)
> <yannick...@yahoo.fr> a écrit:
>> As an additional aside but related question, I'm also interested in the
>> question in the particular context of storage‑pools, which use tagged
>> types instead of simple sub‑program designated by some attributes or
>> operator overloading (I imagine simple sub‑programs could have been an
>> option for the `new` operator, just like for the other operators).
>
> Same question in the context of `Ada.Finalization`. Similar semantic
> could have been made available without requiring tagged types.
>

I also looked at the RM about user‑defined indexing, and could not find a
reason why it is legal for tagged types only. May be I will understand a
future day why it requires a tagged type, so far, it makes me feel it's
lacking orthogonality.

Or else, may be it suggest types should rather be tagged by default but
the primitives ones or derived from the primitive ones.

[Dmitry A. Kazakov]

On Mon, 06 May 2013 12:00:25 +0200, Yannick Duch�ne (Hibou57) wrote:

> Or else, may be it suggest types should rather be tagged by default

No. All untagged types should have untagged classes.

Indexing is just an interface to inherit from.

Neither Ada 2020 nor Ada 2120 will make it right before fixing the type
system first.

[Yannick Duchêne (Hibou57)]

Le Mon, 06 May 2013 12:18:40 +0200, Dmitry A. Kazakov
<mai...@dmitry-kazakov.de> a écrit:

> On Mon, 06 May 2013 12:00:25 +0200, Yannick Duchêne (Hibou57) wrote:
>
>> Or else, may be it suggest types should rather be tagged by default
>
> No. All untagged types should have untagged classes.

If I understand you correctly, that was something very close I was
thinking about when reading the RM page about user‑defined indexing (and
other tagged‑types only allowed features), I just though “so, why not
considerer untagged types has a fixed static class (*) and on that basis,
naturally allow the same definitions to be applied to untagged types”.
While some features are defined for tagged types only, no requirement is
never made any where for these same tagged types to be derived, so it
could be defined for untagged types as well (or else I am missing
something).

(*) class with no dispatching or deterministic dispatching, so would be
untagged, indeed, if I understand you correctly.

I feel the status distinction between tagged and untagged types as an
issue in some ways, this breaks something in the big picture, and break
Ada, the language, in two too much distinct and foreign parts. That's not
that I'm against tagged types, just that I would prefer to not force the
use of tagged types (hence the “lack of orthogonality”); tagged are
sometime nice, sometime not nice, that depends on the area, on the
requirements, …, both should be treated equally with regards to primitives
and constructs, except for any primitives and construct which would
*requires* there are indeed tagged (non‑deterministic members and
sub‑programs) classes (like any operations which involves classes, as an
immediate example).

[Dmitry A. Kazakov]

On Mon, 06 May 2013 12:55:31 +0200, Yannick Duchêne (Hibou57) wrote:

> Le Mon, 06 May 2013 12:18:40 +0200, Dmitry A. Kazakov
> <mai...@dmitry-kazakov.de> a écrit:
>
>> On Mon, 06 May 2013 12:00:25 +0200, Yannick Duchêne (Hibou57) wrote:
>>
>>> Or else, may be it suggest types should rather be tagged by default
>>
>> No. All untagged types should have untagged classes.
>
> If I understand you correctly, that was something very close I was
> thinking about when reading the RM page about user‑defined indexing (and
> other tagged‑types only allowed features), I just though “so, why not
> considerer untagged types has a fixed static class (*) and on that basis,
> naturally allow the same definitions to be applied to untagged types”.
> While some features are defined for tagged types only, no requirement is
> never made any where for these same tagged types to be derived, so it
> could be defined for untagged types as well (or else I am missing
> something).

Perhaps that this feature (static classes) existed since Ada 83.

http://www.adahome.com/rm95/rm9x-N.html

Pos. 6.

What is needed is dynamic classes for untagged types with articulated
interfaces. Operations on a class-wide object will dispatch as usual. Ada
83 classes were implicit. The interface was not stated but described
informally in the RM. That is because there is no language means to
describe such interfaces (integers, reals, arrays, records, tasks etc).
Tagged types were first in Ada to have explicit used-defined interfaces.

> (*) class with no dispatching or deterministic dispatching, so would be
> untagged, indeed, if I understand you correctly.
>
> I feel the status distinction between tagged and untagged types as an
> issue in some ways, this breaks something in the big picture, and break
> Ada, the language, in two too much distinct and foreign parts.

Yes it does. That was a flaw of Ada 95 design. I guess it was the maximum
of what Tucker Taft could press through fierce opposition. Little changed
since then. You will find a lot of people praising "orthogonality" of
tagged types, which was nothing but a language design fault, an ugly
compromise.

> That's not
> that I'm against tagged types, just that I would prefer to not force the
> use of tagged types (hence the “lack of orthogonality”); tagged are
> sometime nice, sometime not nice, that depends on the area, on the
> requirements, …, both should be treated equally with regards to primitives
> and constructs, except for any primitives and construct which would
> *requires* there are indeed tagged (non‑deterministic members and
> sub‑programs) classes (like any operations which involves classes, as an
> immediate example).

There is nothing non-deterministic in tagged types. All calls with specific
objects are statically resolved. Dynamic are only dispatching calls
involving class-wide objects. It should work exactly same with "untagged"
classes. BTW, there will be no problem to have mixed cases. There seems to
be nothing wrong in inheriting from both a tagged and an untagged
interfaces. There result would be tagged, of course.

[Yannick Duchêne (Hibou57)]

Le Mon, 06 May 2013 14:11:32 +0200, Dmitry A. Kazakov
<mai...@dmitry-kazakov.de> a écrit:

>> I feel the status distinction between tagged and untagged types as an
>> issue in some ways, this breaks something in the big picture, and break
>> Ada, the language, in two too much distinct and foreign parts.
>
> Yes it does. That was a flaw of Ada 95 design. I guess it was the maximum
> of what Tucker Taft could press through fierce opposition.

Fierce opposition from who? For what reasons? What did Tucker initially
wanted?

> There is nothing non-deterministic in tagged types. All calls with
> specific objects are statically resolved. Dynamic are only dispatching
> calls
> involving class-wide objects.

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, which depends on this other part, and so on (forgive
me for having this kind of matter in mind, I know that's not the best to
drive a decision, I just have to do with it). However and in the large, I
agree with you and share the same understanding of the topic, at least
theoretically.

(*) 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.

> It should work exactly same with "untagged"
> classes. BTW, there will be no problem to have mixed cases. There seems
> to be nothing wrong in inheriting from both a tagged and an untagged
> interfaces. There result would be tagged, of course.

Agree.

[Dmitry A. Kazakov]

On Mon, 06 May 2013 15:16:21 +0200, Yannick Duch�ne (Hibou57) wrote:

> Le Mon, 06 May 2013 14:11:32 +0200, Dmitry A. Kazakov

> <mai...@dmitry-kazakov.de> a �crit:

>>> I feel the status distinction between tagged and untagged types as an
>>> issue in some ways, this breaks something in the big picture, and break
>>> Ada, the language, in two too much distinct and foreign parts.
>>
>> Yes it does. That was a flaw of Ada 95 design. I guess it was the maximum
>> of what Tucker Taft could press through fierce opposition.
>
> Fierce opposition from who? For what reasons? What did Tucker initially
> wanted?

I wasn't there.

>> There is nothing non-deterministic in tagged types. All calls with
>> specific objects are statically resolved. Dynamic are only dispatching
>> calls involving class-wide objects.
>
> 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.)

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

> (*) 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. What is in the interface cannot be decided before you have
interfaces properly articulated. Thus type system overhaul is the first
step to make. Without doing that you get only mess. See Ada 2012 dynamic
pre-/postconditions as an example.

[Yannick Duchêne (Hibou57)]

Le Mon, 06 May 2013 16:16:02 +0200, Dmitry A. Kazakov
<mai...@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)).

[Dmitry A. Kazakov]

On Mon, 06 May 2013 17:15:36 +0200, Yannick Duchêne (Hibou57) wrote:

> Le Mon, 06 May 2013 16:16:02 +0200, Dmitry A. Kazakov
> <mai...@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).

I don't see how dispatching calls could be relevant to these constraints
which apply to both dispatching and specific calls. Dispatching call is a
bogeyman under the bed.

> 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.).

Instead of banishing exceptions one should put contracts on them.

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

Yes, this is more or less same as having classes.

>> 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).

Usual hand waving used by people who don't want to discuss it seriously.
And they do not.

> 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).

I thought about it, but this is far larger than one-man project and there
is too much things which nobody did before and nobody knows how to do.
Before doing this one should clearly understand it, and before
understanding it there should be a serious discussion about it. And before
that starts there should be a desire in the community to fix the language,
which is clearly absent. Ada 2012 became a patchwork under which one can
barely see its original ideas.

[Adam Beneschan]

On Monday, May 6, 2013 11:55:34 AM UTC-7, Dmitry A. Kazakov wrote:

> Instead of banishing exceptions one should put contracts on them.

Am I still in comp.lang.ada, or did I wander into arts.movies.godfather by mistake? :) :) :)

-- Adam

[Randy Brukardt]

"Yannick Duch�ne (Hibou57)" <yannick...@yahoo.fr> wrote in message
news:op.wwnp2zkrule2fv@cardamome...
...
>I also looked at the RM about user-defined indexing, and could not find a

>reason why it is legal for tagged types only. May be I will understand a
>future day why it requires a tagged type, so far, it makes me feel it's
>lacking orthogonality.

It's simply a matter of practicality. We considered allowing them for all
non-array types, but the problem is that you don't know whether a particular
type is an array type unless you break privacy (a huge no-no for Legality
Rules). And then you get into the problem of having both predefined and
user-defined indexing for a particular type, and which one is used in a
particular case. You can invent some really insane cases by using the
"additional operation" rules (where indexing might only appear in the body
or other very late points). Steve Baird had some head-exploding examples.

We avoided the entire problem by only allowing this on tagged types, as
there are no tagged array types.

It's not a perfect solution, but its the most we could practically do for
Ada 2012 (if this was any more complex, it would have been deep-sixed, that
is, killed).

As a practical matter, I think almost all new composite types ought to be
derived from Controlled (or Limited_Controlled), meaning that they're
tagged, so this restriction doesn't matter much. (The idea of indexing a
numeric type is silly, array types don't need user-defined indexing, and
nobody should be declaring visible access types anyway, so nothing is left.)
YMMV.

Randy.

[Randy Brukardt]

"Yannick Duch�ne (Hibou57)" <yannick...@yahoo.fr> wrote in message

news:op.wwny5jerule2fv@cardamome...

Le Mon, 06 May 2013 14:11:32 +0200, Dmitry A. Kazakov

<mai...@dmitry-kazakov.de> a �crit:

>> Yes it does. That was a flaw of Ada 95 design. I guess it was the maximum
>> of what Tucker Taft could press through fierce opposition.
>
>Fierce opposition from who? For what reasons? What did Tucker initially
>wanted?

WG 9 thought that Ada 95 had grown way too large and was too much of a
change. That led to the infamous "scope reduction", where many important
things were thrown out (including finalization). The Ada 9x team snuck
several of the ideas back in toward the end (including finalization,
renaming of library units, and more), and some of the other ideas have
resurfaced in more recent versions of Ada.

I'm of the opinion that WG 9 was right, in that the market could only handle
so much change to Ada. We lost many compiler vendors at that time as it was,
we might have ended up with none if the language had been too ambitious.
OTOH, the cutting probably went a bit too far.

Randy.

[Yannick Duchêne (Hibou57)]

Le Tue, 07 May 2013 03:14:28 +0200, Randy Brukardt <ra...@rrsoftware.com>
a écrit:

> We lost many compiler vendors at that time as it was,
> we might have ended up with none if the language had been too ambitious.

OK, I see.

[Dmitry A. Kazakov]

(:-))

[Dmitry A. Kazakov]

On Mon, 6 May 2013 20:09:46 -0500, Randy Brukardt wrote:

>The idea of indexing a numeric type is silly,

Not at all, consider Unit type declared modular because it has to be used
as a discriminant. At the same time Unit is a composite of powers for mass,
time, current, temperature etc. One would like to have it indexed (viewed
as an array or as a record).

Another problem is that you cannot make everything Controlled without MD.
Because otherwise you will permanently run into problems with primitive
operations of multiple types, multi-methods etc.

[Jacob Sparre Andersen news]

"Dmitry A. Kazakov" <mai...@dmitry-kazakov.de> wrote in message

news:1luaso698dpcc$.rrv8385qwl92.dlg@40tude.net...

>> On Mon, 6 May 2013 20:09:46 -0500, Randy Brukardt wrote:
>>
>>>The idea of indexing a numeric type is silly,
>>
>> Not at all, consider Unit type declared modular because it has to be used
>> as a discriminant. At the same time Unit is a composite of powers for
>> mass,
>> time, current, temperature etc. One would like to have it indexed (viewed
>> as an array or as a record).

It might make sense to view it as a record (a capability not in Ada 2012),
but it makes little sense to view it as an array (a list of identical
components indexed by a potentially *computed* index). There are a lot of
abuses of arrays out there that would be much better written as records.

> Another problem is that you cannot make everything Controlled without MD.
> Because otherwise you will permanently run into problems with primitive
> operations of multiple types, multi-methods etc.

Say what? Making everything controlled simply means that every type has a
Finalize operation. Dispatching *within* a Finalize operation is usually a
disaster (you don't want to redispatch as you might be finalizing the parent
part of some child type), so what that has to do with MD is beyond my
comprehension.

I suppose you might get into trouble if you mistakenly try to declare
multiple tagged types in a package, but that's always a bad idea and should
be avoidable in almost all cases (possibly with careful use of limited
with). If you really need multiple types in a package, you have too much
coupling between "objects" (in an OO sense), and coupling is always
something to be minimized.

Randy.

[Jacob Sparre Andersen news]

"Dmitry A. Kazakov" <mai...@dmitry-kazakov.de> wrote in message

news:19lrzzbgm77v6.1...@40tude.net...
...

> I thought about it, but this is far larger than one-man project and there
> is too much things which nobody did before and nobody knows how to do.
> Before doing this one should clearly understand it, and before
> understanding it there should be a serious discussion about it. And before
> that starts there should be a desire in the community to fix the language,
> which is clearly absent. Ada 2012 became a patchwork under which one can
> barely see its original ideas.

I don't think there is any point in "fixing" Ada anymore than there is a
point in "fixing" C++ or Java or (pick any other widely used language here).
The language is "good enough" for most purposes, and people are going to
have to see clear advantages to a new language before they would move.

OTOH, that doesn't mean that a complete overhaul of Ada (but keeping most of
its core principles intact) wouldn't be a good idea. The main thing is that
the result most certainly would not be Ada, but rather would be a new
language *inspired by* Ada. (That might even be a good thing, as it would
allow Ada-haters to take an unbiased look without realizing Ada was
involved.) If such a language had clear advantages over Ada 2012 (and few or
no clear disadvanatges), it would be likely that many Ada users would make
the switch.

But obviously this is a tough road; the language has to be designed and a
reference implementation built before it is likely that there would be many
customers. Whether such a model could be managed is hard to say, especially
in terms of funding.

Randy.

[Yannick Duchêne (Hibou57)]

Le Tue, 07 May 2013 22:27:58 +0200, Jacob Sparre Andersen news
<ra...@rrsoftware.com> a écrit:

> "Dmitry A. Kazakov" <mai...@dmitry-kazakov.de> wrote in message
> news:1luaso698dpcc$.rrv8385qwl92.dlg@40tude.net...
>>> On Mon, 6 May 2013 20:09:46 -0500, Randy Brukardt wrote:
>>>
>>>> The idea of indexing a numeric type is silly,
>>>
>>> Not at all, consider Unit type declared modular because it has to be
>>> used
>>> as a discriminant. At the same time Unit is a composite of powers for
>>> mass,
>>> time, current, temperature etc. One would like to have it indexed
>>> (viewed
>>> as an array or as a record).
>
> It might make sense to view it as a record (a capability not in Ada
> 2012),
> but it makes little sense to view it as an array (a list of identical
> components indexed by a potentially *computed* index). There are a lot of
> abuses of arrays out there that would be much better written as records.

Look at the deflate specification (RFC 1951), this makes sense with it to
see modular types as an array of bits. Anyway, user‑defined indexing is
supposed to be a client‑side interface to some data type, most likely and
allowed to be opaque, so what makes the less sense, is assertions about
what the underlying type should be.

[Yannick Duchêne (Hibou57)]

Le Tue, 07 May 2013 22:35:01 +0200, Jacob Sparre Andersen news
<ra...@rrsoftware.com> a écrit:

> OTOH, that doesn't mean that a complete overhaul of Ada (but keeping
> most of
> its core principles intact) wouldn't be a good idea. The main thing is
> that
> the result most certainly would not be Ada, but rather would be a new
> language *inspired by* Ada. (That might even be a good thing, as it would
> allow Ada-haters to take an unbiased look without realizing Ada was
> involved.) If such a language had clear advantages over Ada 2012 (and
> few or
> no clear disadvanatges), it would be likely that many Ada users would
> make
> the switch.

That was indeed the idea (and just an idea or a wish).

[Adam Beneschan]

On Tuesday, May 7, 2013 3:32:03 PM UTC-7, Dennis Lee Bieber wrote:
> On Tue, 7 May 2013 15:35:01 -0500, "Jacob Sparre Andersen news"
>
> Randy declaimed the following in comp.lang.ada:

>
> > OTOH, that doesn't mean that a complete overhaul of Ada (but keeping most of
> > its core principles intact) wouldn't be a good idea. The main thing is that
> > the result most certainly would not be Ada, but rather would be a new
> > language *inspired by* Ada. (That might even be a good thing, as it would
> > allow Ada-haters to take an unbiased look without realizing Ada was
> > involved.) If such a language had clear advantages over Ada 2012 (and few or
> > no clear disadvanatges), it would be likely that many Ada users would make
> > the switch.
>

> What would you call it? AdaPT (Ada-Prime Transform <G>)

We could follow the "increment operator" pattern adopted by C++, and call it something like Language'Succ(Ada) or maybe Ada'Succ for short. Then again, that might not be the best name to induce Ada-haters to take another look at it....

-- Adam

[Shark8]

On Tuesday, May 7, 2013 2:35:01 PM UTC-6, Jacob Sparre Andersen news wrote:
>
> OTOH, that doesn't mean that a complete overhaul of Ada (but keeping most of
> its core principles intact) wouldn't be a good idea. The main thing is that
> the result most certainly would not be Ada, but rather would be a new
> language *inspired by* Ada. (That might even be a good thing, as it would
> allow Ada-haters to take an unbiased look without realizing Ada was
> involved.) If such a language had clear advantages over Ada 2012 (and few or
> no clear disadvanatges), it would be likely that many Ada users would make
> the switch.
>
> But obviously this is a tough road; the language has to be designed and a
> reference implementation built before it is likely that there would be many
> customers. Whether such a model could be managed is hard to say, especially
> in terms of funding.

Aren't we getting ahead of ourselves don't we need RFPs for [working-name] Project Babbage first?

[Dmitry A. Kazakov]

On Tue, 7 May 2013 15:35:01 -0500, Jacob Sparre Andersen news wrote:

> The main thing is that
> the result most certainly would not be Ada, but rather would be a new
> language *inspired by* Ada.

No, that was the path taken by Ada 2005 and Ada 2012. Patches are
destroying the language fabric.

What I wish is to change the language foundation while keeping the
semantics of existing types intact. The whole idea is to move them onto the
library level rather than changing anything in them.

[Dmitry A. Kazakov]

On Tue, 7 May 2013 15:27:58 -0500, Jacob Sparre Andersen news wrote:

> "Dmitry A. Kazakov" <mai...@dmitry-kazakov.de> wrote in message
> news:1luaso698dpcc$.rrv8385qwl92.dlg@40tude.net...
>>> On Mon, 6 May 2013 20:09:46 -0500, Randy Brukardt wrote:
>>>
>>>>The idea of indexing a numeric type is silly,
>>>
>>> Not at all, consider Unit type declared modular because it has to be used
>>> as a discriminant. At the same time Unit is a composite of powers for mass,
>>> time, current, temperature etc. One would like to have it indexed (viewed
>>> as an array or as a record).
>
> It might make sense to view it as a record (a capability not in Ada 2012),
> but it makes little sense to view it as an array (a list of identical
> components indexed by a potentially *computed* index).

The index could be enumeration.

> There are a lot of
> abuses of arrays out there that would be much better written as records.

Yes, but the point is that whether array or record interface there could be
reasons for the programmer to add that interface to any type he wished. It
is not the language business to dictate me if I may index or "dismember"
anything.

>> Another problem is that you cannot make everything Controlled without MD.
>> Because otherwise you will permanently run into problems with primitive
>> operations of multiple types, multi-methods etc.
>
> Say what? Making everything controlled simply means that every type has a
> Finalize operation. Dispatching *within* a Finalize operation is usually a
> disaster (you don't want to redispatch as you might be finalizing the parent
> part of some child type), so what that has to do with MD is beyond my
> comprehension.

That is a different issue. I meant that if A and B are controlled/tagged
you will have troubles in using them as parameters of same subprogram. Even
two parameters of same type is a problem already. Only MD can resolve that.

Regarding dispatching Finalize, the thing is broken. The only model of
destruction I know, which would allow dispatching is having class-wide
destructors called prior to specific destructors. You would be able to
dispatch from the former.

And, yes, re-dispatch is a great evil and should never be in the language
in first place. At least class-wide view conversions in Finalize should be
made illegal. But that is too late.

Though Finalize is irrelevant anyway because if constructors/destructors
will ever added to the language that will not happen on the basis of
primitive operations. So Finalize could be left as is.

> I suppose you might get into trouble if you mistakenly try to declare
> multiple tagged types in a package, but that's always a bad idea and should
> be avoidable in almost all cases (possibly with careful use of limited
> with).

I don't see why is it a bad idea to have related types declared in one
package. On the contrary it is a good idea to group related things in a way
making it easer to use. I am glad that Ada does not tie types to packages.

> If you really need multiple types in a package, you have too much
> coupling between "objects" (in an OO sense), and coupling is always
> something to be minimized.

Declaration scope is not automatically coupling. But otherwise, yes, index
type is coupled to the array type. Sometimes decoupling is a bad idea
because it leads to weaker typing. E.g. if you wanted to decouple array
index you would end up indexing all arrays by one integer type. Welcome to
C.

[Yannick Duchêne (Hibou57)]

Le Wed, 08 May 2013 09:38:03 +0200, Dmitry A. Kazakov
<mai...@dmitry-kazakov.de> a écrit:

> On Tue, 7 May 2013 15:35:01 -0500, Jacob Sparre Andersen news wrote:
>
>> The main thing is that
>> the result most certainly would not be Ada, but rather would be a new
>> language *inspired by* Ada.
>
> No, that was the path taken by Ada 2005 and Ada 2012. Patches are
> destroying the language fabric.
>
> What I wish is to change the language foundation while keeping the
> semantics of existing types intact. The whole idea is to move them onto
> the library level rather than changing anything in them.

Eiffel had this; all types were at what would have been library level for
Eiffel. But it was too much lacking expressiveness in defining numeric
types (ex. you could not cleanly specify ranges).

[Dmitry A. Kazakov]

On Wed, 08 May 2013 09:59:18 +0200, Yannick Duch�ne (Hibou57) wrote:

> But it was too much lacking expressiveness in defining numeric
> types (ex. you could not cleanly specify ranges).

BTW, range should become a proper type. That is the problem of parallel
type hierarchies. I.e. describing relationships of unrelated yet bound to
each other types, like index, range, array, slice, element. There should be
some general mechanism to handle such clouds of types.

[Yannick Duchêne (Hibou57)]

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

> BTW, range should become a proper type. That is the problem of parallel
> type hierarchies. I.e. describing relationships of unrelated yet bound to
> each other types, like index, range, array, slice, element. There should
> be some general mechanism to handle such clouds of types.

That would come as natural. Just to stay with the range case, this would
allow to have range object (we only have the range attribute, which is an
UFO in the overall Ada entities model), without being forced to
de‑structure it (as with some `First` and `Last` argument to a
sub‑program), which would come with added safety at some place. This would
permit proper functions and operations on ranges. I also noted some Ada
new‑comers sometime feel surprised there is no way to pass or declare a
range object in Ada, … that's indeed surprising, as there is a range
attribute.

Creating the glue between an array type and a range type is straight away
actually with Ada, but a more general model could be type properties. This
would allow to declare things in a more readable and reliable way:


-- Fictitious example, not real Ada

A : Array_Type;
I : A'Index_Type; -- As an attribute of an object
J : Array_Type.Index_Type; -- As a member of a type.


May be an idea for something similar with primitive operations:


-- Fictitious example, not real Ada

function Implicit_Indexing
(A : Array_Type; -- An array type or an array interface
I : A'Index_Type)
return A'Element_Type;


That would bind things together, and provide a more general model tan
per‑type adhoc tricks (would help, if you want types at library level).

But then, an example such as the above would present challenge with
derived types.

> BTW, range should become a proper type. That is the problem of parallel
> type hierarchies. I.e. describing relationships of unrelated yet bound to
> each other types

Not everything is bound to each‑other, there is a dependency order. When
not, this means this is a [co‑]recursive structure, and there is already
incomplete declarations for this (the most natural I think).

[Yannick Duchêne (Hibou57)]

Le Wed, 08 May 2013 11:39:23 +0200, Yannick Duchêne (Hibou57)
<yannick...@yahoo.fr> a écrit:

> -- Fictitious example, not real Ada
>
> function Implicit_Indexing
> (A : Array_Type; -- An array type or an array interface
> I : A'Index_Type)
> return A'Element_Type;

That too, Eiffel had something a bit looking like this, using anchors
(with the “like” keyword, ex. `Object : like FOO.Member`).

[Dmitry A. Kazakov]

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. The typical
case is slice, you constrain index and get a constrained subtype of the
array. But if you constrain the multi-dimensional index of a matrix by
fixing one component of you get a new type: submatrix. You need a formalism
describing propagation of constrants, conditions, parent-child
relationships across the cloud of types.

[Yannick Duchêne (Hibou57)]

Le Wed, 08 May 2013 12:23:06 +0200, Dmitry A. Kazakov
<mai...@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).

[Dmitry A. Kazakov]

On Wed, 08 May 2013 13:08:48 +0200, Yannick Duchêne (Hibou57) wrote:

> Le Wed, 08 May 2013 12:23:06 +0200, Dmitry A. Kazakov
> <mai...@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).

First you should be able to define such entities formally = at the language
level.

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

Checks if come in question, then only much later after you have formalized
it.

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

Each time you do something with a type you get another one. Otherwise it
becomes untyped. So if you wanted to disallow operations that would make
another interface. To put it differently, there shall be no preconditions
on types and their operations which aren't trivially true. Another question
is the relationship between the original type and the new one. That brings
the issue of LSP with it, if you attempt to bring them into one hierarchy.
Ad-hoc supertypes could possibly help. Parallel hierarchies could be an
alternative.

[Yannick Duchêne (Hibou57)]

Le Wed, 08 May 2013 17:29:33 +0200, Dmitry A. Kazakov
<mai...@dmitry-kazakov.de> a écrit:

>> 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).
>
> First you should be able to define such entities formally = at the
> language
> level.

Yes, that was the idea. What you say seems equivalent to saying “the
language should allow to express it”. Actually, it's built‑in only (and so
also frozen). By the way, old prover software had a comparable issue in
the paste, they came with built‑in methods to validate this or that kind
of specific inferences technique within this or that kind of specific
domain. Then later came provers with a tiny core engine, on which is
concentrated all the efforts for correctness. The former were more error
prone (one was even well known as buggy and not soun) and less expressive.
The latter present their own issues, but are more safe and more
expressive, as they allow the user to freely express something above, as
the core ensure the soundness of the inferences (you can get it wrong too,
but that's not the topic). I don't try to say a general purpose
programming language should compare to this, just that the way to go ahead
may be a bit similar: less built‑ins, and more support for soundness (I
like to say, the value of a language is not in its libraries, this is a
bit similar here).

>> 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,
>
> Checks if come in question, then only much later after you have
> formalized
> it.

Static checking is not like dynamic checking. Dynamic checking is just
checking, while static checking really ensure some assertions. There are
multiple way to formalize, but sooner or later, all have to arrive at the
point of providing assertions, or else, you can't derive anything from it.
So I believe static check one of the way to the formalization.

>> 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,
>
> Each time you do something with a type you get another one.

Yes

> Otherwise it
> becomes untyped. So if you wanted to disallow operations that would make
> another interface.

That's what a subtype is to me (I don't know if it's the proper term; at
least it seems to match with Ada's own wording).

> To put it differently, there shall be no preconditions
> on types and their operations which aren't trivially true.

I don't understand that point.

> Another question
> is the relationship between the original type and the new one. That
> brings
> the issue of LSP with it, if you attempt to bring them into one
> hierarchy.

LSP is a handy principle, the only one practicable with most general
purpose languages, but that's not the only way to formalize things and
ensure their correctness; sometime it does not fit. Some relations may be
preserved, some may not be. If some are preserved, you can count on it,
while it suffice some are not preserved to make LSP irrelevant, and worst,
reject the system. That's precisely the case with restricted interfaces,
it's easy to see some relations are preserved but it does not conform to
LSP. LSP is nice when applicable, because it is a simple principle; there
are times where it is too rigid. That's why I focused on the topic of the
relations and properties individually.

> Ad-hoc supertypes could possibly help.

Yes, that would allow to understand subtypes as any other simply derived
types. May be the supertype could be automatically or inferred. Or should
that be always explicit?

> Parallel hierarchies could be an
> alternative.

I will try to imagine what this means or how it works, I don't have a
clear picture in mind right at the moment.

[Dmitry A. Kazakov]

On Wed, 08 May 2013 18:13:26 +0200, Yannick Duch�ne (Hibou57) wrote:

> Le Wed, 08 May 2013 17:29:33 +0200, Dmitry A. Kazakov

> <mai...@dmitry-kazakov.de> a �crit:

>> Each time you do something with a type you get another one.
>
> Yes
>
>> Otherwise it
>> becomes untyped. So if you wanted to disallow operations that would make
>> another interface.
>
> That's what a subtype is to me (I don't know if it's the proper term; at
> least it seems to match with Ada's own wording).

No. Ada subtype cannot not disallow an operation. It can at best override
one with "raise Message_Not_Understood;". In order to disallow an operation
you need a new Ada type. Disallowing is not a constraint.

>> To put it differently, there shall be no preconditions
>> on types and their operations which aren't trivially true.
>
> I don't understand that point.

Whatever differences are, they are rendered as differences in the
interfaces rather that in the preconditions. Preconditions of arguments are
always true, or else the language becomes weakly typed.

[Randy Brukardt]

"Dmitry A. Kazakov" <mai...@dmitry-kazakov.de> wrote in message

news:p0pf97g5w6xg.jhca6ztjwpde$.dlg@40tude.net...

> On Tue, 7 May 2013 15:35:01 -0500, Jacob Sparre Andersen news wrote:
>
>> The main thing is that
>> the result most certainly would not be Ada, but rather would be a new
>> language *inspired by* Ada.
>
> No, that was the path taken by Ada 2005 and Ada 2012. Patches are
> destroying the language fabric.

I'm not talking about "patches", I'm talking about starting over. And so are
you...

> What I wish is to change the language foundation while keeping the
> semantics of existing types intact. The whole idea is to move them onto
> the
> library level rather than changing anything in them.

That's precisely what I'm talking about. The result cannot be Ada, because
the result is not going to be close to 100% compatible with Ada (and that
should not be a criteria for a new language). Despite your fantasies to the
contrary, there is no possibility of changing the models in any useful way
and retaining compatibility in subtle cases. Moreover, even if possible, the
pretzel-like rules needed would prevent the sort of overhaul that you really
desire. So why cling to the mistakes of the past - flush all of that down
the drain and start over.

Randy.

P.S. Sorry about getting the name wrong in my postings from yesterday,
especially with any confusion with Jacob.

[Randy Brukardt]

"Dmitry A. Kazakov" <mai...@dmitry-kazakov.de> wrote in message

news:nd22gfeezrwf$.tlj4yyygrwq3$.dlg@40tude.net...
...

> Each time you do something with a type you get another one. Otherwise it
> becomes untyped.

That way leads to madness, I think. It's better for "types" to be fairly
weak and interoperable. In this model, "types" are the low-level view of
entities (with things like representation, "kind" [integer, float, array,
etc.]). On top of that, you have some thing else, let's call them "profiles"
(as "interfaces" imply dynamic behavior, which is not what we're talking
about here). In my language, "profiles" are statically checked and apply to
objects as well as subprograms (objecting being overloadable). "Profiles"
provide the high-level view of entities, and would be where properties like
"apples" and "oranges" would be dealt with. There'd be a shorthand for
adding a profile to all uses of a type (just as subtypes provide that for
constraints in Ada). If the profiles "match", then the items are compatible,
and if they don't, then they're not.

If done right, this would provide a lot more static checking opportunities
than Ada could ever have, and it would get away from the stale notion of
"type", which is just not powerful enough by itself.

Randy.

[Randy Brukardt]

"Dmitry A. Kazakov" <mai...@dmitry-kazakov.de> wrote in message

news:1xlzfj8qy1zey$.up1s1v3syagv.dlg@40tude.net...
> On Tue, 7 May 2013 15:27:58 -0500, Randy Brukardt wrote:
...

>>> Another problem is that you cannot make everything Controlled without
>>> MD.
>>> Because otherwise you will permanently run into problems with primitive
>>> operations of multiple types, multi-methods etc.
>>
>> Say what? Making everything controlled simply means that every type has a
>> Finalize operation. Dispatching *within* a Finalize operation is usually
>> a
>> disaster (you don't want to redispatch as you might be finalizing the
>> parent
>> part of some child type), so what that has to do with MD is beyond my
>> comprehension.
>
> That is a different issue. I meant that if A and B are controlled/tagged
> you will have troubles in using them as parameters of same subprogram.
> Even
> two parameters of same type is a problem already. Only MD can resolve
> that.

That's only a problem if the routine is primitive for *both* types. And
that's only a problem if the types are declared in the same package, which
is already a bad idea because it means that they have excessive coupling.
I'm sure it happens once in a while, but it shouldn't be happening often.

...

>> I suppose you might get into trouble if you mistakenly try to declare
>> multiple tagged types in a package, but that's always a bad idea and
>> should
>> be avoidable in almost all cases (possibly with careful use of limited
>> with).
>
> I don't see why is it a bad idea to have related types declared in one
> package. On the contrary it is a good idea to group related things in a
> way
> making it easer to use. I am glad that Ada does not tie types to packages.

One O-O type per package is the only model that makes sense. It's fine to
include "helper" types in the package (stuff like enumerations, integers,
and the like), but you should never mix the "big" abstractions of your
program. I was never talking about "little" types, like the ones used to
interface to hardware -- these should be hidden in bodies anyway. If you
can't separate the "big" abstractions, you have too much coupling.

Your example of the array index is certainly not the sort of case that I'm
talking about; that's a "helper" type and I certainly agree that it's best
declared with the array. But this is the sort of type that's logically part
of the larger abstraction and is declared separately just because Ada
requires that; it really should be declared as part of the same declaration.

Randy.

[Dmitry A. Kazakov]

On Wed, 8 May 2013 15:27:50 -0500, Randy Brukardt wrote:

> "Dmitry A. Kazakov" <mai...@dmitry-kazakov.de> wrote in message
> news:nd22gfeezrwf$.tlj4yyygrwq3$.dlg@40tude.net...
> ...
>> Each time you do something with a type you get another one. Otherwise it
>> becomes untyped.
>
> That way leads to madness, I think. It's better for "types" to be fairly
> weak and interoperable.

Weak typing is better?

> In this model, "types" are the low-level view of
> entities (with things like representation, "kind" [integer, float, array,
> etc.]).

Structured type equivalence, DDL, the third manifesto etc.

> On top of that, you have some thing else, let's call them "profiles"
> (as "interfaces" imply dynamic behavior, which is not what we're talking
> about here). In my language, "profiles" are statically checked and apply to
> objects as well as subprograms (objecting being overloadable). "Profiles"
> provide the high-level view of entities, and would be where properties like
> "apples" and "oranges" would be dealt with. There'd be a shorthand for
> adding a profile to all uses of a type (just as subtypes provide that for
> constraints in Ada). If the profiles "match", then the items are compatible,
> and if they don't, then they're not.
>
> If done right, this would provide a lot more static checking opportunities
> than Ada could ever have, and it would get away from the stale notion of
> "type", which is just not powerful enough by itself.

This, I am afraid, is how many people view strong typing and how this leads
them away from typing. It takes certain courage to admit that you hate
strong typing, because it became a sort of PC-doctrine, which everybody
feels obliged to commit publicly to, while cursing it privately. Still the
alternative to strong typing is the horrific mess you just have described.
Of course I completely disagree with your view.

Strong typing is madness only without type hierarchies. Types are not
isolated. In certain contexts values of different types are
interchangeable. E.g. Positive can be used as Integer in some contexts. In
other contexts it cannot. This difference makes them distinct types,
nothing else. Where is a difference there is a new type. Substitutability
(= implicit type conversion) is the glue to bring a structure into the
universe of atomized types. You use Positive as if it were Integer because
they participate in a structure of a super-subtype relationship. That does
not make them same type. You cannot force software design into a framework
when types were completely isolated from each other. Types participate in
rich relationships. The language should support declaration and design such
structures of types with static checks. Inventing "profiles", "aspects" etc
gains nothing.

Strong typing is an ability to distinguish types. Not mixing types means
that you could not have subprograms with more than one argument. It is just
crazy. Types are mixed all the time. In a statically typed language all
cases when types get mixed are statically checked. You cannot do that
without taking types apart first.

[Dmitry A. Kazakov]

On Wed, 8 May 2013 15:12:38 -0500, Randy Brukardt wrote:

> "Dmitry A. Kazakov" <mai...@dmitry-kazakov.de> wrote in message
> news:p0pf97g5w6xg.jhca6ztjwpde$.dlg@40tude.net...

>> What I wish is to change the language foundation while keeping the
>> semantics of existing types intact. The whole idea is to move them onto
>> the library level rather than changing anything in them.
>
> That's precisely what I'm talking about. The result cannot be Ada, because
> the result is not going to be close to 100% compatible with Ada (and that
> should not be a criteria for a new language).

I don't see obvious reason why. It is not about reworking exiting built-in
types and type-algebraic operations. There is nothing wrong with them.

> Despite your fantasies to the
> contrary, there is no possibility of changing the models in any useful way
> and retaining compatibility in subtle cases. Moreover, even if possible, the
> pretzel-like rules needed would prevent the sort of overhaul that you really
> desire. So why cling to the mistakes of the past - flush all of that down
> the drain and start over.

Because most of Ada semantics is OK. I don't see any mistakes. Even if they
were, it is irrelevant because I am looking for a more general model, where
mistake or not, it becomes just an implementation. So if you don't like a
particular built-in type for whatever reason, you make your own. No
problem.

[Dmitry A. Kazakov]

On Wed, 8 May 2013 15:37:24 -0500, Randy Brukardt wrote:

> "Dmitry A. Kazakov" <mai...@dmitry-kazakov.de> wrote in message
> news:1xlzfj8qy1zey$.up1s1v3syagv.dlg@40tude.net...
>> On Tue, 7 May 2013 15:27:58 -0500, Randy Brukardt wrote:
> ...
>>>> Another problem is that you cannot make everything Controlled without MD.
>>>> Because otherwise you will permanently run into problems with primitive
>>>> operations of multiple types, multi-methods etc.
>>>
>>> Say what? Making everything controlled simply means that every type has a
>>> Finalize operation. Dispatching *within* a Finalize operation is usually a
>>> disaster (you don't want to redispatch as you might be finalizing the parent
>>> part of some child type), so what that has to do with MD is beyond my
>>> comprehension.
>>
>> That is a different issue. I meant that if A and B are controlled/tagged
>> you will have troubles in using them as parameters of same subprogram. Even
>> two parameters of same type is a problem already. Only MD can resolve that.
>
> That's only a problem if the routine is primitive for *both* types.

There are good arguments for having all parameters either controlled or
else class-wide.

> And
> that's only a problem if the types are declared in the same package, which
> is already a bad idea because it means that they have excessive coupling.

The language should prevent operations from being non-primitive, except for
maybe in the package bodies or nested.

>>> I suppose you might get into trouble if you mistakenly try to declare
>>> multiple tagged types in a package, but that's always a bad idea and should
>>> be avoidable in almost all cases (possibly with careful use of limited with).
>>
>> I don't see why is it a bad idea to have related types declared in one
>> package. On the contrary it is a good idea to group related things in a way
>> making it easer to use. I am glad that Ada does not tie types to packages.
>
> One O-O type per package is the only model that makes sense. It's fine to
> include "helper" types in the package (stuff like enumerations, integers,
> and the like), but you should never mix the "big" abstractions of your
> program. I was never talking about "little" types, like the ones used to
> interface to hardware -- these should be hidden in bodies anyway. If you
> can't separate the "big" abstractions, you have too much coupling.

There is no "little" and no "big" types. It is simply wrong to think about
software design in such terms. It was a very bad OO idea to separate types
into "classes" and other types.

An abstraction is always too large for a single type. It cannot be
otherwise.

> Your example of the array index is certainly not the sort of case that I'm
> talking about; that's a "helper" type and I certainly agree that it's best
> declared with the array.

There should be no helper types in a properly designed language. Each type
should express/implement something useful from the problem space. Index is
such a thing. There is nothing in it that would make it less important than
the array type, or the array element type.

[Randy Brukardt]

"Dmitry A. Kazakov" <mai...@dmitry-kazakov.de> wrote in message

news:1nw4bxyvk1gj5.xmiirr0diavq$.dlg@40tude.net...

> On Wed, 8 May 2013 15:37:24 -0500, Randy Brukardt wrote:

...

>> One O-O type per package is the only model that makes sense. It's fine to
>> include "helper" types in the package (stuff like enumerations, integers,
>> and the like), but you should never mix the "big" abstractions of your
>> program. I was never talking about "little" types, like the ones used to
>> interface to hardware -- these should be hidden in bodies anyway. If you
>> can't separate the "big" abstractions, you have too much coupling.
>
> There is no "little" and no "big" types. It is simply wrong to think about
> software design in such terms. It was a very bad OO idea to separate types
> into "classes" and other types.
>
> An abstraction is always too large for a single type. It cannot be
> otherwise.

As usual, I pretty much totally disagree with your thinking here. The last
statement is trivially true, of course, but so what? A program has to be
built on top of a handful of "big" abstractions. And for each of those "big"
abstractions, there has to be a single type which takes the lead (probably
with a family of other types in support). Interactions between the
abstraction has to be minimized, and preferably takes place through the lead
type.

In bigger systems, each of those abstractions corresponds to a subsystem (in
Ada, that's best modeled as a family of child packages). Inside each of
those subsystems, you'll have another family of types. But the majority of
these types should not extend beyond the subsystem.

You seem to claim that all types are equally important, which is obvious
nonsense. And all I said is that you design your system around the handful
of most important types, and those types should each get a package to
themselves. (Or even a family of packages.) Mixing the declarations of
subsystems is simply madness.

>> Your example of the array index is certainly not the sort of case that
>> I'm
>> talking about; that's a "helper" type and I certainly agree that it's
>> best
>> declared with the array.
>
> There should be no helper types in a properly designed language. Each type
> should express/implement something useful from the problem space. Index is
> such a thing. There is nothing in it that would make it less important
> than
> the array type, or the array element type.

I hope I never, ever have to use any of your software. Claiming that the
lookup result enumeration ("Found", "Missing", "Ambiguous") is as important
as the symbol table data structure is insane. That sort of thinking leads to
all kinds of structuring crazyness.

Randy.

[Randy Brukardt]

"Dmitry A. Kazakov" <mai...@dmitry-kazakov.de> wrote in message

news:1bp6zlpetr5l4.1...@40tude.net...

When you say "semantics", you're really only talking about the dynamic
semantics, that is the runtime model. But the compile-time model is just as
important. You would have to reproduce every feature and flaw of the
existing compile-time model with a totally new underlying model. And doing
that would be very, very complex.

The problem is, when you do that, you'd have no way to determine whether or
not it is really compatible. (After all, there is no formal model for Ada,
and there never has been.) Ada's definition is just a mass of English text,
and replacing it by a different mass of English text leaves one no practical
way to prove compatibility. And it is very unlikely that there would be any
interest in an incompatible version of Ada. Moreover, no one would be much
interested in a version that's *almost* like Ada but would break almost
everyone's code.

If one starts over, you eliminate that need for absolute compatibility. You
might still be fairly close to the semantics of Ada (although I don't see
the point; it should be simplified by removing corner cases and little used
stuff and features that are duplicative), but there is no need to prove
compatibility (or convince anyone of it). And you could fix obvious mistakes
of Ada (objects don't overload, for one example, and the more general
user-defined indexing that you would like, and so on) without having to
worry about the effects in private parts of nested packages -- which is what
prevents most progress today.

Randy.

[Randy Brukardt]

"Dmitry A. Kazakov" <mai...@dmitry-kazakov.de> wrote in message

news:12gn9wvv1gwfk.1...@40tude.net...

> On Wed, 8 May 2013 15:27:50 -0500, Randy Brukardt wrote:
>
>> "Dmitry A. Kazakov" <mai...@dmitry-kazakov.de> wrote in message
>> news:nd22gfeezrwf$.tlj4yyygrwq3$.dlg@40tude.net...
>> ...
>>> Each time you do something with a type you get another one. Otherwise it
>>> becomes untyped.
>>
>> That way leads to madness, I think. It's better for "types" to be fairly
>> weak and interoperable.
>
> Weak typing is better?

Yes, because we need to move beyond typing to other forms of static error
detection. Typing is too rigid to do a good job -- you need to include
statically known information about the contents of variables and parameters,
which can change from line-to-line in a program.

I want checking that is *stronger* than what can be provided by statically
applied types. Trying to get it by extending the type model directly is
madness, especially as it makes sharing much less possible.

Yes, of course. You have completely bought the OOP bill of goods that claims
there is something magical about types.

> Strong typing is madness only without type hierarchies.

Who said anything about getting rid of hierarchies? I think they're greatly
overused (the number of abstractions that benefit from a hierarchy is quite
low), but there certainly are cases where they help.

> Types are not isolated.

Again, no one said anything about them being isolated. Although I do think
that vast majority of types ought to be separate from other types -- the
interactions being handled in the operations, not in the types themselves.

> In certain contexts values of different types are
> interchangeable. E.g. Positive can be used as Integer in some contexts. In
> other contexts it cannot.

Great, context-dependent types. There are only two good descriptions for
that: "madness", or better, "weak typing". :-) (And of course, there are no
contexts where Integer and Positive are "different". You are already far out
of the mainstream when you say that. And of course, to allow such a
difference, you have to go beyond typing, to say "profiles".)

Types form the bedrock of a programming language design, and as such they
should be unchanging. There should be no difference in typing between
contexts -- it has to be the same everywhere. To get further checks, you
have to add on another layer on top.

> This difference makes them distinct types,
> nothing else. Where is a difference there is a new type.

I strongly disagree with this. The only way this could work is for *every*
use of *every* entity of a program to be a separate type. And then have lots
of interconvertability rules. I think you'd quickly reach a level of
insanity.

> Substitutability
> (= implicit type conversion) is the glue to bring a structure into the
> universe of atomized types. You use Positive as if it were Integer because
> they participate in a structure of a super-subtype relationship. That does
> not make them same type. You cannot force software design into a framework
> when types were completely isolated from each other. Types participate in
> rich relationships. The language should support declaration and design
> such
> structures of types with static checks. Inventing "profiles", "aspects"
> etc
> gains nothing.

Seems to me that you are drunk on the OOP-koolaid. What you can usefully do
with type algebra is very limited, and I think we need to go beyond that.

In particular, I think the Ada model of few types (essentially, initial
declaration equivalent) is the way to go; all of the action should be on
enhancing subtypes and subprograms such that static checks are possible (by
combining constraints, null exclusions, predicates, parameter/result
profiles, and possibly other things into an integrated concept).

> Strong typing is an ability to distinguish types. Not mixing types means
> that you could not have subprograms with more than one argument. It is
> just
> crazy.

Certainly when you invent ideas like this, which have nothing to do with
anything that I said or was thinking about. Obviously, operations of one
type need parameters of another type. But your OOP-fever means that you
think that this somehow implies the types are related. And that way can only
lead to madness.

> Types are mixed all the time. In a statically typed language all
> cases when types get mixed are statically checked. You cannot do that
> without taking types apart first.

I have no idea what the heck you are talking about now. In any case, it
makes no sense for me to respond to someone that has an advanced case of
OOP-fever. Certainly, *one* of us is insane -- time will prove which. No
point in my spending any more time on this topic unless someone else wants
to discuss it.

Randy.

[Yannick Duchêne (Hibou57)]

Le Fri, 10 May 2013 00:19:14 +0200, Randy Brukardt <ra...@rrsoftware.com>
a écrit:

> "Dmitry A. Kazakov" <mai...@dmitry-kazakov.de> wrote in message
> news:12gn9wvv1gwfk.1...@40tude.net...
>> On Wed, 8 May 2013 15:27:50 -0500, Randy Brukardt wrote:
>>
>>> "Dmitry A. Kazakov" <mai...@dmitry-kazakov.de> wrote in message
>>> news:nd22gfeezrwf$.tlj4yyygrwq3$.dlg@40tude.net...
>>> ...
>>>> Each time you do something with a type you get another one. Otherwise
>>>> it
>>>> becomes untyped.
>>>
>>> That way leads to madness, I think. It's better for "types" to be
>>> fairly
>>> weak and interoperable.
>>
>> Weak typing is better?
>
> Yes, because we need to move beyond typing to other forms of static error
> detection. Typing is too rigid to do a good job -- you need to include
> statically known information about the contents of variables and
> parameters,
> which can change from line-to-line in a program.

I feel the same. I often though typing can't do everything if it comes
with value type checking, while in some occasions, I tried to express each
validity condition with types and then type checking (that ends to be
crazy, indeed). A simple example, is paired invocation, where whenever a
sub‑program is is invoked, sooner or later, another sub‑program must be
invoked too on the same argument, ex. like `Open` and later `Close`. This
cannot be expressed with types and indeed requires assertions.

But saying “weak” may be erroneously interpreted, and then, the type is
still the first place to holds the validity rules. In the example above,
the paired invocation requirement, could be expressed in the type owning
these two primitives (there is no way to do it actually, except with
external checking tools and custom rules for this tool). That's just that
showing the type is used according to the rules it defines, could not be
ensured with classic type checking (there is no type checking to apply
here), it would needs assertions in the sources.

In summary I would say: the type is the source of validity rules, but
can't help to check it, so there is a need for something along to types.
At least, it would have to go beyond values (so far, types just describe
values).

[Yannick Duchêne (Hibou57)]

Le Fri, 10 May 2013 00:19:14 +0200, Randy Brukardt <ra...@rrsoftware.com>
a écrit:

> Again, no one said anything about them being isolated. Although I do
> think
> that vast majority of types ought to be separate from other types -- the
> interactions being handled in the operations, not in the types
> themselves.

Right, except while you say this, the only static check sub‑programs or
primitive operations provide, is the one applying on the types of their
arguments. So there is nothing handled by operations (at least, so far).

The point is still good enough, as at first sight, seems there are
operations which cannot said to be owned by a single type, so that may
looks hard to focus on type with this picture. Or else, there is a need
for a type representing sub‑program signature (something I wanted to reply
to Dmitry in another message), the arguments tuple, then optionally the
result tuple, and optionally both tuples, say the type of a transition as
an example. With this, interactions between types can be represented with
types.

[Yannick Duchêne (Hibou57)]

Le Fri, 10 May 2013 00:19:14 +0200, Randy Brukardt <ra...@rrsoftware.com>
a écrit:

>> In certain contexts values of different types are
>> interchangeable. E.g. Positive can be used as Integer in some contexts.
>> In
>> other contexts it cannot.
>
> Great, context-dependent types. There are only two good descriptions for
> that: "madness", or better, "weak typing". :-)

If two subtypes of a same root type can be used interchangeably in some
context, that's nothing justifying weak typing, that's just the rules with
subtypes. Or I miss‑understood the point?

[Yannick Duchêne (Hibou57)]

Le Fri, 10 May 2013 00:19:14 +0200, Randy Brukardt <ra...@rrsoftware.com>
a écrit:

>> This difference makes them distinct types,
>> nothing else. Where is a difference there is a new type.
>
> I strongly disagree with this. The only way this could work is for
> *every*
> use of *every* entity of a program to be a separate type.

No, and not more than one may defines a new subtypes for the result of
each numeric operations of a program. One may do if he/she wish or sees a
good reason, but that's not required.

[Yannick Duchêne (Hibou57)]

Le Fri, 10 May 2013 05:29:53 +0200, Yannick Duchêne (Hibou57)
<yannick...@yahoo.fr> a écrit:
> […] A simple example, is paired invocation, where whenever a sub‑program

> is is invoked, sooner or later, another sub‑program must be invoked too
> on the same argument, ex. like `Open` and later `Close`. This cannot be
> expressed with types and indeed requires assertions.
>
> But saying “weak” may be erroneously interpreted, and then, the type is
> still the first place to holds the validity rules. In the example above,
> the paired invocation requirement, could be expressed in the type owning

> these two primitives […]

No, what I said on this is wrong, due to lack of precision. This have to
be an assertion on the outer level, the state of the enclosing scope of
the operations (an implicit value which cannot be explicitly referred to
as a whole with Ada).

[Yannick Duchêne (Hibou57)]

Le Mon, 06 May 2013 20:55:34 +0200, Dmitry A. Kazakov
<mai...@dmitry-kazakov.de> a écrit:
>
> Instead of banishing exceptions one should put contracts on them.
>

In the meanwhile, that's hard to have exception contract without breaking
separation of implementation and specification; or else, the specification
would have to express requirements on the implementation, which is not a
so bad idea on its own, but which is something foreign to Ada, except as
comments.

However, there is an big‑picture contract on exceptions which would be
simple an useful without breaking privacy of implementation: a sub‑program
may or may not raise synchronous exceptions. This contract would be enough
I believe, especially with the help of the (non‑standard) pragma
`No_Exception_Propagation`.

Asynchronous exceptions, such as hardware error, memory chip error, OS
error, and so on, would be left uncovered. Anyway, I see nothing else if
not a rather immediate program termination when it occurs (may be just
logging a short static message, and then terminate).

[Yannick Duchêne (Hibou57)]

Le Mon, 06 May 2013 22:05:25 +0200, Adam Beneschan <ad...@irvine.com> a
écrit:

> On Monday, May 6, 2013 11:55:34 AM UTC-7, Dmitry A. Kazakov wrote:
>
>> Instead of banishing exceptions one should put contracts on them.
>

> Am I still in comp.lang.ada, or did I wander into arts.movies.godfather
> by mistake? :) :) :)
>
> -- Adam

No, that's arts.movies.momada (*), the big block‑buster of year 2013 :D

(*) Full title is “Mom' Ada — mom' said No, she like to say No”.

[Yannick Duchêne (Hibou57)]

Le Wed, 08 May 2013 02:18:44 +0200, Shark8 <onewing...@gmail.com> a
écrit:
> Aren't we getting ahead of ourselves don't we need RFPs for
> [working-name] Project Babbage first?

What is RFP here?

[Yannick Duchêne (Hibou57)]

Le Wed, 08 May 2013 20:17:30 +0200, Dmitry A. Kazakov
<mai...@dmitry-kazakov.de> a écrit:

>> That's what a subtype is to me (I don't know if it's the proper term; at
>> least it seems to match with Ada's own wording).
>
> No. Ada subtype cannot not disallow an operation.

I made a dirty picture based on values. Ada's subtypes can't restrict
operations, however do restrict values.

[Yannick Duchêne (Hibou57)]

Le Thu, 09 May 2013 23:43:29 +0200, Randy Brukardt <ra...@rrsoftware.com>
a écrit:

> If one starts over, you eliminate that need for absolute compatibility.
> You
> might still be fairly close to the semantics of Ada (although I don't see
> the point; it should be simplified by removing corner cases and little
> used
> stuff and features that are duplicative), but there is no need to prove
> compatibility (or convince anyone of it). And you could fix obvious
> mistakes
> of Ada (objects don't overload, for one example, and the more general
> user-defined indexing that you would like, and so on) without having to
> worry about the effects in private parts of nested packages -- which is
> what
> prevents most progress today.
>
> Randy.

Would already very nice!

[Dmitry A. Kazakov]

On Thu, 9 May 2013 16:33:55 -0500, Randy Brukardt wrote:

> As usual, I pretty much totally disagree with your thinking here. The last
> statement is trivially true, of course, but so what? A program has to be
> built on top of a handful of "big" abstractions. And for each of those "big"
> abstractions, there has to be a single type which takes the lead (probably
> with a family of other types in support).

Takes the lead, how? An abstraction including Employer, Employee, Factory,
Salary, Time, Duration, Integer, Address, Gender, Age ... Who takes the
"lead"?

> In bigger systems, each of those abstractions corresponds to a subsystem (in
> Ada, that's best modeled as a family of child packages). Inside each of
> those subsystems, you'll have another family of types. But the majority of
> these types should not extend beyond the subsystem.

How these subsystems are going to interact to each other?

> You seem to claim that all types are equally important, which is obvious
> nonsense.

Yes, I say that unimportant types need not to be exposed in public
interfaces.

Everything declared in the *same* scope is equally important, or else you
have a design issue.

> Claiming that the
> lookup result enumeration ("Found", "Missing", "Ambiguous") is as important
> as the symbol table data structure is insane.

How do you measure importance?

It is not a simple question. If you tried to roll up a measure and apply it
most commonly used types, you would probably see your the idea of leading
types (which, BTW, is one of most damaging ideas in OO ever) quickly
falling apart.

[Dmitry A. Kazakov]

On Thu, 9 May 2013 17:19:14 -0500, Randy Brukardt wrote:

> "Dmitry A. Kazakov" <mai...@dmitry-kazakov.de> wrote in message
> news:12gn9wvv1gwfk.1...@40tude.net...
>> On Wed, 8 May 2013 15:27:50 -0500, Randy Brukardt wrote:
>>
>>> "Dmitry A. Kazakov" <mai...@dmitry-kazakov.de> wrote in message
>>> news:nd22gfeezrwf$.tlj4yyygrwq3$.dlg@40tude.net...
>>> ...
>>>> Each time you do something with a type you get another one. Otherwise it
>>>> becomes untyped.
>>>
>>> That way leads to madness, I think. It's better for "types" to be fairly
>>> weak and interoperable.
>>
>> Weak typing is better?
>
> Yes, because we need to move beyond typing to other forms of static error
> detection.

Based on what? On individual values?

> Typing is too rigid to do a good job

Typing is necessarily rigid because it is on the next, higher level of
power. Types describe the behavior of sets of values. Nothing you can do
with individual values could come even close to that, except for trivial
cases like enumeration types. And there is the next level, classes describe
behavior of sets of types. And higher levels may probably come.

> I want checking that is *stronger* than what can be provided by statically
> applied types. Trying to get it by extending the type model directly is
> madness, especially as it makes sharing much less possible.

No, you will lose a whole universe of checks without gaining anything
useful. Checks of individual values have limits imposed by computability.
Furthermore, focusing on values, you will kill software engineering. Reuse
is what is really important. Checks are only a tool to make reuse safer.

>> This, I am afraid, is how many people view strong typing and how this leads
>> them away from typing. It takes certain courage to admit that you hate
>> strong typing, because it became a sort of PC-doctrine, which everybody
>> feels obliged to commit publicly to, while cursing it privately. Still the
>> alternative to strong typing is the horrific mess you just have described.
>> Of course I completely disagree with your view.
>
> Yes, of course. You have completely bought the OOP bill of goods that claims
> there is something magical about types.

Types were known long before OO and first programming languages (Russell,
Church etc).

>> Types are not isolated.
>
> Again, no one said anything about them being isolated. Although I do think
> that vast majority of types ought to be separate from other types -- the
> interactions being handled in the operations, not in the types themselves.

If you want them separate don't blame them for being separate. It was your
choice.

>> In certain contexts values of different types are
>> interchangeable. E.g. Positive can be used as Integer in some contexts. In
>> other contexts it cannot.
>
> Great, context-dependent types.

Not at all. It is substitutability which is context-depended and thus must
be formalized as context-independent type relationships (e.g. interfaces).
Existence of negative inverse is no property of Positive. There is no
context where it is. But it is a property of Integer. The context where you
want to have a negative inverse is a context where Positive is not
substitutable for Integer.

[ Since this property is directly observable as the operation "-", there is
no design where Positive could statically be same type as Integer. ]

> There are only two good descriptions for
> that: "madness", or better, "weak typing". :-) (And of course, there are no
> contexts where Integer and Positive are "different".

They are different in ALL contexts! Positive (a set of values with
properties of) is not Integer.

> You are already far out
> of the mainstream when you say that.

Not at all. It is plain school mathematics. Everybody knows that -1 is not
positive.

>> This difference makes them distinct types,
>> nothing else. Where is a difference there is a new type.
>
> I strongly disagree with this. The only way this could work is for *every*
> use of *every* entity of a program to be a separate type.

This is how you see it. This is a natural consequence of rejecting types
and thinking in terms of individual values. In this crazy world each value
has a type of its own, which renders types completely useless. Welcome to
OOA/D. (It is funny that you are accusing me of having bought OO's snake
oil (:-))

>> Substitutability
>> (= implicit type conversion) is the glue to bring a structure into the
>> universe of atomized types. You use Positive as if it were Integer because
>> they participate in a structure of a super-subtype relationship. That does
>> not make them same type. You cannot force software design into a framework
>> when types were completely isolated from each other. Types participate in
>> rich relationships. The language should support declaration and design such
>> structures of types with static checks. Inventing "profiles", "aspects" etc
>> gains nothing.
>
> Seems to me that you are drunk on the OOP-koolaid. What you can usefully do
> with type algebra is very limited, and I think we need to go beyond that.
>
> In particular, I think the Ada model of few types (essentially, initial
> declaration equivalent) is the way to go; all of the action should be on
> enhancing subtypes and subprograms such that static checks are possible (by
> combining constraints, null exclusions, predicates, parameter/result
> profiles, and possibly other things into an integrated concept).

Concept of what? You are not yet ready with types and want to introduce
something of unknown nature? How these new things will interact each other,
values, types, classes, packages. What is there to check if the properties
of are nowhere stated, meaning is undefined?

>> Strong typing is an ability to distinguish types. Not mixing types means
>> that you could not have subprograms with more than one argument. It is
>> just crazy.
>
> Certainly when you invent ideas like this, which have nothing to do with
> anything that I said or was thinking about. Obviously, operations of one
> type need parameters of another type. But your OOP-fever means that you
> think that this somehow implies the types are related.

What else a relationship is? Types deal with values and operations. There
is nothing else. Since values are not shared (Ada is typed so far), the
only thing which may bind two types is a shared operation.

[Dmitry A. Kazakov]

On Thu, 9 May 2013 16:43:29 -0500, Randy Brukardt wrote:

> "Dmitry A. Kazakov" <mai...@dmitry-kazakov.de> wrote in message

> news:1bp6zlpetr5l4.1...@40tude.net...

>> Because most of Ada semantics is OK. I don't see any mistakes. Even if they
>> were, it is irrelevant because I am looking for a more general model, where
>> mistake or not, it becomes just an implementation. So if you don't like a
>> particular built-in type for whatever reason, you make your own. No
>> problem.
>
> When you say "semantics", you're really only talking about the dynamic
> semantics, that is the runtime model. But the compile-time model is just as
> important. You would have to reproduce every feature and flaw of the
> existing compile-time model with a totally new underlying model. And doing
> that would be very, very complex.

Exactly.

> The problem is, when you do that, you'd have no way to determine whether or
> not it is really compatible. (After all, there is no formal model for Ada,
> and there never has been.) Ada's definition is just a mass of English text,
> and replacing it by a different mass of English text leaves one no practical
> way to prove compatibility.

Why should I need it if no existing Ada compiler does that? It will be as
compatible as any existing Ada implementation is. There is no reason to
require more than that, e.g. formal verification.

[Yannick Duchêne (Hibou57)]

Le Fri, 10 May 2013 09:48:26 +0200, Dmitry A. Kazakov
<mai...@dmitry-kazakov.de> a écrit:

>> Typing is too rigid to do a good job
>
> Typing is necessarily rigid because

I think he meant something else when he said “rigid”. I understood he
meant “not expressive enough”, “not always applicable”. I would say
“limited” (which is less ambiguous, except in terms of Ada wordings).

> it is on the next, higher level of
> power. Types describe the behavior of sets of values. Nothing you can do
> with individual values could come even close to that, except for trivial
> cases like enumeration types.

To be able to apply types beyond trivial cases, would need to have types
beyond trivial types. If it is supposed type must be as they already are,
there is not solution. If it is supposed the concept of type must be
defined, I would say it is what holds a set of axioms which will be
automatically pulled in a context with each reference to that type.
Actually, and except with discriminated records and pre/post condition
(which are not statically checked), the only static capability of types,
is to enumerate a simple list of values and list operations applicable to
that list of values. That's indeed too limited except for trivial cases.

[Simon Wright]

"Yannick Duchêne (Hibou57)" <yannick...@yahoo.fr> writes:

> Le Wed, 08 May 2013 02:18:44 +0200, Shark8 <onewing...@gmail.com>
> a écrit:
>> Aren't we getting ahead of ourselves don't we need RFPs for
>> [working-name] Project Babbage first?
>
> What is RFP here?

From Wikipedia,

"A request for proposal (RFP) is a solicitation made, often through a
bidding process, by an agency or company interested in procurement of
a commodity, service or valuable asset, to potential suppliers to
submit business proposals."

[Dmitry A. Kazakov]

On Fri, 10 May 2013 05:29:53 +0200, Yannick Duch�ne (Hibou57) wrote:

> I tried to express each validity condition with types and then type checking.

You cannot express program semantics in terms of types.

If you could express semantics, you won't need to program it.

[Yannick Duchêne (Hibou57)]

Le Fri, 10 May 2013 10:42:25 +0200, Dmitry A. Kazakov
<mai...@dmitry-kazakov.de> a écrit:

> On Fri, 10 May 2013 05:29:53 +0200, Yannick Duchêne (Hibou57) wrote:
>
>> I tried to express each validity condition with types and then type
>> checking.
>
> You cannot express program semantics in terms of types.
>
> If you could express semantics, you won't need to program it.

I don't understand what means “if you could express semantics, you won't
need to program it”. Or may be you meant the program is already in the
described semantic? If so, that's indeed be true, as the program can then
be derived, but there is not a single possible derivation, there are
typically multiple solutions, so the program still requires human
intervention to be generated.

Then if you see a types as set of axioms, and an instance of a type, as
something with which the axioms are all turned into true hypothesis (you
always need to prove hypothesis are true, before you can infer anything
which in turn is true, and that must be at the object level for program),
then you express semantic with types. And types in Ada, already holds
axioms. Its axiom language is just too limited (ranges and available
operations, that's near to all what's available).

Then again, semantic is expressed with axioms, or else that's not formal
semantic, and that's, say, natural language semantic, always subject to
possible subjective re‑interpretation (no deterministic interpretation).

I will be back to it later and I'm not versed in it enough so far, but
quickly, Isabelle/HOL (HOL stands for Higher Order Logic here), you have
something close to that. With Isabelle, axioms and theorems may be
organized into classes or local theories, which are kind of generic which
are to be instantiated, this instantiation being named “an interpretation
of a local theory”. You instantiate providing functions and values as
arguments.

With this kind of formal system, you typically go from a specification and
derives a program. Ada do it the other way, and go from the program and
prove it matches a specification later (either formally proving with SPARK
or using runtime‑check), or immediately for what is statically checked
(whether or not an operation exist, whether or not a value belongs to the
values of a type). But the concept does not imply a direction and would
make as much sense with the Ada way to go from program and later prove or
check its properties: in both case, you have to express what is to be
verified, whatever you do it before you generate a program or after a
program was authored.

If types could go beyond specification of a simple list of values (and we
already have a taste of that with discriminated records since always and
invariant predicates since Ada 2012) and available sub–programs, you won't
see types as you see it actually, it would look more expressive (and as a
consequence, safer) and less “rigid”.

[Dmitry A. Kazakov]

On Fri, 10 May 2013 13:18:12 +0200, Yannick Duchêne (Hibou57) wrote:

> Le Fri, 10 May 2013 10:42:25 +0200, Dmitry A. Kazakov
> <mai...@dmitry-kazakov.de> a écrit:
>
>> On Fri, 10 May 2013 05:29:53 +0200, Yannick Duchêne (Hibou57) wrote:
>>
>>> I tried to express each validity condition with types and then type
>>> checking.
>>
>> You cannot express program semantics in terms of types.
>>
>> If you could express semantics, you won't need to program it.
>
> I don't understand what means “if you could express semantics, you won't
> need to program it”. Or may be you meant the program is already in the
> described semantic?

Program implements semantics. If you define the semantics using some other
formalism you don't need the program anymore. The problem is that there is
no formalism, or else the formalism is too powerful for being computable.

> If so, that's indeed be true, as the program can then
> be derived, but there is not a single possible derivation, there are
> typically multiple solutions, so the program still requires human
> intervention to be generated.

Human intervention is needed to handle the semantics, not because of
multiplicity of implementations. You could choose them randomly.

> Then if you see a types as set of axioms, and an instance of a type, as
> something with which the axioms are all turned into true hypothesis (you
> always need to prove hypothesis are true, before you can infer anything
> which in turn is true, and that must be at the object level for program),
> then you express semantic with types. And types in Ada, already holds
> axioms. Its axiom language is just too limited (ranges and available
> operations, that's near to all what's available).

It is not axioms. However the axiomatic framework looks somewhat similar in
the sense that rules of logical inference could be compared with the types
algebra. But there is a sufficient difference that applying algebraic
operations in programming is imperative. You never present a ready type in
order to prove it being a result of some algebraic operations (=algebraic
type). Maybe only in academic studies. Rather you apply operations directly
and the result becomes algebraic merely per construction.

> Then again, semantic is expressed with axioms, or else that's not formal
> semantic, and that's, say, natural language semantic, always subject to
> possible subjective re‑interpretation (no deterministic interpretation).

No, the program semantics is the meaning of what the program does (to the
customer). That lies outside the language. Not to confuse with the language
semantics which describes how to execute the code (to the CPU).

> I will be back to it later and I'm not versed in it enough so far, but
> quickly, Isabelle/HOL (HOL stands for Higher Order Logic here), you have
> something close to that. With Isabelle, axioms and theorems may be
> organized into classes or local theories, which are kind of generic which
> are to be instantiated, this instantiation being named “an interpretation
> of a local theory”. You instantiate providing functions and values as
> arguments.

I am not familiar with that, but formal methods are always a meta language
relatively to the programming language and its type system, which are the
object language for them. You never mix the two.

> With this kind of formal system, you typically go from a specification and
> derives a program.

That won't work. If you can derive the program (in the object language) you
don't need the object language anymore. If that indeed works, as it does
with the Assembly language, you move up to the meta language (higher-level
programming language in this case) and forget about silly lower-level
stuff. Regarding specification languages and modeling language I have
serious reservations about them being capable to replace Ada and other
general purpose languages.

> If types could go beyond specification of a simple list of values (and we
> already have a taste of that with discriminated records since always and
> invariant predicates since Ada 2012) and available sub–programs, you won't
> see types as you see it actually, it would look more expressive (and as a
> consequence, safer) and less “rigid”.

I don't see how Ada 2012 makes it more expressive. It did not extend types
algebra in any significant way.

BTW, static checks if have something to do with expressiveness, then by
hampering it. Because it is evident that the more powerful constructs you
have, less you could prove about their outcome. The most notorious example
is goto. The art of language design is to deploy least powerful constructs,
while keeping it useful for programming.

[Yannick Duchêne (Hibou57)]

Le Fri, 10 May 2013 14:15:35 +0200, Dmitry A. Kazakov
<mai...@dmitry-kazakov.de> a écrit:

>> If so, that's indeed be true, as the program can then
>> be derived, but there is not a single possible derivation, there are
>> typically multiple solutions, so the program still requires human
>> intervention to be generated.
>
> Human intervention is needed to handle the semantics, not because of
> multiplicity of implementations. You could choose them randomly.

You can't choose randomly, the program must have runtime properties as
well.

Another case, is with what in the domain is known as shallow embedding;
this means you model the target language (or a subset of it or some
constructs of it) in the terms of the formal language, then write the
program in the target language indirectly writing proof involving these
constructs (I mean, the ones representing the target language). Then, you
ends with a program in the target language with syntactic transformations.
There is another way to do, which is named deep embedding, but I don't
really know it and don't like it anyway.

In all cases (either one of the three), the target language is always
there, it just appears at different stage, sometime immediately from the
start, sometime only at the final stage.

>> With this kind of formal system, you typically go from a specification
>> and
>> derives a program.
>
> That won't work. If you can derive the program (in the object language)
> you don't need the object language anymore.

You really can't say “it won't work”, since there are people who already
do this, and that works, and that's not restricted to “academic
experiments”. The object language is still needed, as further more, Ada
had even been famously involved as a target language with the B formal
method (whose target languages may be either Ada or C). I know it was used
in france for the software of some subway lines in Paris (they used B and
Ada 95 if I'm not wrong). This was from specification to Ada, and not from
Ada to proof (as SPARK do).

[Yannick Duchêne (Hibou57)]

Le Fri, 10 May 2013 14:40:00 +0200, Yannick Duchêne (Hibou57)
<yannick...@yahoo.fr> a écrit:

> Le Fri, 10 May 2013 14:15:35 +0200, Dmitry A. Kazakov
> <mai...@dmitry-kazakov.de> a écrit:
>>> If so, that's indeed be true, as the program can then
>>> be derived, but there is not a single possible derivation, there are
>>> typically multiple solutions, so the program still requires human
>>> intervention to be generated.
>>
>> Human intervention is needed to handle the semantics, not because of
>> multiplicity of implementations. You could choose them randomly.
>
> You can't choose randomly, the program must have runtime properties as
> well.

I should have given another example, a more obvious one: as the program
derivation is a consequence of a proof the specification is satisfiable
(the proof and the program are the same thing), automated program
generation from the specification, would implies automated proof. This
does not exist with the actual technology, if not for trivial stuffs. So
far you have proof assistants, not automated provers (just some steps of
proofs may be automated, if the user request some help from the assistant…
but it may fail and it's not usable for program generation as far as I
know).

[Dmitry A. Kazakov]

On Fri, 10 May 2013 14:40:00 +0200, Yannick Duchêne (Hibou57) wrote:

> Le Fri, 10 May 2013 14:15:35 +0200, Dmitry A. Kazakov
> <mai...@dmitry-kazakov.de> a écrit:
>>> If so, that's indeed be true, as the program can then
>>> be derived, but there is not a single possible derivation, there are
>>> typically multiple solutions, so the program still requires human
>>> intervention to be generated.
>>
>> Human intervention is needed to handle the semantics, not because of
>> multiplicity of implementations. You could choose them randomly.
>
> You can't choose randomly, the program must have runtime properties as
> well.

The only properties a program must have are derived from its semantics, per
definition.

>>> With this kind of formal system, you typically go from a specification
>>> and derives a program.
>>
>> That won't work. If you can derive the program (in the object language)
>> you don't need the object language anymore.
>
> You really can't say “it won't work”, since there are people who already
> do this,

That is their problem. People do crazy things all the time.

[Yannick Duchêne (Hibou57)]

Le Fri, 10 May 2013 15:54:40 +0200, Dmitry A. Kazakov
<mai...@dmitry-kazakov.de> a écrit:

>>> Human intervention is needed to handle the semantics, not because of
>>> multiplicity of implementations. You could choose them randomly.
>>
>> You can't choose randomly, the program must have runtime properties as
>> well.
>
> The only properties a program must have are derived from its semantics,
> per definition.

The time required for a computation, the memory used, are not part of the
semantic. Computational complexity is not semantic.

>>> That won't work. If you can derive the program (in the object language)
>>> you don't need the object language anymore.
>>
>> You really can't say “it won't work”, since there are people who already
>> do this,
>
> That is their problem. People do crazy things all the time.

What's crazy with this?

[Dmitry A. Kazakov]

On Fri, 10 May 2013 16:01:46 +0200, Yannick Duchêne (Hibou57) wrote:

> Le Fri, 10 May 2013 15:54:40 +0200, Dmitry A. Kazakov
> <mai...@dmitry-kazakov.de> a écrit:
>>>> Human intervention is needed to handle the semantics, not because of
>>>> multiplicity of implementations. You could choose them randomly.
>>>
>>> You can't choose randomly, the program must have runtime properties as
>>> well.
>>
>> The only properties a program must have are derived from its semantics,
>> per definition.
>
> The time required for a computation, the memory used, are not part of the
> semantic.

It is for RT or else irrelevant.

> Computational complexity is not semantic.

And so irrelevant.

>>>> That won't work. If you can derive the program (in the object language)
>>>> you don't need the object language anymore.
>>>
>>> You really can't say “it won't work”, since there are people who already
>>> do this,
>>
>> That is their problem. People do crazy things all the time.
>
> What's crazy with this?

Because it is impossible to do. When meant seriously beyond academic
exercises, it is most likely undecidable, incomputable, halting etc.

[Yannick Duchêne (Hibou57)]

Le Fri, 10 May 2013 10:12:22 +0200, Yannick Duchêne (Hibou57)
<yannick...@yahoo.fr> a écrit:

> Actually, and except with discriminated records and pre/post condition
> (which are not statically checked), the only static capability of types,
> is to enumerate a simple list of values and list operations applicable
> to that list of values. That's indeed too limited except for trivial
> cases.

I was wrong, forgetting an important one: Ada types can be described by
their origins too. I mean the thing you get when you tell a type has only
a private full definition and have functions returning an instance of that
type. These functions are the origin of instances, and more or less
express what instances are, as the assertions about what's returned by the
function, finally becomes assertions of the type. These functions are
finally part of the type definition too. That's informal specifications,
while that still opens the door to better.

That's a consequence of type being matched by name and not by structure
(that's a reason why type matched by name is better, more expressive).

As a summary of what's available to describe a type:

* list of contiguous values (unfortunately, holes are not allowed,
except using static predicates);
* list of applicable operations (unfortunately, very poorly specified:
only signature);
* invariant predicate (unfortunately, not statically checked, except
with static predicate);
* functions generating the initial values (for private types only, not
trustable otherwise).

(did I still forget one?)

Not enough, while finally not that bad.

[Yannick Duchêne (Hibou57)]

Le Fri, 10 May 2013 16:27:42 +0200, Dmitry A. Kazakov
<mai...@dmitry-kazakov.de> a écrit:

>> The time required for a computation, the memory used, are not part of
>> the
>> semantic.
>
> It is for RT or else irrelevant.
>
>> Computational complexity is not semantic.
>
> And so irrelevant.

I've never asserted semantic is everything (and even suggested the
opposite). Runtime properties is another aspect. Not the same methods, not
the same formalisms, these are orthogonal aspects (or more or less).

> Because it is impossible to do. When meant seriously beyond academic
> exercises, it is most likely undecidable, incomputable, halting etc.

That's not impossible nor academic only, that's used for real life case (I
gave an example, there are many others). Generating program from
specification does not prevent nor disallow proofs of bounded runtime
requirement.

[Yannick Duchêne (Hibou57)]

Le Thu, 09 May 2013 09:33:54 +0200, Dmitry A. Kazakov
<mai...@dmitry-kazakov.de> a écrit:

> Not mixing types means
> that you could not have subprograms with more than one argument.

More than that, this would mean you could not even have composite type. To
understand it, think of the sub‑program parameters as a implicit record of
some implicit type.

So obviously, mixing types is unavoidable and Ada already knows it (but it
does not always knowns mixing types means creating a new type, or else,
sometime it just knowns anonymous and implicit types).

[Niklas Holsti]

On 13-05-10 06:29 , Yannick Duchêne (Hibou57) wrote:
> Le Fri, 10 May 2013 00:19:14 +0200, Randy Brukardt

...

>> Yes, because we need to move beyond typing to other forms of static error

>> detection. Typing is too rigid to do a good job -- you need to include
>> statically known information about the contents of variables and
>> parameters,
>> which can change from line-to-line in a program.
>
> I feel the same. I often though typing can't do everything if it comes
> with value type checking, while in some occasions, I tried to express
> each validity condition with types and then type checking (that ends to
> be crazy, indeed). A simple example, is paired invocation, where

> whenever a sub‑program is is invoked, sooner or later, another
> sub‑program must be invoked too on the same argument, ex. like `Open`
> and later `Close`. This cannot be expressed with types and indeed
> requires assertions.

Are you familiar with the "typestate" concept? As I understand it, the
intent is to check state-sequence rules such as Open-followed-by-Close.
See http://en.wikipedia.org/wiki/Typestate_analysis.

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

[Niklas Holsti]

On 13-05-10 07:34 , Yannick Duchêne (Hibou57) wrote:
> Le Wed, 08 May 2013 02:18:44 +0200, Shark8 <onewing...@gmail.com> a
> écrit:
>> Aren't we getting ahead of ourselves don't we need RFPs for
>> [working-name] Project Babbage first?
>
> What is RFP here?

Probably "Request For Proposal" was meant. In other words, a general
invitation for interested parties to submit proposals for a new
language, to satisfy some requirements posited in the RFP.

[Yannick Duchêne (Hibou57)]

Le Fri, 10 May 2013 20:04:42 +0200, Niklas Holsti
<niklas...@tidorum.invalid> a écrit:

> Are you familiar with the "typestate" concept? As I understand it, the
> intent is to check state-sequence rules such as Open-followed-by-Close.
> See http://en.wikipedia.org/wiki/Typestate_analysis.

I did not knew it before. Thanks for the pointer, that's always good to
know the name of things (may be interesting to see if it's related to
temporal logic).

Just for the anecdote, the way I tried to solve it with static check, was
using typed tokens, returned and/or required by operations. Say an
operation B is allowed to occur only if an operation A occurred before.
The operation A returns a value of type TA. As B requires to occurs only
after A, then it can requires a token of type TA as its input arguments.
Similarly, B may return a token of type TB, which may be required by any
operation which must occur only after B.

To be trustable, it requires TA, TB and so on, cannot be created out of
control of A, B an so on, so it must be limited types with unknown
discriminant (the latter to force initialization).

Well, that looks a nice hack, it's statically checked, but that's limited
and bloats everything, and near to be unusable due to the required
initialisation (imagine writing a program all in the declarative part).
Then, no way to tell B must always occur later after A if ever A occurred.
It also only know about simple sequence, and can't differentiate between
A;B;C and A;C. It can't differentiate neither between instances (there is
no way to check a token was return by an operation on this or that
instance). So finally, I gave up with this hack.

That's what I was thinking about, when I said it can indeed become crazy
to try to express all validity rules using the type system.

There is another less restrictive way to do, except it cannot statically
check, which ends to be the same as pre/post, and that's finally better to
just use pre/post in this case (at that time, Ada 2012 was not there).

[Randy Brukardt]

"Dmitry A. Kazakov" <mai...@dmitry-kazakov.de> wrote in message

news:1jc46ynzptlxm.1...@40tude.net...

> On Thu, 9 May 2013 16:43:29 -0500, Randy Brukardt wrote:

...

>> The problem is, when you do that, you'd have no way to determine whether
>> or
>> not it is really compatible. (After all, there is no formal model for
>> Ada,
>> and there never has been.) Ada's definition is just a mass of English
>> text,
>> and replacing it by a different mass of English text leaves one no
>> practical
>> way to prove compatibility.
>
> Why should I need it if no existing Ada compiler does that? It will be as
> compatible as any existing Ada implementation is. There is no reason to
> require more than that, e.g. formal verification.

Because there is no other way to tell. No one is going to implement it (or
put it into the Standard) unless they know that it is "at least as
compatible as an existing Ada implementation". You're going to have to prove
that somehow, and that proof is going to have to be at least semi-formal,
because it is going to have to be convincing. Handwaving in a forum like
this is not a convincing proof.

Randy.

[Randy Brukardt]

"Niklas Holsti" <niklas...@tidorum.invalid> wrote in message
news:av4r5q...@mid.individual.net...

> On 13-05-10 06:29 , Yannick Duch�ne (Hibou57) wrote:
>> Le Fri, 10 May 2013 00:19:14 +0200, Randy Brukardt
> ...
>>> Yes, because we need to move beyond typing to other forms of static
>>> error
>>> detection. Typing is too rigid to do a good job -- you need to include
>>> statically known information about the contents of variables and
>>> parameters,
>>> which can change from line-to-line in a program.
>>
>> I feel the same. I often though typing can't do everything if it comes
>> with value type checking, while in some occasions, I tried to express
>> each validity condition with types and then type checking (that ends to
>> be crazy, indeed). A simple example, is paired invocation, where

>> whenever a sub-program is is invoked, sooner or later, another
>> sub-program must be invoked too on the same argument, ex. like `Open`

>> and later `Close`. This cannot be expressed with types and indeed
>> requires assertions.
>
> Are you familiar with the "typestate" concept? As I understand it, the
> intent is to check state-sequence rules such as Open-followed-by-Close.
> See http://en.wikipedia.org/wiki/Typestate_analysis.

Thanks for the reference. I doubted that the idea was new (there are no new
ideas), but I hadn't heard of it before. I don't like the name much, because
it feeds into the "type is everything" madness that Dmitry exhibits so
clearly. This clearly (just like constraints and predicates) is something
that's added in addition to type analysis; it's not part of it at all.

Randy.

[Randy Brukardt]

"Yannick Duch�ne (Hibou57)" <yannick...@yahoo.fr> wrote in message
news:op.wwung605ule2fv@cardamome...
Le Fri, 10 May 2013 00:19:14 +0200, Randy Brukardt <ra...@rrsoftware.com>
a �crit:

>> Again, no one said anything about them being isolated. Although I do
>> think
>> that vast majority of types ought to be separate from other types -- the
>> interactions being handled in the operations, not in the types
>> themselves.
>

>Right, except while you say this, the only static check sub-programs or
>primitive operations provide, is the one applying on the types of their
>arguments. So there is nothing handled by operations (at least, so far).
>
>The point is still good enough, as at first sight, seems there are
>operations which cannot said to be owned by a single type, so that may
>looks hard to focus on type with this picture. Or else, there is a need
>for a type representing sub-program signature (something I wanted to reply
>to Dmitry in another message), the arguments tuple, then optionally the
>result tuple, and optionally both tuples, say the type of a transition as
>an example. With this, interactions between types can be represented with
>types.

One of the reasons I chose "profile" for the name of the thingy that I was
describing on top of types was that I expected it to include profile
operations. That's because I figured that a redesign of Ada would have
first-class subprogram types; (along with subprogram objects); there is no
good reason to use explicit "access" values for this. (Object access values
are so different from the subprogram kind that there is virtually no
commonality, so it's confusing to treat them as the same sort of thing.) And
of course, any first-class type would need an associated profile.

Randy.

[Randy Brukardt]

"Dmitry A. Kazakov" <mai...@dmitry-kazakov.de> wrote in message

news:1oy5rmprgawqs.1jz36okze0xju$.dlg@40tude.net...

> On Thu, 9 May 2013 17:19:14 -0500, Randy Brukardt wrote:
>
>> "Dmitry A. Kazakov" <mai...@dmitry-kazakov.de> wrote in message
>> news:12gn9wvv1gwfk.1...@40tude.net...
>>> On Wed, 8 May 2013 15:27:50 -0500, Randy Brukardt wrote:
>>>
>>>> "Dmitry A. Kazakov" <mai...@dmitry-kazakov.de> wrote in message
>>>> news:nd22gfeezrwf$.tlj4yyygrwq3$.dlg@40tude.net...
>>>> ...
>>>>> Each time you do something with a type you get another one. Otherwise
>>>>> it
>>>>> becomes untyped.
>>>>
>>>> That way leads to madness, I think. It's better for "types" to be
>>>> fairly
>>>> weak and interoperable.
>>>
>>> Weak typing is better?
>>
>> Yes, because we need to move beyond typing to other forms of static error
>> detection.
>
> Based on what? On individual values?

What I was calling profiles; Nicolas has provided a reference that says its
known as "typestate" analysis. It sits on top of types providing more
information for static checking.


...

>> I want checking that is *stronger* than what can be provided by
>> statically
>> applied types. Trying to get it by extending the type model directly is
>> madness, especially as it makes sharing much less possible.
>
> No, you will lose a whole universe of checks without gaining anything
> useful. Checks of individual values have limits imposed by computability.
> Furthermore, focusing on values, you will kill software engineering. Reuse
> is what is really important. Checks are only a tool to make reuse safer.

I'm adding on top of types, not in place of them. And I don't see what would
change about software engineering -- that's about visibility control (i.e.
packages) and strong checking. OOP-madness (inheritance and the like) adds
little to the ability for reuse -- in large part because it's almost never
appropriate. (The fact that inheritance is only additive kills most reuse --
a different abstraction is, for the lack of a better term, different -- it's
not going to share all or even a lot of the operations.)

...
> Not at all. It is substitutability which is context-depended ...

Bow down to the great god of "substitutability". The real crux of
OOP-madness -- this is fantasy that does not exist in real problems.


...

>> In particular, I think the Ada model of few types (essentially, initial
>> declaration equivalent) is the way to go; all of the action should be on
>> enhancing subtypes and subprograms such that static checks are possible
>> (by
>> combining constraints, null exclusions, predicates, parameter/result
>> profiles, and possibly other things into an integrated concept).
>
> Concept of what? You are not yet ready with types and want to introduce
> something of unknown nature? How these new things will interact each
> other,
> values, types, classes, packages. What is there to check if the properties
> of are nowhere stated, meaning is undefined?

Yes, because I'm starting over. That means a nearly clean slate. I want to
clean up all of those interactions (which are currently a mess), and that
means rethinking everything. There's no point to small tweaks to Ada (if you
want model changes), you simply can't get there. You'll just end up adding
more "gazebos", as you once put it.

>>> Strong typing is an ability to distinguish types. Not mixing types means
>>> that you could not have subprograms with more than one argument. It is
>>> just crazy.
>>
>> Certainly when you invent ideas like this, which have nothing to do with
>> anything that I said or was thinking about. Obviously, operations of one
>> type need parameters of another type. But your OOP-fever means that you
>> think that this somehow implies the types are related.
>
> What else a relationship is? Types deal with values and operations. There
> is nothing else. Since values are not shared (Ada is typed so far), the
> only thing which may bind two types is a shared operation.

I don't think operations have anything to do with types: they *use* types,
they aren't part of them in any way. The "profile" of objects determines
what operations can be used with them.

Keep in mind that what I've trying to do here is to get the sort of
statically checked preconditions that you keep saying are necessary. That
requires formalizing at least part of the state of objects, because a model
that can't statically check whether files are open in I/O is a pretty
useless model.

You may describe this is terms of a different formalism, but as far as I'm
concerned, that's simply trying to confuse the issue. It's confusing enough
without that kind of "help".

Randy.

[Randy Brukardt]

"Dmitry A. Kazakov" <mai...@dmitry-kazakov.de> wrote in message

news:1q07vm77kfwla$.1cz0xwxspxhay.dlg@40tude.net...

> On Thu, 9 May 2013 16:33:55 -0500, Randy Brukardt wrote:
>
>> As usual, I pretty much totally disagree with your thinking here. The
>> last
>> statement is trivially true, of course, but so what? A program has to be
>> built on top of a handful of "big" abstractions. And for each of those
>> "big"
>> abstractions, there has to be a single type which takes the lead
>> (probably
>> with a family of other types in support).
>
> Takes the lead, how? An abstraction including Employer, Employee, Factory,
> Salary, Time, Duration, Integer, Address, Gender, Age ... Who takes the
> "lead"?

The container that wraps those things up, of course. And if there is no
container, then they're clearly all separate abstractions that have to be
treated that way.

>> In bigger systems, each of those abstractions corresponds to a subsystem
>> (in
>> Ada, that's best modeled as a family of child packages). Inside each of
>> those subsystems, you'll have another family of types. But the majority
>> of
>> these types should not extend beyond the subsystem.
>
> How these subsystems are going to interact to each other?

As little as possible. That's necessary to reduce coupling. Beyond that,
almost exclusively by containment, that is that one abstraction contains
components of another.

>> You seem to claim that all types are equally important, which is obvious
>> nonsense.
>
> Yes, I say that unimportant types need not to be exposed in public
> interfaces.
>
> Everything declared in the *same* scope is equally important, or else you
> have a design issue.

What utter nonsense.

Ada.Text_IO defines Count, File_Type, File_Mode, Field, and Number_Base
types. If you think these are all equally important for the primary task of
doing I/O, you have a real problem with perspective. File_Type does all of
the work, while the rest just raise the abstraction level a bit.

>> Claiming that the
>> lookup result enumeration ("Found", "Missing", "Ambiguous") is as
>> important
>> as the symbol table data structure is insane.
>
> How do you measure importance?

You don't have to quantify it in order for it to be a useful idea. If it's
not obvious, your design is already too unstructured.

> It is not a simple question. If you tried to roll up a measure and apply
> it
> most commonly used types, you would probably see your the idea of leading
> types (which, BTW, is one of most damaging ideas in OO ever) quickly
> falling apart.

I don't see any reason to quantify "importance". Almost every package that
I've designed (as opposed to tossed stuff in, and there are a number of
those. ;-) has a single type around which everything else is built. There
are a few (like the containers) that have a pair of such types -- but that
always proves to be a problem in practice.

I don't quite see what this has to do with OOP; I've used this design
pattern since I first encountered a package (in the form of a Modula module)
in 1978. That predates OOP doctrine by a number of years (some of the
principles already existed, especially in Simula, at that point).

Randy.

[Simon Wright]

"Dmitry A. Kazakov" <mai...@dmitry-kazakov.de> writes:

> On Thu, 9 May 2013 16:33:55 -0500, Randy Brukardt wrote:
>
>> As usual, I pretty much totally disagree with your thinking here. The last
>> statement is trivially true, of course, but so what? A program has to be
>> built on top of a handful of "big" abstractions. And for each of those "big"
>> abstractions, there has to be a single type which takes the lead (probably
>> with a family of other types in support).
>
> Takes the lead, how? An abstraction including Employer, Employee, Factory,
> Salary, Time, Duration, Integer, Address, Gender, Age ... Who takes the
> "lead"?

Randy said there would be a handful of abstractions, not just one. Just
taking a guess here, but in this case those would probably be Employer,
Employee, and possibly Factory. I don't see how you can seriously
suggest that Integer is a candidate.

[Dmitry A. Kazakov]

On Fri, 10 May 2013 19:42:37 -0500, Randy Brukardt wrote:

> "Dmitry A. Kazakov" <mai...@dmitry-kazakov.de> wrote in message
> news:1oy5rmprgawqs.1jz36okze0xju$.dlg@40tude.net...
>> On Thu, 9 May 2013 17:19:14 -0500, Randy Brukardt wrote:
>>
>>> "Dmitry A. Kazakov" <mai...@dmitry-kazakov.de> wrote in message
>>> news:12gn9wvv1gwfk.1...@40tude.net...
>>>> On Wed, 8 May 2013 15:27:50 -0500, Randy Brukardt wrote:
>>>>
>>>>> "Dmitry A. Kazakov" <mai...@dmitry-kazakov.de> wrote in message
>>>>> news:nd22gfeezrwf$.tlj4yyygrwq3$.dlg@40tude.net...
>>>>> ...
>>>>>> Each time you do something with a type you get another one. Otherwise
>>>>>> it becomes untyped.
>>>>>
>>>>> That way leads to madness, I think. It's better for "types" to be
>>>>> fairly weak and interoperable.
>>>>
>>>> Weak typing is better?
>>>
>>> Yes, because we need to move beyond typing to other forms of static error
>>> detection.
>>
>> Based on what? On individual values?
>
> What I was calling profiles; Nicolas has provided a reference that says its
> known as "typestate" analysis. It sits on top of types providing more
> information for static checking.

That applies to stateful types only. Not every type is stateful. Bringing
state into objects is considered bad practice. So bad, that it motivated
some people to invent whole programming paradigms to avoid stateful object,
e.g. functional programming. The sole idea of FP is to sweep states under
the carpet.

Stateful OOA/D vs. stateless FP are both extremes, but in any case one
should not base the language design (!) on exposing states. State machines
existed since the beginning of computing. As a compiler designer you should
know better how difficult, almost impossibly, it is to use state machine
patterns.

>>> I want checking that is *stronger* than what can be provided by statically
>>> applied types. Trying to get it by extending the type model directly is
>>> madness, especially as it makes sharing much less possible.
>>
>> No, you will lose a whole universe of checks without gaining anything
>> useful. Checks of individual values have limits imposed by computability.
>> Furthermore, focusing on values, you will kill software engineering. Reuse
>> is what is really important. Checks are only a tool to make reuse safer.
>
> I'm adding on top of types, not in place of them.

On top of something which formalization of you call madness?

>>>> Strong typing is an ability to distinguish types. Not mixing types means
>>>> that you could not have subprograms with more than one argument. It is
>>>> just crazy.
>>>
>>> Certainly when you invent ideas like this, which have nothing to do with
>>> anything that I said or was thinking about. Obviously, operations of one
>>> type need parameters of another type. But your OOP-fever means that you
>>> think that this somehow implies the types are related.
>>
>> What else a relationship is? Types deal with values and operations. There
>> is nothing else. Since values are not shared (Ada is typed so far), the
>> only thing which may bind two types is a shared operation.
>
> I don't think operations have anything to do with types: they *use* types,
> they aren't part of them in any way. The "profile" of objects determines
> what operations can be used with them.

Dynamically? Because if statically, then that is exactly what is called a
type. When dynamically, why bother yourself inventing another SmallTalk? It
is already there.

> Keep in mind that what I've trying to do here is to get the sort of
> statically checked preconditions that you keep saying are necessary.

First of all, there are preconditions of operations and the precondition
put on individual calls. I don't know which one you mean here. But the
preconditions of operations must be statically true. Meaning: a declared
operation can be called anywhere. The client may annotate his calls to the
operation with additional preconditions related to the logic of the program
that uses the operation. These are not the property of the operation and
unrelated to the type.

The idea that the precondition of first kind should depend on the state of
the objects involved in the operation is a very, VERY bad idea.

[Dmitry A. Kazakov]

You didn't answer the question. If it goes without a proof now, why can it
continue so?

[Georg Bauhaus]

On 11.05.13 08:37, Dmitry A. Kazakov wrote:
> First of all, there are preconditions of operations and the precondition
> put on individual calls. I don't know which one you mean here. But the
> preconditions of operations must be statically true. Meaning: a declared
> operation can be called anywhere. The client may annotate his calls to the
> operation with additional preconditions related to the logic of the program
> that uses the operation. These are not the property of the operation and
> unrelated to the type.
>
> The idea that the precondition of first kind should depend on the state of
> the objects involved in the operation is a very, VERY bad idea.

How do you specify the preconditions of the second kind (on individual
calls) in such a way that a programmer, wishing to calling these operations,
ensures the calls won't fail as a consequence of violating these
preconditions?

[Yannick Duchêne (Hibou57)]

Le Sat, 11 May 2013 03:00:39 +0200, Randy Brukardt <ra...@rrsoftware.com>
a écrit:

>> Yes, I say that unimportant types need not to be exposed in public
>> interfaces.
>>
>> Everything declared in the *same* scope is equally important, or else
>> you
>> have a design issue.
>
> What utter nonsense.
>
> Ada.Text_IO defines Count, File_Type, File_Mode, Field, and Number_Base
> types. If you think these are all equally important for the primary task
> of
> doing I/O, you have a real problem with perspective. File_Type does all
> of
> the work, while the rest just raise the abstraction level a bit.

I don't feel Dmitry talked about amount of work done when he introduced
“importance”. I'm guessing it was about importance for the abstraction and
so its usability. That also depend on the abstraction level. The most
abstract is surely File_Type, then File_Mode comes next while not
necessarily, then Field and Number_Base, depends if these specialisations
are required.

If something is said not that much important, it should be removable, or
else, what means not important? If that's not important in some case while
important for some others, then there should be different child packages
or parallel hierarchy (with one withing another). Seems to be basic design
rules.

[Dmitry A. Kazakov]

On Fri, 10 May 2013 20:00:39 -0500, Randy Brukardt wrote:

> "Dmitry A. Kazakov" <mai...@dmitry-kazakov.de> wrote in message
> news:1q07vm77kfwla$.1cz0xwxspxhay.dlg@40tude.net...
>> On Thu, 9 May 2013 16:33:55 -0500, Randy Brukardt wrote:
>>
>>> As usual, I pretty much totally disagree with your thinking here. The last
>>> statement is trivially true, of course, but so what? A program has to be
>>> built on top of a handful of "big" abstractions. And for each of those "big"
>>> abstractions, there has to be a single type which takes the lead
>>> (probably with a family of other types in support).
>>
>> Takes the lead, how? An abstraction including Employer, Employee, Factory,
>> Salary, Time, Duration, Integer, Address, Gender, Age ... Who takes the
>> "lead"?
>
> The container that wraps those things up, of course. And if there is no
> container, then they're clearly all separate abstractions that have to be
> treated that way.

How to separate Employer and Employee?

>>> In bigger systems, each of those abstractions corresponds to a subsystem
>>> (in Ada, that's best modeled as a family of child packages). Inside each of
>>> those subsystems, you'll have another family of types. But the majority of
>>> these types should not extend beyond the subsystem.
>>
>> How these subsystems are going to interact to each other?
>
> As little as possible.

It does not tell how.

>>> You seem to claim that all types are equally important, which is obvious
>>> nonsense.
>>
>> Yes, I say that unimportant types need not to be exposed in public
>> interfaces.
>>
>> Everything declared in the *same* scope is equally important, or else you
>> have a design issue.
>
> What utter nonsense.
>
> Ada.Text_IO defines Count, File_Type, File_Mode, Field, and Number_Base
> types. If you think these are all equally important for the primary task of
> doing I/O, you have a real problem with perspective. File_Type does all of
> the work, while the rest just raise the abstraction level a bit.

In which sense? From the implementation point of view GNAT's File_Type is
an address or integer, if I correctly remember. It does nothing. From the
user's point of view Put_Line, Get_Line do not even mention File_Type. And
there are lot of questions to Text_IO design anyway. One problem is worth
mentioning. It is a typical God-class design:

http://en.wikipedia.org/wiki/God_class

This is the destination point of the idea of equivalence of object and
abstraction, a very OO idea. What you are talking about is basically
classic OOA/D put in different terms.

> I don't see any reason to quantify "importance".

In order to prove your point?

[Yannick Duchêne (Hibou57)]

Le Sat, 11 May 2013 02:18:30 +0200, Randy Brukardt <ra...@rrsoftware.com>
a écrit:

> Thanks for the reference. I doubted that the idea was new (there are no
> new
> ideas), but I hadn't heard of it before. I don't like the name much,
> because
> it feeds into the "type is everything" madness that Dmitry exhibits so
> clearly. This clearly (just like constraints and predicates) is something
> that's added in addition to type analysis; it's not part of it at all.

I agree this cannot be checked with typing and needs an additional
analysis, that seems obvious. But where would you state the predicates to
be verified, if not in something which is bounded to the type? The type
definition it self or its methods, is the only one place where to requires
the predicates to be verified; this can't move around freely, this have to
be bound to it in some way.

[Georg Bauhaus]

On 10.05.13 16:27, Dmitry A. Kazakov wrote:
> On Fri, 10 May 2013 16:01:46 +0200, Yannick Duchêne (Hibou57) wrote:
>
>> Le Fri, 10 May 2013 15:54:40 +0200, Dmitry A. Kazakov
>> <mai...@dmitry-kazakov.de> a écrit:
>>>>> Human intervention is needed to handle the semantics, not because of
>>>>> multiplicity of implementations. You could choose them randomly.
>>>>
>>>> You can't choose randomly, the program must have runtime properties as
>>>> well.
>>>
>>> The only properties a program must have are derived from its semantics,
>>> per definition.
>>
>> The time required for a computation, the memory used, are not part of the
>> semantic.
>
> It is for RT or else irrelevant.

"It" becomes a compile time thing as soon as we can state meaningfully
(hence, checked by the compiler), in source text, that some part of a
program must (and will) make bounded use of resources, where "bounded"
is not trivially true but specifically true of the program being
translated.

Semi-formally, the data structure parts of C++ and Ada have made a
move in this direction by advising that certain language-provided
operations on containers be bounded specifically.

It will be sufficient if compilers decide this when translating the
very few (compared to the possible) of the non-undecidable programs
that warrant our profession.

[Dmitry A. Kazakov]

On Sat, 11 May 2013 06:31:57 +0100, Simon Wright wrote:

> "Dmitry A. Kazakov" <mai...@dmitry-kazakov.de> writes:
>
>> On Thu, 9 May 2013 16:33:55 -0500, Randy Brukardt wrote:
>>
>>> As usual, I pretty much totally disagree with your thinking here. The last
>>> statement is trivially true, of course, but so what? A program has to be
>>> built on top of a handful of "big" abstractions. And for each of those "big"
>>> abstractions, there has to be a single type which takes the lead (probably
>>> with a family of other types in support).
>>
>> Takes the lead, how? An abstraction including Employer, Employee, Factory,
>> Salary, Time, Duration, Integer, Address, Gender, Age ... Who takes the
>> "lead"?
>
> Randy said there would be a handful of abstractions, not just one.

In a program, but in a package, he said, there should be just one. Which is
a nonsense to me.

> Just
> taking a guess here, but in this case those would probably be Employer,
> Employee, and possibly Factory. I don't see how you can seriously
> suggest that Integer is a candidate.

What is wrong with Integer? I also asked for a measure. My suggestion is
that the measure he implicitly uses is the man-hours invested in the coding
the type in question!

[Yannick Duchêne (Hibou57)]

Le Sat, 11 May 2013 02:22:58 +0200, Randy Brukardt <ra...@rrsoftware.com>
a écrit:

> One of the reasons I chose "profile" for the name of the thingy that I
> was
> describing on top of types was that I expected it to include profile
> operations. That's because I figured that a redesign of Ada would have
> first-class subprogram types; (along with subprogram objects); there is
> no
> good reason to use explicit "access" values for this.

I like the idea (it happened I missed the same with some use case).

> (Object access values
> are so different from the subprogram kind that there is virtually no
> commonality, so it's confusing to treat them as the same sort of thing.)

Sure, unless someone want to allocate executable memory and dynamically
create a sub‑program there in some way (that's feasible at least on Linux
and suggested by POSIX), but that would be a different type of sub‑program
and access anyway.

[Yannick Duchêne (Hibou57)]

Le Sat, 11 May 2013 02:42:37 +0200, Randy Brukardt <ra...@rrsoftware.com>
a écrit:

>> Not at all. It is substitutability which is context-depended ...
>
> Bow down to the great god of "substitutability". The real crux of
> OOP-madness -- this is fantasy that does not exist in real problems.

As often, depends on the use case and domain (with proofs and analysis,
substitutability is important).

Was just thinking about something to please both: don't see
substitutability as a requirement, but as something optionally provided;
there could be a way to assert substitutability when something can provide
it, while not requiring it all the time. That would be a kind of
noticeable property which could be explicitly created and asserted.

There are people who need it, there are others who really don't care.

[Dmitry A. Kazakov]

"Fail" is a wrong word here. The right wording is ensuring postconditions.
That is completely unrelated issue, IMO.

I have a feeling that people confuse typing with this, which is basically
program correctness en large. You cannot ensure program correctness through
types. And since full correctness proof is unachievable anyway I want to
separate it from types.

Second kind checks (e.g. SPARK) should be optional so that the programmer
would add or remove checks depending on requirements and provability.

Especially because there is also a big difference in the design of type
checks and correctness checks. We design types top-down, at least the most
important ones. Type design is frequently irreversible, few things can be
changed later without big troubles. It is almost waterfall. On the
contrary, the correctness checks are bottom-up. You probably never get to
the top. But you can well figure up essential things at the bottom for
which it were possible and desirable to check things statically.

[Yannick Duchêne (Hibou57)]

Le Sat, 11 May 2013 02:42:37 +0200, Randy Brukardt <ra...@rrsoftware.com>
a écrit:

> I don't think operations have anything to do with types: they *use*
> types,
> they aren't part of them in any way. The "profile" of objects determines
> what operations can be used with them.

Well, “they use” or “they provides” or “they comes with”, ends to be all
the same: that's a system of interdependent things. A type may depends on
a function to create its instances, at least in the public view, as much
as sub‑programs depends on types, and there are optional and required
dependencies (if optional, better in child or other packages).

To be checked: do all formalism use functions and types at their core
basis or are there some formalisms which only uses functions and defines
types in terms of functions (I will check it a future day, I believe the
latter is the is true, while not sure).

[Yannick Duchêne (Hibou57)]

Le Sat, 11 May 2013 08:37:15 +0200, Dmitry A. Kazakov
<mai...@dmitry-kazakov.de> a écrit:

> That applies to stateful types only. Not every type is stateful. Bringing
> state into objects is considered bad practice. So bad, that it motivated
> some people to invent whole programming paradigms to avoid stateful
> object,
> e.g. functional programming. The sole idea of FP is to sweep states under
> the carpet.

FP is about expression without side effects (pure expression), not about
refusing to express states. There is no issue to have expressions
representing states and functions returning a state from a state, or even
expressions representing state transition. That's not an FP matter, but a
domain matter.

I've never seen so far, a paper about avoiding states in FP (what would be
state in FP anywhere, it not defined by the domain?). Else, out of
curiosity, I would welcome a pointer.

[Yannick Duchêne (Hibou57)]

Le Sat, 11 May 2013 08:37:15 +0200, Dmitry A. Kazakov
<mai...@dmitry-kazakov.de> a écrit:

> First of all, there are preconditions of operations and the precondition
> put on individual calls. I don't know which one you mean here. But the
> preconditions of operations must be statically true.

That's the point I don't understand or can't visualize: “preconditions of
operations must be statically true”. Out of any context? Or else, do you
suggest to move all the constraints on the types used by the operations?
(if so, that's just delegating or moving the condition elsewhere, isn't
it?).