Seeking for papers about tagged types vs access to subprograms

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

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

[Yannick Duchêne (Hibou57)]

Le Sun, 28 Apr 2013 07:14:15 +0200, Yannick Duchêne (Hibou57)  
<yannick_duchene@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.


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

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

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

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

[Yannick Duchêne (Hibou57)]

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

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

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


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

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

[Randy Brukardt]

[-- Warning: decoded text below may be mangled, UTF-8 assumed --]
[-- Attachment #1: Type: text/plain, Size: 876 bytes --]

"Yannick Duchêne (Hibou57)" <yannick_duchene@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.

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

[Randy Brukardt]

[-- Warning: decoded text below may be mangled, UTF-8 assumed --]
[-- Attachment #1: Type: text/plain, Size: 2367 bytes --]

"Yannick Duchêne (Hibou57)" <yannick_duchene@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 

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

[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

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

[Dmitry A. Kazakov]

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

> "Yannick Duch魥 (Hibou57)" <yannick_duchene@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.)

   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

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

[Randy Brukardt]

"Dmitry A. Kazakov" <mailbox@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.

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

[Dmitry A. Kazakov]

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

> "Dmitry A. Kazakov" <mailbox@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)

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

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

[Yannick Duchêne (Hibou57)]

Le Tue, 30 Apr 2013 02:31:37 +0200, Yannick Duchêne (Hibou57)  
<yannick_duchene@yahoo.fr> a écrit:

> Le Sun, 28 Apr 2013 07:14:15 +0200, Yannick Duchêne (Hibou57)  
> <yannick_duchene@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.


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

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

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

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

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

[Yannick Duchêne (Hibou57)]

Le Mon, 06 May 2013 12:18:40 +0200, Dmitry A. Kazakov  
<mailbox@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).


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

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

[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  
> <mailbox@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.

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

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

[Yannick Duchêne (Hibou57)]

Le Mon, 06 May 2013 14:11:32 +0200, Dmitry A. Kazakov  
<mailbox@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.


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

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

[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  
> <mailbox@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.

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

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

[Yannick Duchêne (Hibou57)]

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

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

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

Interfaces for all types :-D

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

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

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

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

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

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


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

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

[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  
> <mailbox@dmitry-kazakov.de> a écrit:
>>> Theoretically. In practice, GNAT don't agree (*). It has a pragma for
>>> that, `pragma Restrictions (No_Dispatching_Calls)` which should even
>>> enforce it in a whole application, but seems even with this active, it
>>> still requires the whole part of the runtime dedicated to it, a part  
>>> which depends on this part,
>>
>> I suppose it would be difficult to implement this so that the code used to
>> maintain dispatching tables and tags could be removed. It may require two
>> versions of the compiler. Furthermore there are packages defining
>> operations on tags which could require some of the stuff.
>>
>> Why do you bother? Especially, because dispatching calls are deterministic
>> and could be done time bounded, unless you manipulate tags. (Not everything
>> in people write in their guidelines for RT projects makes sense.)
> 
> That's not real‑time, that's just saving dependencies (have to be static)  
> and memory (static linking easily make it big) and to be sure to know  
> what's running beneath (no implicit heap allocation, no secondary stack,  
> bounded stack, no output to standard I/O streams except if the program do  
> it explicitly, and so on).

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.

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

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

[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

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

[Randy Brukardt]

[-- Warning: decoded text below may be mangled, UTF-8 assumed --]
[-- Attachment #1: Type: text/plain, Size: 1657 bytes --]

"Yannick Duchêne (Hibou57)" <yannick_duchene@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.

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

[Randy Brukardt]

[-- Warning: decoded text below may be mangled, UTF-8 assumed --]
[-- Attachment #1: Type: text/plain, Size: 1152 bytes --]

"Yannick Duchêne (Hibou57)" <yannick_duchene@yahoo.fr> wrote in message 
news:op.wwny5jerule2fv@cardamome...
Le Mon, 06 May 2013 14:11:32 +0200, Dmitry A. Kazakov
<mailbox@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.

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

[Yannick Duchêne (Hibou57)]

Le Tue, 07 May 2013 03:14:28 +0200, Randy Brukardt <randy@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.

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

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

[Dmitry A. Kazakov]

On Mon, 6 May 2013 13:05:25 -0700 (PDT), Adam Beneschan wrote:

> 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?  :) :) :)

(:-))

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

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

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

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

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

[Jacob Sparre Andersen news]

"Dmitry A. Kazakov" <mailbox@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.

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

[Jacob Sparre Andersen news]

"Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message 
news:19lrzzbgm77v6.1dzpgqckptaj6.dlg@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.

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

[Yannick Duchêne (Hibou57)]

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

> "Dmitry A. Kazakov" <mailbox@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.

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

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

[Yannick Duchêne (Hibou57)]

Le Tue, 07 May 2013 22:35:01 +0200, Jacob Sparre Andersen news  
<randy@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).

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

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

[Dennis Lee Bieber]

On Tue, 7 May 2013 15:35:01 -0500, "Jacob Sparre Andersen news"
<randy@rrsoftware.com> 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>)
-- 
	Wulfraed                 Dennis Lee Bieber         AF6VN
        wlfraed@ix.netcom.com    HTTP://wlfraed.home.netcom.com/

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

[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

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

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

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

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

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

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

[Dmitry A. Kazakov]

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

> "Dmitry A. Kazakov" <mailbox@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.

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

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

[Yannick Duchêne (Hibou57)]

Le Wed, 08 May 2013 09:38:03 +0200, Dmitry A. Kazakov  
<mailbox@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).


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

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

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

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

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

[Yannick Duchêne (Hibou57)]

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


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

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

[Yannick Duchêne (Hibou57)]

Le Wed, 08 May 2013 11:39:23 +0200, Yannick Duchêne (Hibou57)  
<yannick_duchene@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`).


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

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

[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.
 
-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

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

[Yannick Duchêne (Hibou57)]

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

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

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

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

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

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

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

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

[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  
> <mailbox@dmitry-kazakov.de> a écrit:
> 
>> On Wed, 08 May 2013 11:39:23 +0200, Yannick Duchêne (Hibou57) wrote:
>>
>>> But then, an example such as the above would present challenge with
>>> derived types.
>>
>> That is the main question about parallel hierarchies: if you derive or
>> constrain one type in the cloud, what happens with other types? Does this
>> produce new types, related or unrelated, constrained or not.
> 
> I would say there is no general answer without additional informations  
> about what the whole means, and no language or its compiler can tell it in  
> place of the author (or else, you decide in place of the author, and are  
> back to what it actually is).

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.

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

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

[Yannick Duchêne (Hibou57)]

Le Wed, 08 May 2013 17:29:33 +0200, Dmitry A. Kazakov  
<mailbox@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.


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

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

[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  
> <mailbox@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.

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

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

[Randy Brukardt]

"Dmitry A. Kazakov" <mailbox@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.

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

[Randy Brukardt]

"Dmitry A. Kazakov" <mailbox@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.

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

[Randy Brukardt]

"Dmitry A. Kazakov" <mailbox@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.

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

[Dmitry A. Kazakov]

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

> "Dmitry A. Kazakov" <mailbox@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.

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

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

[Dmitry A. Kazakov]

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

> "Dmitry A. Kazakov" <mailbox@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.

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

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

[Dmitry A. Kazakov]

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

> "Dmitry A. Kazakov" <mailbox@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.

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

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

[Randy Brukardt]

"Dmitry A. Kazakov" <mailbox@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.

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

[Randy Brukardt]

"Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message 
news:1bp6zlpetr5l4.12a9zcd1x3yya.dlg@40tude.net...
> On Wed, 8 May 2013 15:12:38 -0500, Randy Brukardt wrote:
>
>> "Dmitry A. Kazakov" <mailbox@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.

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.

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

[Randy Brukardt]

"Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message 
news:12gn9wvv1gwfk.10ikfju4rzmnj.dlg@40tude.net...
> On Wed, 8 May 2013 15:27:50 -0500, Randy Brukardt wrote:
>
>> "Dmitry A. Kazakov" <mailbox@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.

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

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.

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

[Yannick Duchêne (Hibou57)]

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

> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message
> news:12gn9wvv1gwfk.10ikfju4rzmnj.dlg@40tude.net...
>> On Wed, 8 May 2013 15:27:50 -0500, Randy Brukardt wrote:
>>
>>> "Dmitry A. Kazakov" <mailbox@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).


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

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

[Yannick Duchêne (Hibou57)]

Le Fri, 10 May 2013 00:19:14 +0200, Randy Brukardt <randy@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.


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

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

[Yannick Duchêne (Hibou57)]

Le Fri, 10 May 2013 00:19:14 +0200, Randy Brukardt <randy@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?

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

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

[Yannick Duchêne (Hibou57)]

Le Fri, 10 May 2013 00:19:14 +0200, Randy Brukardt <randy@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.

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

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

[Yannick Duchêne (Hibou57)]

Le Fri, 10 May 2013 05:29:53 +0200, Yannick Duchêne (Hibou57)  
<yannick_duchene@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).

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

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

[Yannick Duchêne (Hibou57)]

Le Mon, 06 May 2013 20:55:34 +0200, Dmitry A. Kazakov  
<mailbox@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).

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

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

[Yannick Duchêne (Hibou57)]

Le Mon, 06 May 2013 22:05:25 +0200, Adam Beneschan <adam@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”.

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

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

[Yannick Duchêne (Hibou57)]

Le Wed, 08 May 2013 02:18:44 +0200, Shark8 <onewingedshark@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?

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

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

[Yannick Duchêne (Hibou57)]

Le Wed, 08 May 2013 20:17:30 +0200, Dmitry A. Kazakov  
<mailbox@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.


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

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

[Yannick Duchêne (Hibou57)]

Le Thu, 09 May 2013 23:43:29 +0200, Randy Brukardt <randy@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!


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

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

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

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

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

[Dmitry A. Kazakov]

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

> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message 
> news:12gn9wvv1gwfk.10ikfju4rzmnj.dlg@40tude.net...
>> On Wed, 8 May 2013 15:27:50 -0500, Randy Brukardt wrote:
>>
>>> "Dmitry A. Kazakov" <mailbox@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.

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

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

[Dmitry A. Kazakov]

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

> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message 
> news:1bp6zlpetr5l4.12a9zcd1x3yya.dlg@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.

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

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

[Yannick Duchêne (Hibou57)]

Le Fri, 10 May 2013 09:48:26 +0200, Dmitry A. Kazakov  
<mailbox@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.

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

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

[Simon Wright]

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

> Le Wed, 08 May 2013 02:18:44 +0200, Shark8 <onewingedshark@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."

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

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

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

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

[Yannick Duchêne (Hibou57)]

Le Fri, 10 May 2013 10:42:25 +0200, Dmitry A. Kazakov  
<mailbox@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”.


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

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

[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  
> <mailbox@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.

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

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

[Yannick Duchêne (Hibou57)]

Le Fri, 10 May 2013 14:15:35 +0200, Dmitry A. Kazakov  
<mailbox@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).


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

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

[Yannick Duchêne (Hibou57)]

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

> Le Fri, 10 May 2013 14:15:35 +0200, Dmitry A. Kazakov  
> <mailbox@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).

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

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

[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  
> <mailbox@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.

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

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

[Yannick Duchêne (Hibou57)]

Le Fri, 10 May 2013 15:54:40 +0200, Dmitry A. Kazakov  
<mailbox@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?


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

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

[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  
> <mailbox@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.

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

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

[Yannick Duchêne (Hibou57)]

Le Fri, 10 May 2013 10:12:22 +0200, Yannick Duchêne (Hibou57)  
<yannick_duchene@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.


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

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

[Yannick Duchêne (Hibou57)]

Le Fri, 10 May 2013 16:27:42 +0200, Dmitry A. Kazakov  
<mailbox@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.


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

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

[Yannick Duchêne (Hibou57)]

Le Thu, 09 May 2013 09:33:54 +0200, Dmitry A. Kazakov  
<mailbox@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).


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

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

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

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

[Niklas Holsti]

On 13-05-10 07:34 , Yannick Duchêne (Hibou57) wrote:
> Le Wed, 08 May 2013 02:18:44 +0200, Shark8 <onewingedshark@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.

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

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

[Yannick Duchêne (Hibou57)]

Le Fri, 10 May 2013 20:04:42 +0200, Niklas Holsti  
<niklas.holsti@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).

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

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

[Randy Brukardt]

"Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message 
news:1jc46ynzptlxm.1fafjhr8hlblq.dlg@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.

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

[Randy Brukardt]

[-- Warning: decoded text below may be mangled, UTF-8 assumed --]
[-- Attachment #1: Type: text/plain, Size: 1673 bytes --]

"Niklas Holsti" <niklas.holsti@tidorum.invalid> wrote in message 
news:av4r5qFitfiU1@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.

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

[Randy Brukardt]

[-- Warning: decoded text below may be mangled, UTF-8 assumed --]
[-- Attachment #1: Type: text/plain, Size: 1826 bytes --]

"Yannick Duch�ne (Hibou57)" <yannick_duchene@yahoo.fr> wrote in message 
news:op.wwung605ule2fv@cardamome...
Le Fri, 10 May 2013 00:19:14 +0200, Randy Brukardt <randy@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.

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

[Randy Brukardt]

"Dmitry A. Kazakov" <mailbox@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" <mailbox@dmitry-kazakov.de> wrote in message
>> news:12gn9wvv1gwfk.10ikfju4rzmnj.dlg@40tude.net...
>>> On Wed, 8 May 2013 15:27:50 -0500, Randy Brukardt wrote:
>>>
>>>> "Dmitry A. Kazakov" <mailbox@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.

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

[Randy Brukardt]

"Dmitry A. Kazakov" <mailbox@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.

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

[Simon Wright]

"Dmitry A. Kazakov" <mailbox@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.

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

[Dmitry A. Kazakov]

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

> "Dmitry A. Kazakov" <mailbox@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" <mailbox@dmitry-kazakov.de> wrote in message
>>> news:12gn9wvv1gwfk.10ikfju4rzmnj.dlg@40tude.net...
>>>> On Wed, 8 May 2013 15:27:50 -0500, Randy Brukardt wrote:
>>>>
>>>>> "Dmitry A. Kazakov" <mailbox@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.

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

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

[Dmitry A. Kazakov]

On Fri, 10 May 2013 19:09:12 -0500, Randy Brukardt wrote:

> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message 
> news:1jc46ynzptlxm.1fafjhr8hlblq.dlg@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.

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

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

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

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

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

[Yannick Duchêne (Hibou57)]

Le Sat, 11 May 2013 03:00:39 +0200, Randy Brukardt <randy@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.

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

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

[Dmitry A. Kazakov]

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

> "Dmitry A. Kazakov" <mailbox@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?

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

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

[Yannick Duchêne (Hibou57)]

Le Sat, 11 May 2013 02:18:30 +0200, Randy Brukardt <randy@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.

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

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

[Dmitry A. Kazakov]

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

> "Dmitry A. Kazakov" <mailbox@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! 

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

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

[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
>> <mailbox@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.

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

[Yannick Duchêne (Hibou57)]

Le Sat, 11 May 2013 02:22:58 +0200, Randy Brukardt <randy@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.



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

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

[Yannick Duchêne (Hibou57)]

Le Sat, 11 May 2013 02:42:37 +0200, Randy Brukardt <randy@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.

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

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

[Dmitry A. Kazakov]

On Sat, 11 May 2013 09:06:11 +0200, Georg Bauhaus wrote:

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

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

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

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

[Yannick Duchêne (Hibou57)]

Le Sat, 11 May 2013 02:42:37 +0200, Randy Brukardt <randy@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).

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

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

[Yannick Duchêne (Hibou57)]

Le Sat, 11 May 2013 08:37:15 +0200, Dmitry A. Kazakov  
<mailbox@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.

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

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

[Yannick Duchêne (Hibou57)]

Le Sat, 11 May 2013 08:37:15 +0200, Dmitry A. Kazakov  
<mailbox@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?).

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

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

[Yannick Duchêne (Hibou57)]

Le Sat, 11 May 2013 09:42:14 +0200, Dmitry A. Kazakov  
<mailbox@dmitry-kazakov.de> a écrit:

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

All sounds wise to me, agree.


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

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

[Dmitry A. Kazakov]

On Sat, 11 May 2013 09:58:38 +0200, Yannick Duch�ne (Hibou57) wrote:

> Le Sat, 11 May 2013 08:37:15 +0200, Dmitry A. Kazakov  
> <mailbox@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.

Side effect here = object[s] state.

[You certainly cannot attribute it to the control flow state as you return
to the definite point after expression is computed.]

> There is no issue to have expressions  
> representing states and functions returning a state from a state,

You return values not states. State of the object is the value it presently
represents. State of flow is the source code location.

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

FP-guys usually refuse to mention objects for evident reasons.

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

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

[Dmitry A. Kazakov]

On Sat, 11 May 2013 10:03:13 +0200, Yannick Duchêne (Hibou57) wrote:

> Le Sat, 11 May 2013 08:37:15 +0200, Dmitry A. Kazakov  
> <mailbox@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?

Yep. The reason for that is that the designed of an operation cannot
control or even foresee the contexts where the operation will be used. It
is neither his responsibility nor his concern.

> Or else, do you  
> suggest to move all the constraints on the types used by the operations?

I suggest that properly designed types should have no constraints of this
kind.
  
> (if so, that's just delegating or moving the condition elsewhere, isn't  
> it?).

The condition is moved to the post-condition. E.g.

# require X >= 0.0
   function sqrt (X : Float) return Float;
# ensure sqrt (X)**2 = X

is replaced with

# require true
   function sqrt (X : Float) return Float;
# ensure sqrt (X)**2 = X or else Constraint_Error raised

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

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

[Georg Bauhaus]

"Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote:

> The condition is moved to the post-condition. E.g.
> 
> # require X >= 0.0
>    function sqrt (X : Float) return Float;
> # ensure sqrt (X)**2 = X
> 
> is replaced with
> 
> # require true
>    function sqrt (X : Float) return Float;
> # ensure sqrt (X)**2 = X or else Constraint_Error raised

So sqrt tests X for being non-negative and raises C_E otherwise?
Can the test be turned off?

# require true
  procedure increase_pressure (P : in out Pot; X : Float);
# ensure pressure (P) = X * pressure (P'old) or else Kaboom raised

So where goes the precondition of the second kind mentioned
earlier, for calls, the one that is needed for correctness of the program?
I take it that the former kind of precondition prevents Kaboom in the
system?

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

[Dmitry A. Kazakov]

On 11 May 2013 11:49:12 GMT, Georg Bauhaus wrote:

> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote:
> 
>> The condition is moved to the post-condition. E.g.
>> 
>> # require X >= 0.0
>>    function sqrt (X : Float) return Float;
>> # ensure sqrt (X)**2 = X
>> 
>> is replaced with
>> 
>> # require true
>>    function sqrt (X : Float) return Float;
>> # ensure sqrt (X)**2 = X or else Constraint_Error raised
> 
> So sqrt tests X for being non-negative and raises C_E otherwise?
> Can the test be turned off?

It is not test, it is a behavior. However if sqrt were inlined, at least
partially, one branch of "if" could be removed if its condition proved
static.

> # require true
>   procedure increase_pressure (P : in out Pot; X : Float);
> # ensure pressure (P) = X * pressure (P'old) or else Kaboom raised
> 
> So where goes the precondition of the second kind mentioned
> earlier, for calls, the one that is needed for correctness of the program?

Is it a physical system you are talking about? In that case it does not
work this way. You have a hardware in the [control] loop (HIL). E.g. a
valve, a boiler, whatever. You set the valve using an actuator, you control
its position using position sensors, you control pressure using pressure
sensors, you control things using indirect measures, e.g. of the
temperature etc. There is a model of the system according to which you act
and react. It is very different from digital deterministic systems where
cause and effect are tied to the point of being equivalent.

> I take it that the former kind of precondition prevents Kaboom in the
> system?

By not raising it. So long the model is adequate [as estimated though the
sensors] you don't raise anything. When the model is no more adequate you
drive the system into a definite state as specified by the requirements,
e.g. by doing an emergency shutdown. This procedure may be implemented
using exceptions. In some cases definite state is achieved by self
destruction (see Ariane).

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

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

[Niklas Holsti]

On 13-05-11 10:58 , Yannick Duchêne (Hibou57) wrote:
> Le Sat, 11 May 2013 08:37:15 +0200, Dmitry A. Kazakov
> <mailbox@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.

Monads? http://en.wikipedia.org/wiki/Monad_%28functional_programming%29

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

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

[Niklas Holsti]

On 13-05-11 03:18 , Randy Brukardt wrote:
> "Niklas Holsti" <niklas.holsti@tidorum.invalid> wrote in message 
> news:av4r5qFitfiU1@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'm not sure if "typestate" matches all of what you were describing or
thinking of -- I meant it only as a pointer to Yannick for things like
the Open-Close protocol example. But if it resonates with your thinking,
good.

> 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 haven't studied typestate analysis at all deeply. I had a look at the
"Plaid" language referenced from the Wikipedia article, at
http://www.cs.cmu.edu/~aldrich/plaid/, and was a bit surprised to
understand that Ada subtypes come rather close to it, in particular
subtypes of discriminated record types with variants. The value of the
discriminant represents the state, with certain components of the record
(= attributes of the object or type) existing or not existing depending
on the variant selected by the discriminant.

For the Open-Close example:

   type File_State is (Is_Closed, Is_Open);

   type File_Object (State : File_State := Is_Closed) is
   record
      case State is
      when Is_Closed => null;
      when Is_Open   => Handle : System.IO.File_Handle;
      end case;
   end record;

   subtype Closed_File is File_Object (State => Is_Closed);
   subtype Open_File   is File_Object (State => Is_Open  );

By using subtypes on formal parameters, we can indicate that the
available operations on a File_Object depend on the actual subtype
(i.e. the state), except for one deficiency, on which more below.

First, reading and writing is possible only for open files:

   procedure Read  (File : in Open_File; ...)
   procedure Write (File : in Open_File; ...)

Second, a Closed file can be Opened, and an Open file can be Closed:

   procedure Open  (File : in out Closed_File);
   procedure Close (File : in out Open_File  );

The problem here is that these operations should change the subtype of
the "in out" parameter: Open changes the File from Closed_File to
Open_File, and Close changes it from Open_File to Closed_File. However,
Ada does not let us specify such changes, in the subprogram profile.
(This can of course be specified with pre- and post-conditions, but I'm
looking for a closer connection between the subprogram profile and the
subtypes.)

Well, why is Ada limited in this way? There is no real reason why an "in
out" parameter should have the same constraints on input and on output.
So let us extend Ada to allow different "in" and "out" subtypes:

   -- Extended Ada:
   procedure Open  (File : in Closed_File out Open_File  ; ...);
   procedure Close (File : in Open_File   out Closed_File; ...);

This gives us exactly the open/close typestate example. A compiler with
strong value-range analysis should then be able to deduce, for example,
that the "in" constraint check on a particular call of Open, Close,
Read, or Write always succeeds (= typestate correctness) or may or must
fail (various degrees of typestate incorrectness). I believe that many
current compilers could do such value-range analysis, and thus Ada could
support this kind of typestate concept with rather small language changes.

(You may ask: if an "in out" parameter has different "in" and "out"
subtypes, what subtype is applied when the formal parameter is used or
assigned within the subprogram body? I think the logical answer would be
the "disjunctive subtype" that represents the union of the "in" and
"out" subtypes, which unfortunately could be a subtype with "holes". But
I think that would be manageable, since this disjunctive subtype would
have at most two separate components, i.e. at most one hole.)

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

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

[Robert A Duff]

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

> The condition is moved to the post-condition. E.g.
>
> # require X >= 0.0
>    function sqrt (X : Float) return Float;
> # ensure sqrt (X)**2 = X
>
> is replaced with
>
> # require true
>    function sqrt (X : Float) return Float;
> # ensure sqrt (X)**2 = X or else Constraint_Error raised

It seems to me that this replacement loses information (the info that 
X is "supposed to be nonnegative").

For example, a body of sqrt that says "return X / 0.0;" obeys the second
contract but not the first above.  But that's obviously wrong to anyone
who thinks that "sqrt" means "approximate square root of X".

(Never mind the accuracy issues -- sqrt(X) might not be representable as
a Float. ;-) )

- Bob

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

[Shark8]

On Saturday, May 11, 2013 3:06:25 PM UTC-6, Niklas Holsti wrote:
>
> Well, why is Ada limited in this way? There is no real reason why an "in
> out" parameter should have the same constraints on input and on output. 

What? Ada's not constrained like that, at least as you're implying:

Given the types you have:
> 
>    type File_State is (Is_Closed, Is_Open);
> 
>    type File_Object (State : File_State := Is_Closed) is
>    record
>       case State is
>       when Is_Closed => null;
>       when Is_Open   => Handle : System.IO.File_Handle;
>       end case;
>    end record;
> 
>    subtype Closed_File is File_Object (State => Is_Closed);
>    subtype Open_File   is File_Object (State => Is_Open  ); 

the proper way to formulate _EXACTLY_ what you want is this:

procedure Read  (File : in out File_Object; ...)
  with pre => File in Closed_File, post => file in Open_File;

Or am I wrong?

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

[Dmitry A. Kazakov]

On Sat, 11 May 2013 18:51:27 -0400, Robert A Duff wrote:

> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> writes:
> 
>> The condition is moved to the post-condition. E.g.
>>
>> # require X >= 0.0
>>    function sqrt (X : Float) return Float;
>> # ensure sqrt (X)**2 = X
>>
>> is replaced with
>>
>> # require true
>>    function sqrt (X : Float) return Float;
>> # ensure sqrt (X)**2 = X or else Constraint_Error raised
> 
> It seems to me that this replacement loses information (the info that 
> X is "supposed to be nonnegative").

# ensure
    (X >= 0.0 and then sqrt (X)**2 = X)
or else
    (X < 0.0 and then Constraint_Error raised)

> For example, a body of sqrt that says "return X / 0.0;" obeys the second
> contract but not the first above.  But that's obviously wrong to anyone
> who thinks that "sqrt" means "approximate square root of X".

As "approximate square root" any implementation is OK. A more realistic
contract that defines accuracy of the result could be like:

   sqrt (X)**2 in Float'Max (0.0, X'Pred)..Float'Min (Float'Last, X'Succ)

[It was just an illustration of the idea how preconditions of operations
are relaxed.]
 
> (Never mind the accuracy issues -- sqrt(X) might not be representable as
> a Float. ;-) )

No, because sqrt(X) < X, if X > 0.

But considering mathematical sqrt, yes, it is not even complex-valued. sqrt
is a multi-valued complex function. If we are lucky one value of sqrt(X)
might have zero imaginary part.

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

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

[Niklas Holsti]

On 13-05-12 02:19 , Shark8 wrote:
> On Saturday, May 11, 2013 3:06:25 PM UTC-6, Niklas Holsti wrote:
>>
>> Well, why is Ada limited in this way? There is no real reason why an "in
>> out" parameter should have the same constraints on input and on output. 
> 
> What? Ada's not constrained like that, at least as you're implying:

When you declare an "in out" parameter, Ada now requires that you
specify the same subtype for both roles. In the example, if the File
parameter to Open is declared as "in out Closed_File", but Open tries to
change the parameter to (State => Is_Open, Handle => ...) a
Constraint_Error results at run-time.

> Given the types you have:
>>
>>    type File_State is (Is_Closed, Is_Open);
>>
>>    type File_Object (State : File_State := Is_Closed) is
>>    record
>>       case State is
>>       when Is_Closed => null;
>>       when Is_Open   => Handle : System.IO.File_Handle;
>>       end case;
>>    end record;
>>
>>    subtype Closed_File is File_Object (State => Is_Closed);
>>    subtype Open_File   is File_Object (State => Is_Open  ); 
> 
> the proper way to formulate _EXACTLY_ what you want is this:
> 
> procedure Read  (File : in out File_Object; ...)
>   with pre => File in Closed_File, post => file in Open_File;

(I think you mean "procedure Open" there, not "Read".)

As I said, it can be expressed with pre- and post-conditions in this
way, but then the parameter profile does not mention the subtypes and
instead uses the unconstrained type (here File_Object). As I also said,
I wanted the subtype changes to be visible in the subprogram profile, to
show more clearly (or at least, more traditionally) how the availability
of the subprogram depends on the state (i.e. the subtype) of the
parameter, and how it affects the state.

To condense my points:

1. The typestate concept, as implemented in the Plaid language, seems
(after my brief study of Plaid) to be implementable in Ada through
discriminated records with variants.

2. The influence of the current typestate of an object, on the set of
subprograms (operations) available for the object, can be represented as
constraints on the "in" subtype of the object, and the typestate changes
can be represented as the "out" subtype. In current Ada, of course, the
subtype checks in principle occur at run-time, so typestate correctness
is not checked at compile-time. Moreover, current Ada does not allow the
formal subtype (as written in the profile) to be different for the "in"
and "out" roles.

3. Those different "in" and "out" constraints can be implemented in Ada
2012 as pre/post-conditions, as you say.

4. A closer match to Plaid can be achieved if Ada is extended to allow
different subtypes for the "in" and "out" roles of an "in out" parameter.

As the pre/post-condition feature of Ada 2012 becomes more familiar,
perhaps the pre- and post-conditions will be seen as a more integrated
part of the subprogram's profile, and there is no reason to consider
changes to the formal subtypes allowed in the language (point 4).

On the other hand, it seems to me that there are other cases, not
perhaps related to typestate, where it would be natural to specify
different "in" and "out" subtypes for an "in out" parameter. Something
as simple as:

   procedure Increment (Counter : in out Natural)

could become

   -- Extended Ada:
   procedure Increment (
      Counter : in  Natural range 0 .. Natural'Last - 1
                out Positive);

Of course, all such different in/out constraints can be expressed using
the "heavy guns" of pre/post-conditions, so perhaps this suggestion is
out of date after Ada 2012. Any compiler powerful enough to do useful
typestate analysis based on the formal parameter subtypes is probably
able to do the same analysis using the corresponding
pre/post-conditions, at least when the conditions take the simple form
"parameter in subtype".

It is interesting that Randy thinks his ideas regarding a future
replacement for Ada resemble the typestate concept, but that the
typestate concept as implemented in Plaid seems to be implementable in
Ada 2012. Perhaps Randy's ideas go much further than this, however.

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

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

[Yannick Duchêne (Hibou57)]

Le Sun, 12 May 2013 08:02:16 +0200, Dmitry A. Kazakov  
<mailbox@dmitry-kazakov.de> a écrit:
>>> The condition is moved to the post-condition. E.g.
>>>
>>> # require X >= 0.0
>>>    function sqrt (X : Float) return Float;
>>> # ensure sqrt (X)**2 = X
>>>
>>> is replaced with
>>>
>>> # require true
>>>    function sqrt (X : Float) return Float;
>>> # ensure sqrt (X)**2 = X or else Constraint_Error raised
>>
>> It seems to me that this replacement loses information (the info that
>> X is "supposed to be nonnegative").
>
> # ensure
>     (X >= 0.0 and then sqrt (X)**2 = X)
> or else
>     (X < 0.0 and then Constraint_Error raised)

But what's the benefit of moving the precondition to the postcondition? Or  
more simply, why dropping the idea of precondition for sub‑program  
declarations?

Do you have to re‑invent or re‑derive the precondition at each call place,  
 from the postcondition? Isn't it kind of bloat?

It makes more me feel like losing something than the opposite. And how do  
you clearly connect valid invocations into sequence? You can't connect any  
more, the post condition of A to precondition of B (when B comes next to  
A), or else, less clearly. There may be an issue with separation of  
concern here (the God postcondition?). I won't enjoy a variant of Ada  
doing so.

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

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

[Yannick Duchêne (Hibou57)]

Le Sat, 11 May 2013 23:06:25 +0200, Niklas Holsti  
<niklas.holsti@tidorum.invalid> a écrit:

>    type File_State is (Is_Closed, Is_Open);
>
>    type File_Object (State : File_State := Is_Closed) is
>    record
>       case State is
>       when Is_Closed => null;
>       when Is_Open   => Handle : System.IO.File_Handle;
>       end case;
>    end record;
>
>    subtype Closed_File is File_Object (State => Is_Closed);
>    subtype Open_File   is File_Object (State => Is_Open  );
>
> By using subtypes on formal parameters, we can indicate that the
> available operations on a File_Object depend on the actual subtype
> (i.e. the state), except for one deficiency, on which more below.
>
> First, reading and writing is possible only for open files:
>
>    procedure Read  (File : in Open_File; ...)
>    procedure Write (File : in Open_File; ...)
>
> Second, a Closed file can be Opened, and an Open file can be Closed:
>
>    procedure Open  (File : in out Closed_File);
>    procedure Close (File : in out Open_File  );
>
> The problem here is that these operations should change the subtype of
> the "in out" parameter: Open changes the File from Closed_File to
> Open_File, and Close changes it from Open_File to Closed_File.

Additionally to the idea you suggested, that may also suggest to use a  
function instead of a procedure with in/out parameter, with a new  
declaration for each of the important state changes which would become  
clearly visible (still what if this already was a function already  
returning something… Ada functions can return only one single element).  
There is now the question about compilers: are compilers clever enough to  
statically catch subtype miss‑match in such a use cases and give warnings  
(I believe no), and are compilers clever enough to optimize out multiple  
object declaration into a single one, changing its subtype (I believe no,  
too), while the latter is not an issue if you use a default discriminant  
as you did.

Another issue with subtype, is that it requires the `File_Object` full  
definition to be public, or else, there is no way to define a subtype of  
it as the example do (no opaque type).

The idea is still nice and worth to investigate.


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

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

[Dmitry A. Kazakov]

On Sun, 12 May 2013 08:25:33 +0200, Yannick Duchêne (Hibou57) wrote:

> Le Sun, 12 May 2013 08:02:16 +0200, Dmitry A. Kazakov  
> <mailbox@dmitry-kazakov.de> a écrit:
>>>> The condition is moved to the post-condition. E.g.
>>>>
>>>> # require X >= 0.0
>>>>    function sqrt (X : Float) return Float;
>>>> # ensure sqrt (X)**2 = X
>>>>
>>>> is replaced with
>>>>
>>>> # require true
>>>>    function sqrt (X : Float) return Float;
>>>> # ensure sqrt (X)**2 = X or else Constraint_Error raised
>>>
>>> It seems to me that this replacement loses information (the info that
>>> X is "supposed to be nonnegative").
>>
>> # ensure
>>     (X >= 0.0 and then sqrt (X)**2 = X)
>> or else
>>     (X < 0.0 and then Constraint_Error raised)
> 
> But what's the benefit of moving the precondition to the postcondition? Or  
> more simply, why dropping the idea of precondition for sub‑program  
> declarations?

In short, because it is inconsistent with the notion of type. Other issues
are merely consequences.

> Do you have to re‑invent or re‑derive the precondition at each call place,  
> from the postcondition?

Conditions at call place are of second kind. They could be any or none.

> It makes more me feel like losing something than the opposite. And how do  
> you clearly connect valid invocations into sequence?

See above, it is 1st and 2nd kind conditions. You are conflating the
semantics of a type with the semantics of *a* program that uses this type
somewhere, somehow.

To put it simply: if a type is designed in a way that limits it use, it is
a poor design.

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

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

[Simon Wright]

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

> To put it simply: if a type is designed in a way that limits it use,
> it is a poor design.

I think that depends on who is paying for all the extra work you would
be putting in.

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

[Dmitry A. Kazakov]

On Sun, 12 May 2013 08:37:11 +0100, Simon Wright wrote:

> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> writes:
> 
>> To put it simply: if a type is designed in a way that limits it use,
>> it is a poor design.
> 
> I think that depends on who is paying for all the extra work you would
> be putting in.

Not much. If you can formalize the constraint to the level which would
allow its specification as a precondition, then you also can as easily
remove it from there.

On the other hand, considering all sorts of write once run once designs, it
would be quite strange to expect that people doing that would pay any
attention to writing preconditions.

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

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

[Niklas Holsti]

On 13-05-12 09:44 , Yannick Duchêne (Hibou57) wrote:
> Le Sat, 11 May 2013 23:06:25 +0200, Niklas Holsti
> <niklas.holsti@tidorum.invalid> a écrit:
> 
>>    type File_State is (Is_Closed, Is_Open);
>>
>>    type File_Object (State : File_State := Is_Closed) is
>>    record
>>       case State is
>>       when Is_Closed => null;
>>       when Is_Open   => Handle : System.IO.File_Handle;
>>       end case;
>>    end record;
>>
>>    subtype Closed_File is File_Object (State => Is_Closed);
>>    subtype Open_File   is File_Object (State => Is_Open  );
>>
>> By using subtypes on formal parameters, we can indicate that the
>> available operations on a File_Object depend on the actual subtype
>> (i.e. the state), except for one deficiency, on which more below.
>>
>> First, reading and writing is possible only for open files:
>>
>>    procedure Read  (File : in Open_File; ...)
>>    procedure Write (File : in Open_File; ...)
>>
>> Second, a Closed file can be Opened, and an Open file can be Closed:
>>
>>    procedure Open  (File : in out Closed_File);
>>    procedure Close (File : in out Open_File  );
>>
>> The problem here is that these operations should change the subtype of
>> the "in out" parameter: Open changes the File from Closed_File to
>> Open_File, and Close changes it from Open_File to Closed_File.
> 
> Additionally to the idea you suggested, that may also suggest to use a
> function instead of a procedure with in/out parameter, with a new
> declaration for each of the important state changes which would become
> clearly visible (still what if this already was a function already
> returning something… Ada functions can return only one single element).

You mean like this:

   function Open  (File : in Closed_File) return Open_File;
   function Close (File : in Open_File  ) return Closed_File;

I agree that this is a possible approach. This would work, but at the
cost of writing the parameter/object name twice in each call:

   File : File_Object;
   ...
   File := Open (File);
   File := Close (File);

But this code seems to cause a problem:

   File1, File2 : File_Object;
   ...
   File1 := Open (File1);
   File2 := Close (File1);

Now File2 is a clone of File1, and the underlying system file is closed,
but File1 still considers it open. (This may of course be acceptable to
the specific underlying system and not lead to an error, but in general
I believe that such side-effects could be problematic.)

The "function" approach thus tends to clone objects, and to lose the
"object identity".

If we want to preserve object identity under that approach, I think we
need a "linear type system"
(http://en.wikipedia.org/wiki/Linear_type_system) in which each variable
can be used exactly once. However, every use (e.g. as a parameter to a
function) can produce a new incarnation of the object (the function
return value), which can be assigned to a new variable, so the object
lives on. However, this would be a BIG change to the language.

> There is now the question about compilers: are compilers clever enough
> to statically catch subtype miss‑match in such a use cases and give
> warnings (I believe no),

I think that if this issue of subtype matching comes to be considered
important, compiler writers could give it more attention, and
conservative (but incomplete) static-analysis solutions could be
implemented with current technology.

> and are compilers clever enough to optimize out
> multiple object declaration into a single one, changing its subtype (I
> believe no, too),

Those problems are solved by a linear type system. But I agree with you
that it is too much to expect that the compiler would automatically
implement an Ada-like program using linear typing behind the scenes.

> Another issue with subtype, is that it requires the `File_Object` full
> definition to be public, or else, there is no way to define a subtype of
> it as the example do (no opaque type).

Yes, that could be a problem. The language might allow the declaration
of subtypes of opaque types, with opaque constraints. That does not seem
too hard to implement if the type and subtypes are fully defined in the
private part of a package, but it seems more difficult if the full type
declaration is deferred (through an access type) to the package body.

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

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

[Yannick Duchêne (Hibou57)]

Le Sun, 12 May 2013 09:14:41 +0200, Dmitry A. Kazakov  
<mailbox@dmitry-kazakov.de> a écrit:

> To put it simply: if a type is designed in a way that limits it use, it  
> is
> a poor design.

The sense or meaning, both in natural and formal languages, comes from  
restricting possible interpretations.

> You are conflating the
> semantics of a type with the semantics of *a* program that uses this type
> somewhere, somehow.

Precisely, I see types as constituents of a domain, so also as  
constituents of applications of the domain. I'm guessing I'm not the only  
one.

We may diverge here, in short I would say: I don't want bricks giving the  
illusions I may always be able to use it to build something which may or  
may not fails, I want bricks which will tell the sooner I will not be able  
to use it in some invalid ways if I want something which will not fail (or  
at least reduce potentials for failures, as program proof is more than  
that).

What I don't understand is: how something which give the illusion it has  
no prerequisites, can help in constructing safer and more trustable  
architectures? Reusing is nice, however only where it, and in a way which,  
make sense for the domain (I don't believe an exception is meaningful,  
that's not a value, that's a runtime error). Seems the invariably `True`  
precondition wants to give the illusion of universal reuse without  
conditions. With all precondition moved to the postcondition, the program  
has more potential for erroneous interpretation, because that may turns  
into a lot more decision paths in the program after each invocation.

I will not argue that much on this issue, as that may involves personal  
feeling.


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

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

[Yannick Duchêne (Hibou57)]

Le Sun, 12 May 2013 10:10:01 +0200, Niklas Holsti  
<niklas.holsti@tidorum.invalid> a écrit:
> You mean like this:
>
>    function Open  (File : in Closed_File) return Open_File;
>    function Close (File : in Open_File  ) return Closed_File;
>
> I agree that this is a possible approach. This would work, but at the
> cost of writing the parameter/object name twice in each call:

Yes, that was that. I don't bother about writing more when it that makes  
things more readable.

>    File : File_Object;
>    ...
>    File := Open (File);
>    File := Close (File);
>
> But this code seems to cause a problem:
>
>    File1, File2 : File_Object;
>    ...
>    File1 := Open (File1);
>    File2 := Close (File1);
>
> Now File2 is a clone of File1, and the underlying system file is closed,
> but File1 still considers it open.

Interesting point. Note the the procedural way present the same issue, as  
the object may be copied too, even if limited, using component by  
component copy (as with actual Ada, the type cannot be private for the  
reason given before). Less likely to occurs, but if it can occurs, it's  
enough to say the issue is still there.

>
> The "function" approach thus tends to clone objects, and to lose the
> "object identity".

The topic of object identity is interesting, I have not though about it.  
That's finally an issue similar to aliasing here… as the file type is  
finally a kind of reference, via its handle.

> If we want to preserve object identity under that approach, I think we
> need a "linear type system"
> (http://en.wikipedia.org/wiki/Linear_type_system)

Your nickname must Santa Clause :) Thanks for the new pointer, again.


> Yes, that could be a problem. The language might allow the declaration
> of subtypes of opaque types, with opaque constraints.

But the subtype would not have readable sense if the constraints would be  
opaque. Or else as an alternative, may be Ada could allow partly unknown  
discriminant (something I miss):


     -- Valid actual Ada:

     type T1 (<>) is private;


     -- Invalid, actual Ada don't permits this:

     type T2 (Foo: Foo_Type; <>) is private;


As an unrelated side note, something I miss too with private types, is the  
ability for the completion to be a subtype (actual Ada requires it to be a  
type‑new or a record).


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

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

[Dmitry A. Kazakov]

On Sun, 12 May 2013 10:21:49 +0200, Yannick Duchêne (Hibou57) wrote:

> We may diverge here, in short I would say: I don't want bricks giving the  
> illusions I may always be able to use it to build something which may or  
> may not fails, I want bricks which will tell the sooner I will not be able  
> to use it in some invalid ways if I want something which will not fail (or  
> at least reduce potentials for failures, as program proof is more than  
> that).

It is impossible to achieve. It also contradicts the basic principle of
design: divide and conquer. You want bricks to learn architecture? Even if
that were possible such bricks would be unaffordable. And how would you
validate, test, certify such bricks?

> What I don't understand is: how something which give the illusion it has  
> no prerequisites, can help in constructing safer and more trustable  
> architectures?

Simplicity, abstraction, Occam's razor, the principle of minimum energy,
basic customs of engineering etc.

> Seems the invariably `True`  
> precondition wants to give the illusion of universal reuse without  
> conditions.

No, "true" means what that the contract was not a lie. If you say that the
argument of sqrt is Float and another person say that it is not negative,
then somebody is lying here.

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

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

[Yannick Duchêne (Hibou57)]

Le Sun, 12 May 2013 11:25:51 +0200, Dmitry A. Kazakov  
<mailbox@dmitry-kazakov.de> a écrit:

>> Seems the invariably `True`
>> precondition wants to give the illusion of universal reuse without
>> conditions.
>
> No, "true" means what that the contract was not a lie. If you say that  
> the
> argument of sqrt is Float and another person say that it is not negative,
> then somebody is lying here.

This is the same person who says both as this is the one who wrote the  
signature and the precondition. And this is not a contradiction to have  
conjunction of conditions, that's common.


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

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

[Dmitry A. Kazakov]

On Sun, 12 May 2013 11:32:13 +0200, Yannick Duchêne (Hibou57) wrote:

> Le Sun, 12 May 2013 11:25:51 +0200, Dmitry A. Kazakov  
> <mailbox@dmitry-kazakov.de> a écrit:
> 
>>> Seems the invariably `True`
>>> precondition wants to give the illusion of universal reuse without
>>> conditions.
>>
>> No, "true" means what that the contract was not a lie. If you say that  the
>> argument of sqrt is Float and another person say that it is not negative,
>> then somebody is lying here.
> 
> This is the same person who says both as this is the one who wrote the  
> signature and the precondition. And this is not a contradiction to have  
> conjunction of conditions, that's common.

Except that it is not a conjunction. If it were a conjunction then either
specified as proper type or else, if there were no types, as solely a
dynamic precondition. That is the choice between being untyped or strong
types. Your case is neither. Furthermore it cannot be made the second in
realistic cases because such constraints cannot be statically enforced. So
if you want it a conjunction it must be the first:

# pre X in Float and then X >= 0.0
   function sqrt (X : Any) return Float;

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

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

[Jeffrey Carter]

On 05/12/2013 01:10 AM, Niklas Holsti wrote:
>
> You mean like this:
>
>     function Open  (File : in Closed_File) return Open_File;
>     function Close (File : in Open_File  ) return Closed_File;
>
> I agree that this is a possible approach. This would work, but at the
> cost of writing the parameter/object name twice in each call:
>
>     File : File_Object;
>     ...
>     File := Open (File);
>     File := Close (File);

I'm not sure I see the point in having an object for a closed file, other than 
the requirements of low-level languages in which such things were 1st 
implemented. Why not something like

type File_Info (<>) is tagged limited private;

function Open   (Name : ...; ...) return File_Info;
function Create (Name : ...; ...) return File_Info;

function Read   (File : in out File_Info) return ...;
procedure Write (File : in out File_Info; Item : in ...);

declare
    File : File_Info := Open ("junk", ...);
begin
    Data := Read (File);
    ...
end;

A File_Info must be opened or created when declared, and is closed when it's 
finalized.

-- 
Jeff Carter
"C++ is like giving an AK-47 to a monk, shooting him
full of crack and letting him loose in a mall and
expecting him to balance your checking account
'when he has the time.'"
Drew Olbrich
52

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

[Robert A Duff]

Jeffrey Carter <spam.jrcarter.not@spam.not.acm.org> writes:

> I'm not sure I see the point in having an object for a closed file,

Yeah, I was about to post basically the same thing.  A closed file
is pretty useless.  It's like an uninitialized variable -- you can't
do anything with it.

> other than the requirements of low-level languages in which such things
> were 1st implemented.

Low-level languages like Ada 83?  ;-)

>...Why not something like
>
> type File_Info (<>) is tagged limited private;

Yes, but I would have separate types for Input_File and Output_File.
Possibly another type for the rare case when you want to
read and write to/from the same file handle.

> function Open   (Name : ...; ...) return File_Info;
> function Create (Name : ...; ...) return File_Info;

Note that these are build-in-place functions.  You can't call them
as the right-hand side of an assignment statement.

> function Read   (File : in out File_Info) return ...;
> procedure Write (File : in out File_Info; Item : in ...);
>
> declare
>    File : File_Info := Open ("junk", ...);
> begin
>    Data := Read (File);
>    ...
> end;

You could use it as above, or like this:

    Grind_Upon_File(Open("junk", ...));

Or like this:

    X := new File_Info'(Open(...));

But you couldn't use it like this:

    File : File_Info; -- Illegal!
    ... -- some code that computes File_Name
    File := Open (File_Name); -- Illegal!

which is a limitation, compared to the current design of Text_IO
and friends.

> A File_Info must be opened or created when declared, and is closed when
> it's finalized.

Right.

- Bob

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

[Jeffrey Carter]

On 05/12/2013 03:15 PM, Robert A Duff wrote:
> Jeffrey Carter <spam.jrcarter.not@spam.not.acm.org> writes:
>
>> I'm not sure I see the point in having an object for a closed file,
>
> Yeah, I was about to post basically the same thing.  A closed file
> is pretty useless.  It's like an uninitialized variable -- you can't
> do anything with it.
>
>> other than the requirements of low-level languages in which such things
>> were 1st implemented.
>
> Low-level languages like Ada 83?  ;-)

Or even Ada 80 :) But I suspect everything goes back to how files were handled 
in 1950's assembly languages.

> Yes, but I would have separate types for Input_File and Output_File.
> Possibly another type for the rare case when you want to
> read and write to/from the same file handle.

Yes, that's an additional possible refinement.

> But you couldn't use it like this:
>
>      File : File_Info; -- Illegal!
>      ... -- some code that computes File_Name
>      File := Open (File_Name); -- Illegal!
>
> which is a limitation, compared to the current design of Text_IO
> and friends.

That's what block statements are for.

-- 
Jeff Carter
"I fart in your general direction."
Monty Python & the Holy Grail
05

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

[Niklas Holsti]

On 13-05-12 21:56 , Jeffrey Carter wrote:
> On 05/12/2013 01:10 AM, Niklas Holsti wrote:
>>
>> You mean like this:
>>
>>     function Open  (File : in Closed_File) return Open_File;
>>     function Close (File : in Open_File  ) return Closed_File;
>>
>> I agree that this is a possible approach. This would work, but at the
>> cost of writing the parameter/object name twice in each call:
>>
>>     File : File_Object;
>>     ...
>>     File := Open (File);
>>     File := Close (File);
> 
> I'm not sure I see the point in having an object for a closed file,
> other than the requirements of low-level languages in which such things
> were 1st implemented.

This "file" stuff is only an example of a protocol that can be subjected
to typestate analysis. For "closed file", substitute "an object that is
in its initial state".

> Why not something like
> 
> type File_Info (<>) is tagged limited private;
> 
> function Open   (Name : ...; ...) return File_Info;
> function Create (Name : ...; ...) return File_Info;
> 
> function Read   (File : in out File_Info) return ...;
> procedure Write (File : in out File_Info; Item : in ...);
> 
> declare
>    File : File_Info := Open ("junk", ...);
> begin
>    Data := Read (File);
>    ...
> end;
> 
> A File_Info must be opened or created when declared, and is closed when
> it's finalized.

The point of the example was to illustrate typestate analysis. For this
example, with only Open - (Read/Write)* - Close, your approach collapses
the example into a trivial one, where adherence to the operation
protocol is ensured by the necessity to declare a File_Info object
before it can be used. So it would no longer be a useful example.

Your approach works in some cases, but it is problematic if you cannot
initialize the object to an "active" state in its declaration, for
example because the "activation" is conditional in some way, or must be
delayed. The "activation" must then be done in a statement, and the
declaration leaves the object in some inactive initial state.

Another limitation in your approach is that the opening and closing of
different files must be strictly nested: if you declare and open file A,
then declare and open file B, file B must be closed before file A is
closed (as long as it all happens in the same task). Such forced
constraints between the states of different object is often not wanted.

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

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

[Yannick Duchêne (Hibou57)]

Le Mon, 13 May 2013 00:15:24 +0200, Robert A Duff  
<bobduff@shell01.theworld.com> a écrit:

> Jeffrey Carter <spam.jrcarter.not@spam.not.acm.org> writes:
>
>> I'm not sure I see the point in having an object for a closed file,
>
> Yeah, I was about to post basically the same thing.  A closed file
> is pretty useless.

As said Niklas, the initial idea was requirements on the state of objects  
for some operation to occur or not occur.

Just on the object for a closed file, this make sense if the object does  
not really disappear when it is closed. If the object still exist in scope  
or via kind of references, it needs to have a `Closed` state. That would  
not be the same if the file would be automatically closed when going out  
of scope and always be opened when appearing in the scope.

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

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

[Dmitry A. Kazakov]

On Mon, 13 May 2013 08:21:14 +0300, Niklas Holsti wrote:

> The point of the example was to illustrate typestate analysis. For this
> example, with only Open - (Read/Write)* - Close, your approach collapses
> the example into a trivial one, where adherence to the operation
> protocol is ensured by the necessity to declare a File_Info object
> before it can be used. So it would no longer be a useful example.

It is still a useful example of a good software component design.

> Your approach works in some cases, but it is problematic if you cannot
> initialize the object to an "active" state in its declaration, for
> example because the "activation" is conditional in some way, or must be
> delayed.

This is rather a language problem. Most of such cases can be attributed to
the lack or insufficient constructors. The notorious Ada's problem with
task components is due to the lack of class-wide constructors, when
Initialize tries to sit on two chairs struggling to be both a specific and
a class-wide initialization.

> The "activation" must then be done in a statement, and the
> declaration leaves the object in some inactive initial state.

That is not a problem so long this state is not exposed. The idea is that
when you have an object which may transit from state to state (e.g. a
connection object, when the connection can be lost), you should not expose
this state. You better make the object to maintain the state (e.g. by
making the connection restored by the object automatically) and leave its
interface free of the state (e.g. an operation on unconnected object would
block or else raise Busy_Error etc).

[ Note that here again, the precondition is relaxed to true and the
operation behavior gets defined for the exceptional state, which cannot be
avoided anyway. ]
 
> Another limitation in your approach is that the opening and closing of
> different files must be strictly nested: if you declare and open file A,
> then declare and open file B, file B must be closed before file A is
> closed (as long as it all happens in the same task). Such forced
> constraints between the states of different object is often not wanted.

You can have a container, e.g. a bag, to handle this.

Jeffrey's model translates this into the problem of object's scope
(lifetime), which saves time and mental efforts. Each programmer faces it
on daily basis and has his ready-to-use solutions already.

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

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

[Yannick Duchêne (Hibou57)]

Le Mon, 13 May 2013 09:22:24 +0200, Dmitry A. Kazakov  
<mailbox@dmitry-kazakov.de> a écrit:

>> The "activation" must then be done in a statement, and the
>> declaration leaves the object in some inactive initial state.
>
> That is not a problem so long this state is not exposed. The idea is that
> when you have an object which may transit from state to state (e.g. a
> connection object, when the connection can be lost), you should not  
> expose
> this state. You better make the object to maintain the state (e.g. by
> making the connection restored by the object automatically) and leave its
> interface free of the state (e.g. an operation on unconnected object  
> would
> block or else raise Busy_Error etc).

Except for the exception which implies a lot of more things, the idea is  
indeed nice, while not universal. To stick with this example, that depends  
on the level of the application (it may or may not be aware of possible  
loss of connection), depends on the protocol in use (there may or may not  
be a way to know if the connection can be restored, if it is loss of if  
the peer closed it), that may be replacing a problem with another (state  
vs delay), and so on.

I agree with you (or may not, depending on the concrete case), except with  
this: “That is not a problem so long this state is not exposed”; this  
seems to suggest another design is an error and this is an universal  
pattern.


>> Another limitation in your approach is that the opening and closing of
>> different files must be strictly nested: if you declare and open file A,
>> then declare and open file B, file B must be closed before file A is
>> closed (as long as it all happens in the same task). Such forced
>> constraints between the states of different object is often not wanted.
>
> You can have a container, e.g. a bag, to handle this.
>
> Jeffrey's model translates this into the problem of object's scope
> (lifetime), which saves time and mental efforts. Each programmer faces it
> on daily basis and has his ready-to-use solutions already.

The same: may be an option, however nothing universal with it (ex. may be  
too much to pull the container concept, or for the second, objects  
identities may be important and one object may be opened and closed  
multiple times).

There is the topic of premature optimizations, there may be as well a  
topic about premature decisions (especially an issue if it adds  
dependencies or complexity).

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

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

[Robert A Duff]

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

> As said Niklas, the initial idea was requirements on the state of
> objects  for some operation to occur or not occur.

Yes, I understood that.  I just don't think "open/closed file" is
the best example.  Maybe something like, you can't do the "land
aircraft" operation unless you're in the "landing gear down" state.

By the way, Text_IO has more design flaws than I can count without
taking off my shoes.  ;-)

- Bob

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

[Jeffrey Carter]

On 05/13/2013 06:15 AM, Robert A Duff wrote:
>
> Yes, I understood that.  I just don't think "open/closed file" is
> the best example.  Maybe something like, you can't do the "land
> aircraft" operation unless you're in the "landing gear down" state.

Sure you can. It happens all the time. There are 2 kinds of pilots who fly 
retractable-gear airplanes: those who have made a gear-up landing, and those who 
will.

> By the way, Text_IO has more design flaws than I can count without
> taking off my shoes.  ;-)

All the file handling seems poorly designed. I would only have 1 file type (or a 
few, for input, output, and input-output files), for example, with different 
levels of operations on them. It seems ridiculous to have different File_Type's 
declared for Stream, Direct, and Text access to files.

-- 
Jeff Carter
"People called Romanes, they go the house?"
Monty Python's Life of Brian
79

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

[J-P. Rosen]

Le 13/05/2013 19:30, Jeffrey Carter a écrit :
> All the file handling seems poorly designed. I would only have 1 file
> type (or a few, for input, output, and input-output files), for example,
> with different levels of operations on them. It seems ridiculous to have
> different File_Type's declared for Stream, Direct, and Text access to
> files.
Because you are used to poor operating systems like Unix and Windows,
where files are simply a raw bag of bytes.

In the old times, when people still knew how to write OSes (VMS...), you
had various kinds of files that were managed at OS level. A sequential
file was the logical mapping for a tape, and a direct file for a disc.

-- 
J-P. Rosen
Adalog
2 rue du Docteur Lombard, 92441 Issy-les-Moulineaux CEDEX
Tel: +33 1 45 29 21 52, Fax: +33 1 45 29 25 00
http://www.adalog.fr

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

[Bill Findlay]

On 13/05/2013 19:01, in article kmr9ja$40g$1@dont-email.me, "J-P. Rosen"
<rosen@adalog.fr> wrote:

> Le 13/05/2013 19:30, Jeffrey Carter a écrit :
>> All the file handling seems poorly designed. I would only have 1 file
>> type (or a few, for input, output, and input-output files), for example,
>> with different levels of operations on them. It seems ridiculous to have
>> different File_Type's declared for Stream, Direct, and Text access to
>> files.
> Because you are used to poor operating systems like Unix and Windows,
> where files are simply a raw bag of bytes.
> 
> In the old times, when people still knew how to write OSes (VMS...), you
> had various kinds of files that were managed at OS level. A sequential
> file was the logical mapping for a tape, and a direct file for a disc.

Yes, and a complete pain in the neck it was too.

-- 
Bill Findlay
with blueyonder.co.uk;
use  surname & forename;

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

[Jeffrey Carter]

On 05/13/2013 11:01 AM, J-P. Rosen wrote:
>
> In the old times, when people still knew how to write OSes (VMS...), you
> had various kinds of files that were managed at OS level. A sequential
> file was the logical mapping for a tape, and a direct file for a disc.

Those are implementation details. They should not drive the design of high-level 
abstractions.

-- 
Jeff Carter
"People called Romanes, they go the house?"
Monty Python's Life of Brian
79

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

[Robert A Duff]

"J-P. Rosen" <rosen@adalog.fr> writes:

> Because you are used to poor operating systems like Unix and Windows,
> where files are simply a raw bag of bytes.

"sequence", not "bag".

> In the old times, when people still knew how to write OSes (VMS...), you
> had various kinds of files that were managed at OS level. A sequential
> file was the logical mapping for a tape, and a direct file for a disc.

I haven't used VMS in years, but I recall Record Management Services
being a nightmare!  Far more complexity than could possibly be worth
the functionality provided.

Anyway, I don't see VMS (etc) being a good excuse for the design
flaws of Text_IO, because Text_IO doesn't match VMS particularly
well.

Text_IO ought to provide simple streams-of-characters abstractions,
and what it looks like on the disk, or what it looks like to the
OS should be hidden at that level.

- Bob

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

[Niklas Holsti]

On 13-05-13 10:22 , Dmitry A. Kazakov wrote:
> On Mon, 13 May 2013 08:21:14 +0300, Niklas Holsti wrote:
> 
>> The point of the example was to illustrate typestate analysis. For this
>> example, with only Open - (Read/Write)* - Close, your approach collapses
>> the example into a trivial one, where adherence to the operation
>> protocol is ensured by the necessity to declare a File_Info object
>> before it can be used. So it would no longer be a useful example.
> 
> It is still a useful example of a good software component design.

Hm. In this thread, I think this example is interesting only if it can
show us alternatives to typestate analysis, giving the same verification
power by other means. I don't think this Open-in-declaration approach
(essentially removing the Open and Close operations from the problem)
applies in the general case, so I don't find it interesting in this thread.

>> Your approach works in some cases, but it is problematic if you cannot
>> initialize the object to an "active" state in its declaration, for
>> example because the "activation" is conditional in some way, or must be
>> delayed.
> 
> This is rather a language problem. Most of such cases can be attributed to
> the lack or insufficient constructors. The notorious Ada's problem with
> task components is due to the lack of class-wide constructors, when
> Initialize tries to sit on two chairs struggling to be both a specific and
> a class-wide initialization.

The initialization step, which is just the first state transition of an
object, is only a small part of the problem for typestate analysis.

>> The "activation" must then be done in a statement, and the
>> declaration leaves the object in some inactive initial state.
> 
> That is not a problem so long this state is not exposed. The idea is that
> when you have an object which may transit from state to state (e.g. a
> connection object, when the connection can be lost), you should not expose
> this state.

Even if the state is hidden from the clients, it is present internally,
and must be considered in any analysis of correctness.

> You better make the object to maintain the state (e.g. by
> making the connection restored by the object automatically) and leave its
> interface free of the state (e.g. an operation on unconnected object would
> block or else raise Busy_Error etc).

Here "unconnected object" is analogous to "closed file". The state
exists, even if hidden from clients. In fact, from the point of view of
typestate analysis, the state is or should be visible, since it affects
the availability or success of operations on the object.

The goal of typestate analysis, even of client code, is to show if
operations can be illegally applied and thus fail, for example by
raising Busy_Error. For this, the analysis must include the
"unconnected" state.

>> Another limitation in your approach is that the opening and closing of
>> different files must be strictly nested: if you declare and open file A,
>> then declare and open file B, file B must be closed before file A is
>> closed (as long as it all happens in the same task). Such forced
>> constraints between the states of different object is often not wanted.
> 
> You can have a container, e.g. a bag, to handle this.

This introduces a new object -- the container -- with its own, perhaps
more complex state: whether or not it contains the object (e.g. a
File_Object) that is our real interest. Not a good idea, I think.

> Jeffrey's model translates this into the problem of object's scope
> (lifetime), which saves time and mental efforts.

Only in this special case, the "file" example, where the state structure
is so simple that after hiding the first state transition (Open) into
the construction of the object, and the last state transition (Close)
into the destruction, there is only one state left (Is_Open), which
makes typestate analysis trivial.

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

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

[J-P. Rosen]

Le 13/05/2013 21:13, Robert A Duff a écrit :
> I haven't used VMS in years, but I recall Record Management Services
> being a nightmare!  Far more complexity than could possibly be worth
> the functionality provided.
> 
Maybe you used it from C... I remember VMS had to invent new access
methods specifically for C, because the VMS view of a file was too high
level for C.

> Text_IO ought to provide simple streams-of-characters abstractions,
> and what it looks like on the disk, or what it looks like to the
> OS should be hidden at that level.
Sorry, but I see a stream of characters as a lower level abstraction
than an organised sequence of pages, lines, and individual characters
(not that I am especially fan of pages)

-- 
J-P. Rosen
Adalog
2 rue du Docteur Lombard, 92441 Issy-les-Moulineaux CEDEX
Tel: +33 1 45 29 21 52, Fax: +33 1 45 29 25 00
http://www.adalog.fr

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

[Randy Brukardt]

"Niklas Holsti" <niklas.holsti@tidorum.invalid> wrote in message 
news:av8pvtFehv2U1@mid.individual.net...
...
> It is interesting that Randy thinks his ideas regarding a future
> replacement for Ada resemble the typestate concept, but that the
> typestate concept as implemented in Plaid seems to be implementable in
> Ada 2012. Perhaps Randy's ideas go much further than this, however.

The main thing I was thinking about was some extension to the things that 
have to be compile-time analyzable (as Static Predicates are in Ada 2012). 
Probably the basis of them would remain subtypes and subprogram profiles 
(via preconditions and postconditions). For the Open example, that requires 
some way to encode the notion of "properties" in a statically understandable 
way. Perhaps you are right that discriminants would do the trick, but we'd 
want them to be "virtual" discriminants without any runtime cost.

I agree that you can get the effect of typestate analysis in Ada 2012 using 
discriminants, predicates, and pre/postconditions, but those would be 
checked at runtime. The key here for me is to require static detection of 
these errors, even when variables and unconstrained formal parameters are 
involved.

Anyway, I'm just musing here as opposed to having fully worked out ideas. So 
I could in fact be going down the wrong path.

                                                Randy.

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

[Randy Brukardt]

"Robert A Duff" <bobduff@shell01.TheWorld.com> wrote in message 
news:wccmwrzu9oj.fsf@shell01.TheWorld.com...
> Jeffrey Carter <spam.jrcarter.not@spam.not.acm.org> writes:
>
>> I'm not sure I see the point in having an object for a closed file,
>
> Yeah, I was about to post basically the same thing.  A closed file
> is pretty useless.  It's like an uninitialized variable -- you can't
> do anything with it.

Yes, and of course Ada allows uninitialized variables, too. Clearly the same 
sorts of reasons apply.

We briefly tried that model when designing Claw, but it really didn't work, 
because the underlying handle can be closed by some other operation and in 
that case the object becomes closed (we called it "invalid") without any 
explicit action in your code. For a windowing system, that other operation 
can be the guy with the mouse, who can easily screw up all of your carefully 
thought out code.

Another issue is that doing that means that you are limited to Ada's scopes 
for managing objects, which means that you're limited in how you can set up 
and tear down structures. (You can always get around those problems by 
essentially making your clients use new/unchecked_deallocation for 
everything -- but I don't consider that a step forward. I'd rather have 
"invalid" objects than force people to use access types.)

We used that model throughout Claw, and that included in Claw.Directories, 
so of course it carried over into the original proposal for Ada.Directories 
(which was heavily based on Claw.Directories). So "Search_Type" originally 
had a "Is_Valid" routine, which eventually got folded into "More_Entries". 
(Which demonstrates an intermediate approach that often works -- have a 
default initial state which is well-defined but not useful.)

                                        Randy.

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

[Randy Brukardt]

"Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message 
news:hxkln519n179.1kt13z7phxg2f.dlg@40tude.net...
> On Sat, 11 May 2013 09:06:11 +0200, Georg Bauhaus wrote:
>
>> 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?
>
> "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.

Which is why I'm suggesting something built on top of Ada's types for this 
purpose.

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

Again, this is precisely what I'm talking about. SPARK is a disaster because 
it insists that you do everything it's way, or nothing at all. I want to be 
able to incrementally add checks as they become apparent.

The big disconnect is that you (and lots of other misguided people) think 
that types have something to do with operations. Types are more fundamental 
than operations; they get *used* in operations, rather than the operations 
being part of the type. Ideally, a type is nothing but a black box (an Ada 
private type). Operations are the next level of complexity, and exist 
separately from the types.

                             Randy.

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

[Randy Brukardt]

"Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message 
news:1181wq8vjk781.2wo8wfbtbr61.dlg@40tude.net...
> On Fri, 10 May 2013 20:00:39 -0500, Randy Brukardt wrote:
>
>> "Dmitry A. Kazakov" <mailbox@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?

It makes no sense to separate them. They're instances of the same thing 
(I've been both simultaeously, for example). And if you did separate them, 
you are going to have to have components of the other kind. So what? 
"component of" does not suddenly break an abstraction or eliminate 
separation, any more than having a parameter of a type eliminates 
separation.

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

No one ought to care about the "implementation point of view". You design 
specifications for the client, the implementation is whatever you need.

> 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 whatsoever that keeping your types separate is going 
to somehow lead to a "god_class". And of course OOD uses the same ideas --  
it would be silly to ignore the common sense lessons of modular programming, 
OOD was supposed to build on top of them. But they got all tangled up in OOP 
religion, worrying about "inheritance" and "object purity" and other silly 
things rather than getting the problems solved. (And most problems don't 
lend themselves very well to OOD religion.)

                            Randy.

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

[Randy Brukardt]

"Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message 
news:bkozr3g5i0hk$.15qnfap6hrj20$.dlg@40tude.net...
> On Fri, 10 May 2013 19:09:12 -0500, Randy Brukardt wrote:
>
>> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message
>> news:1jc46ynzptlxm.1fafjhr8hlblq.dlg@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.
>
> You didn't answer the question. If it goes without a proof now, why can it
> continue so?

I'm afraid I don't understand your question, so I can't answer it directly. 
I can only repeat the situation:

You are proposing a complete overhaul of the model of types in Ada. You keep 
claiming that this overhaul would be compatible without a shred of proof 
that this is achievable. You would have to find *some* way to convince the 
Ada community that your revised model is in fact 100% compatible with the 
current model. A semi-formal proof would clearly be the best way to do that.

Remember that Ada is defined in English, and as such there is not currently 
a formal way to tell if we're staying compatible. As such, there is a great 
reluctance to make major changes to the text, because there is no way to 
find regression errors. Our experience has been that we introduce about as 
many serious bugs to the standard as we make changes to it, simply because 
we can't easily tell when we break things.

As such, there would have to be an amazingly serious problem that absolutely 
had to be fixed in Ada for us to consider any major change to the model --  
even if such a model would be an improvement. The only sure-fire way to get 
a level of confidence in such a model would be to provide extrodinary proof 
of its correctness compared to the existing standard. And that's all I'm 
talking about when I say a "semi-formal proof" is needed.

                                                Randy.

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

[Dmitry A. Kazakov]

On Mon, 13 May 2013 22:38:43 +0200, J-P. Rosen wrote:

> Le 13/05/2013 21:13, Robert A Duff a écrit :
>> I haven't used VMS in years, but I recall Record Management Services
>> being a nightmare!  Far more complexity than could possibly be worth
>> the functionality provided.
>> 
> Maybe you used it from C... I remember VMS had to invent new access
> methods specifically for C, because the VMS view of a file was too high
> level for C.
> 
>> Text_IO ought to provide simple streams-of-characters abstractions,
>> and what it looks like on the disk, or what it looks like to the
>> OS should be hidden at that level.
> Sorry, but I see a stream of characters as a lower level abstraction
> than an organised sequence of pages, lines, and individual characters
> (not that I am especially fan of pages)

Exactly.

IMO, RSX and VMS were precursors of type-safe (one could say an OO) file
system which never came to life.

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

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

[Dmitry A. Kazakov]

On Mon, 13 May 2013 21:29:15 -0500, Randy Brukardt wrote:

> The big disconnect is that you (and lots of other misguided people) think 
> that types have something to do with operations. Types are more fundamental 
> than operations; they get *used* in operations, rather than the operations 
> being part of the type.

Neither type nor operation nor value exist before other. You cannot
separate them. It is like magnetic field and current.

> Operations are the next level of complexity, and exist 
> separately from the types.

You cannot define operation without type and conversely. Your concept comes
from languages of 60's built upon predefined types, e.g. FORTRAN. There
predefined types were given and the rest only used them as building blocks
for algorithms.

The point is that conceptually there is nothing special in such types. They
are not better (no more fundamental) and not worse than user-defined types.
And the operations you define on them are as much operations as the
built-in operations. Operations and types are fully equal.

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

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

[Dmitry A. Kazakov]

On Mon, 13 May 2013 22:20:12 +0300, Niklas Holsti wrote:

> On 13-05-13 10:22 , Dmitry A. Kazakov wrote:
>> On Mon, 13 May 2013 08:21:14 +0300, Niklas Holsti wrote:
>> 
>>> The point of the example was to illustrate typestate analysis. For this
>>> example, with only Open - (Read/Write)* - Close, your approach collapses
>>> the example into a trivial one, where adherence to the operation
>>> protocol is ensured by the necessity to declare a File_Info object
>>> before it can be used. So it would no longer be a useful example.
>> 
>> It is still a useful example of a good software component design.
> 
> Hm. In this thread, I think this example is interesting only if it can
> show us alternatives to typestate analysis, giving the same verification
> power by other means. I don't think this Open-in-declaration approach
> (essentially removing the Open and Close operations from the problem)
> applies in the general case, so I don't find it interesting in this thread.

It does. The idea is not to expose the state or else split object into
smaller ones.

>>> Your approach works in some cases, but it is problematic if you cannot
>>> initialize the object to an "active" state in its declaration, for
>>> example because the "activation" is conditional in some way, or must be
>>> delayed.
>> 
>> This is rather a language problem. Most of such cases can be attributed to
>> the lack or insufficient constructors. The notorious Ada's problem with
>> task components is due to the lack of class-wide constructors, when
>> Initialize tries to sit on two chairs struggling to be both a specific and
>> a class-wide initialization.
> 
> The initialization step, which is just the first state transition of an
> object, is only a small part of the problem for typestate analysis.

And the point is that this would probably be bad design.

>>> The "activation" must then be done in a statement, and the
>>> declaration leaves the object in some inactive initial state.
>> 
>> That is not a problem so long this state is not exposed. The idea is that
>> when you have an object which may transit from state to state (e.g. a
>> connection object, when the connection can be lost), you should not expose
>> this state.
> 
> Even if the state is hidden from the clients, it is present internally,
> and must be considered in any analysis of correctness.

But not at the client side!

>> You better make the object to maintain the state (e.g. by
>> making the connection restored by the object automatically) and leave its
>> interface free of the state (e.g. an operation on unconnected object would
>> block or else raise Busy_Error etc).
> 
> Here "unconnected object" is analogous to "closed file".

No. Unconnected object can become connected asynchronously to the client. 

If the state can be controlled by the client, the object should be designed
so that its sate were usable. See Jeffrey's design.

If the sate cannot be controlled the object should be responsible in each
of its states. I.e. the state should be hidden by the object
implementation.

> The state exists, even if hidden from clients.

Right. The design question is who is to control the state. You want clients
to do this. Which is distributed design overhead.

> In fact, from the point of view of
> typestate analysis, the state is or should be visible, since it affects
> the availability or success of operations on the object.

This is exactly why I consider this paradigm wrong from the design's POV.

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

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

[Dmitry A. Kazakov]

On Mon, 13 May 2013 22:01:56 -0500, Randy Brukardt wrote:

> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message 
> news:bkozr3g5i0hk$.15qnfap6hrj20$.dlg@40tude.net...
>> On Fri, 10 May 2013 19:09:12 -0500, Randy Brukardt wrote:
>>
>>> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message
>>> news:1jc46ynzptlxm.1fafjhr8hlblq.dlg@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.
>>
>> You didn't answer the question. If it goes without a proof now, why can it
>> continue so?
> 
> I'm afraid I don't understand your question, so I can't answer it directly. 
> I can only repeat the situation:
> 
> You are proposing a complete overhaul of the model of types in Ada. You keep 
> claiming that this overhaul would be compatible without a shred of proof 
> that this is achievable. You would have to find *some* way to convince the 
> Ada community that your revised model is in fact 100% compatible with the 
> current model. A semi-formal proof would clearly be the best way to do that.
> 
> Remember that Ada is defined in English, and as such there is not currently 
> a formal way to tell if we're staying compatible. As such, there is a great 
> reluctance to make major changes to the text, because there is no way to 
> find regression errors. Our experience has been that we introduce about as 
> many serious bugs to the standard as we make changes to it, simply because 
> we can't easily tell when we break things.
> 
> As such, there would have to be an amazingly serious problem that absolutely 
> had to be fixed in Ada for us to consider any major change to the model --  
> even if such a model would be an improvement. The only sure-fire way to get 
> a level of confidence in such a model would be to provide extrodinary proof 
> of its correctness compared to the existing standard. And that's all I'm 
> talking about when I say a "semi-formal proof" is needed.

You are saying that there are political reasons not to do this. I am fully
aware of this. I am not a politician and have not idea how to deal with
that. My point is that these reasons are NOT technical ones.

You suggest that there could be a way to convince people like you by
presenting some formalism? Seriously? You would reject the formalism using
same methods you and others did before. We could not even agree on the
notion of type! Not even on IMPROTANCE of types for Ada!

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

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

[Yannick Duchêne (Hibou57)]

Le Tue, 14 May 2013 09:44:00 +0200, Dmitry A. Kazakov  
<mailbox@dmitry-kazakov.de> a écrit:

> On Mon, 13 May 2013 21:29:15 -0500, Randy Brukardt wrote:
>
>> The big disconnect is that you (and lots of other misguided people)  
>> think
>> that types have something to do with operations. Types are more  
>> fundamental
>> than operations; they get *used* in operations, rather than the  
>> operations
>> being part of the type.
>
> Neither type nor operation nor value exist before other. You cannot
> separate them. It is like magnetic field and current.

An operation has a type, while a type may be defined without operations  
(not a lot useful, however still possible). The type gets realised even  
before runtime (except for some subtypes), most values too, while an  
operation, is nothing but a value (with an implicit type) before runtime.  
Values and types, seems to me the most fundamental concept. At least, this  
looks unavoidable for analysis, which looks at everything, as if it was  
static.

If a program is mainly a structure, then it is mainly made of typed values  
(and the program as a whole, is a complex value). Functional programming,  
where even a function is a value, won't say the opposite.

This fact is also what makes the differences between data (hopefully typed  
data) and program, narrow, and a matter of interpretation (not that much  
apparent with general purpose languages such as Ada; more apparent with  
domain‑specific‑languages).


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

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

[Dmitry A. Kazakov]

On Tue, 14 May 2013 13:34:09 +0200, Yannick Duchêne (Hibou57) wrote:

> Le Tue, 14 May 2013 09:44:00 +0200, Dmitry A. Kazakov  
> <mailbox@dmitry-kazakov.de> a écrit:
> 
>> Neither type nor operation nor value exist before other. You cannot
>> separate them. It is like magnetic field and current.
> 
> An operation has a type,, while a type may be defined without operations  
> (not a lot useful, however still possible). 

   procedure Foo;

> If a program is mainly a structure, then it is mainly made of typed values  
> (and the program as a whole, is a complex value).

No idea, what does this mean.

Value is not a programming language term, it belongs to the application
domain. Value is the meaning attributed to the state of a typed object in
some context.

E.g.

   Salary : Buckazoid := 1;

Salary is meant to have the value of 1 Buckazoid.

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

Weaker typing as a part of the way to stronger typing? (Was: Seeking for papers about tagged types vs access to subprograms)

[Jacob Sparre Andersen]

Randy Brukardt wrote:
> Dmitry A. Kazakov wrote:

[ Nothing whatsoever about access to subprograms. - Please update the
  subject line to match what you are writing about. It makes it much
  easier for everybody to follow you. ]

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

Considering that SPARK on one level is rather un-typed (all numbers seem
to be equivalent on the constraint error checking level of SPARK), you
may be onto something.  But how would avoid making a monster like Java,
where programmers can use weak types everywhere (except as the main
subprogram).

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

Might be right.  But how would you separate operations on the
representation level from operations on the typed ("profile") level?

Greetings,

Jacob
-- 
"... there may be many others,
 but they haven't been discovered"             -- Tom Lehrer

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

[Yannick Duchêne (Hibou57)]

Le Tue, 14 May 2013 14:16:52 +0200, Dmitry A. Kazakov  
<mailbox@dmitry-kazakov.de> a écrit:

> On Tue, 14 May 2013 13:34:09 +0200, Yannick Duchêne (Hibou57) wrote:
>> An operation has a type,, while a type may be defined without operations
>> (not a lot useful, however still possible).
>
>    procedure Foo;

This is not random data, this has type. The type is implicit in most case  
and becomes more explicit with access to sub‑program (the same with many  
other languages), and as well‑known, there is nothing in Ada looking like  
an access to an untyped entity, which implies the sub‑program has an  
implicit type. You just can't dynamically create or manipulate value of  
that type in Ada (unlike with say, SML or other LISP variant), which makes  
that type special, and prevented it to be given a name, a syntax or ever  
be explicitly referred to in Ada (not the same with all languages).

>> If a program is mainly a structure, then it is mainly made of typed  
>> values
>> (and the program as a whole, is a complex value).
>
> No idea, what does this mean.
>
> Value is not a programming language term, it belongs to the application
> domain.

Then think about meta‑programming or “programming as a human activity”.  
That said, obviously, the concept of value I referred to, was either at a  
level higher than values manipulated by the program, or else, constants  
values referred to (and interpreted) by the program.


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

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

[Randy Brukardt]

"Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message 
news:mk9m6fxa1jbr$.mm0kw7g3igma$.dlg@40tude.net...
...
> Value is not a programming language term, it belongs to the application
> domain.

The Ada Standard uses the word an awful lot (starting with 3.2(1)) for 
something that isn't "a programming language term". The AARM even gives a 
definition for "value" (3.2(10.a)). I'd say that it certainly is a 
programming language term, but it's one whose meaning is assumed to be 
understood and thus is axiomatic. (There are of course a number of such 
terms, it would be impossible to define every word used in a Standard.)

                                Randy.

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

[Randy Brukardt]

"Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message 
news:1wzphazeho17m$.zy00zh7l7yu5$.dlg@40tude.net...
> On Mon, 13 May 2013 22:01:56 -0500, Randy Brukardt wrote:
...
>> As such, there would have to be an amazingly serious problem that 
>> absolutely
>> had to be fixed in Ada for us to consider any major change to the 
>> model --
>> even if such a model would be an improvement. The only sure-fire way to 
>> get
>> a level of confidence in such a model would be to provide extrodinary 
>> proof
>> of its correctness compared to the existing standard. And that's all I'm
>> talking about when I say a "semi-formal proof" is needed.
>
> You are saying that there are political reasons not to do this. I am fully
> aware of this. I am not a politician and have not idea how to deal with
> that. My point is that these reasons are NOT technical ones.

Two points here:

(1) Virtually all constraints are political, not technical. Without the 
constraints posed by cost, compatibility, and the like, essentially anything 
is possible. Especially in software. One of the first problems we had to 
solve when starting as one of the Ada 9x User-Implementer teams was how to 
answer the question of implementability that we were supposed to provide 
feedback on. Virtually everything is implementable with enough effort (and 
levels of indirection); the question was where to draw the line. Eventually, 
we found that the question had been posed incorrectly; the Ada 9x team 
wanted to know about any implementation difficulties so they could sort out 
whether or not to change the feature to reduce the issues.

Indeed, you could consider Ada's goals like readability and maintainability 
to be political, rather than technical, constraints. So pretty much anything 
that could be proposed is going to have to deal with the various political 
constraints -- they *cannot* be ignored in any real-world scenario.

I'm not a politician either, and I'd rather avoid those sorts of games, but 
one has to do what it takes to get things done.

> You suggest that there could be a way to convince people like you by
> presenting some formalism? Seriously? You would reject the formalism using
> same methods you and others did before. We could not even agree on the
> notion of type! Not even on IMPROTANCE of types for Ada!

You might be right. The only sure-fire way to convince everyone would be to 
write wording for the entire proposal and as well have a prototype 
implementation. If the prototype implementation were to show only minor 
incompatibilities when processing existing Ada code (including the ACATS, 
AdaCore test suite, and the like), that would be clear evidence that it is 
OK.

But I'm quite aware that that's impractical. (Which is the crux of the 
problem, of course.)

I suspect that you might be able to convince some people if you provided a 
fully fleshed out proposal with revisions to the wording of the Standard. 
That would mitigate the terminology problem because you would have to 
provide definitions for all of the terms that you use. But I suspect that it 
also too large a job for one person (as someone who has undertook smaller 
revisions that took a *long* time, like the revisions to support the aspect 
terminology -- and the language has long had some of that terminology, I 
wasn't quite starting from scratch.)

When I was talking about a semi-formal proof above, I was thinking of it 
layered on top of fully fleshed out wording. I don't think you're every 
going to get much interest without that, precisely because of the issues 
with terminology.

                                      Randy.

Re: Weaker typing as a part of the way to stronger typing? (Was: Seeking for papers about tagged types vs access to subprograms)

[Randy Brukardt]

"Jacob Sparre Andersen" <jacob.sparre@koparo.com> wrote in message 
news:871u99ohk7.fsf_-_@adaheads.sparre-andersen.dk...
> Randy Brukardt wrote:
>> Dmitry A. Kazakov wrote:
>
> [ Nothing whatsoever about access to subprograms. - Please update the
>  subject line to match what you are writing about. It makes it much
>  easier for everybody to follow you. ]
>
>>> 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.
>
> Considering that SPARK on one level is rather un-typed (all numbers seem
> to be equivalent on the constraint error checking level of SPARK), you
> may be onto something.  But how would avoid making a monster like Java,
> where programmers can use weak types everywhere (except as the main
> subprogram).
>
>> 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.
>
> Might be right.  But how would you separate operations on the
> representation level from operations on the typed ("profile") level?

I don't think there are any operations on the representation level (well, 
maybe a small number, like the predefined numeric operations in Ada). I 
would guess that such operations would have an empty profile (meaning 
they're always applicable), while most operations would have profiles that 
would restrict their applicability.

In any case, these are the questions for a new language design. If they are 
already clearly answered, we wouldn't need a new language!

                                          Randy.

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

[Robert A Duff]

"Randy Brukardt" <randy@rrsoftware.com> writes:

>...Our experience has been that we introduce about as 
> many serious bugs to the standard as we make changes to it, simply because 
> we can't easily tell when we break things.

I don't think it's QUITE that bad.  I think there were around 1000
AI's for Ada 83, 400 for Ada 95, and 300 for Ada 2005.  Not all of
those were approved.  I suspect the vast majority of Ada 83 AI's
were bug reports, whereas for Ada 95 and 2005, many were enhancements.
So the number of bug reports has been going down over the years.

But your point is correct:  We can't do automated regression testing
on the RM, so it's easy to insert bugs.

I don't think it's possible to do a major overhaul of the Ada type
system while remaining compatible.  But then, in 1990 or so, I
didn't think it was possible to add object-oriented support to
Ada 83.  Tucker proved me wrong.  ;-)

- Bob

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

[Robert A Duff]

"Randy Brukardt" <randy@rrsoftware.com> writes:

> Yes, and of course Ada allows uninitialized variables, too. Clearly the same 
> sorts of reasons apply.

Yes.  I think what's missing is an ability to initialize an object
after creating it (either by declaring it, or via "new").  My hobby
language has that.  And it distinguishes syntactically between
initialization and assignment_statement.

Ada uses ":=" for both, so if you do:

    F : constant File_Type; -- Illegal!
    ... -- calculate File_Name
    F := Open (File_Name); -- Illegal!

that last statement is an assignment_statement in Ada, whereas it
is conceptually an initialization.  (That's illegal in Ada, because
F is declared 'constant'.  You can erase 'constant', but it's STILL
illegal, because File_Type is a build-in-place limited type.)

> We briefly tried that model when designing Claw, but it really didn't work, 
> because the underlying handle can be closed by some other operation and in 
> that case the object becomes closed (we called it "invalid") without any 
> explicit action in your code. For a windowing system, that other operation 
> can be the guy with the mouse, who can easily screw up all of your carefully 
> thought out code.

So how does it work in CLAW?  Are you talking about some task
writing into a window, while the user is asynchronously clicking
on "close window"?  So that task must be constantly checking
Is_Open (or handling an exception), and locking things to make
sure there are no race conditions?

> Another issue is that doing that means that you are limited to Ada's scopes 
> for managing objects, which means that you're limited in how you can set up 
> and tear down structures.

I think allowing to separate initialization from declaration
can solve that.

>...(You can always get around those problems by 
> essentially making your clients use new/unchecked_deallocation for 
> everything -- but I don't consider that a step forward. I'd rather have 
> "invalid" objects than force people to use access types.)

Agreed -- heap allocation solves the problem, but creates other
problems.

- Bob

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

[Robert A Duff]

"J-P. Rosen" <rosen@adalog.fr> writes:

> Le 13/05/2013 21:13, Robert A Duff a écrit :
>> I haven't used VMS in years, but I recall Record Management Services
>> being a nightmare!  Far more complexity than could possibly be worth
>> the functionality provided.
>> 
> Maybe you used it from C...

No, I don't recall writing any C on VMS.  On Unix, Windows,
misc embedded systems, yes, but not on VMS.

On VMS I mainly used Pascal, with a little bit of assembly.
Pascal I/O is also poorly designed, by the way, which is
probably why I was horsing around with RMS.  Text I/O in Java
or Lisp, for example, is superior to either C or Ada, IMHO.

>... I remember VMS had to invent new access
> methods specifically for C, because the VMS view of a file was too high
> level for C.

Interesting.  I don't see why -- VMS files can represent a
"sequence of bytes", among other things.

>> Text_IO ought to provide simple streams-of-characters abstractions,
>> and what it looks like on the disk, or what it looks like to the
>> OS should be hidden at that level.
> Sorry, but I see a stream of characters as a lower level abstraction
> than an organised sequence of pages, lines, and individual characters
> (not that I am especially fan of pages)

OK, let's agree that pages are junk.

That leaves "sequence of lines, each of which is a sequence of
characters".  Some programs do indeed want to view text that way.  But
Text_IO doesn't support that very conveniently.  There isn't even a Line
type in Ada.  And the Get_Line procedure requires a fixed-length string,
and the length of that string is guaranteed to be both too short and too
long.  (I'm talking about flaws in the original design, here, so Ada 83
-- I realize a Get_Line function was later added.)  So the design
encourages the sort of broken program that doesn't work right when there
are long lines.  There are lots of C programs with the same kind of bug,
for similar reasons.

And there's no data type in Ada that can portably represent a multi-line
piece of text.  Of course, you can build your own, but something so
basic ought to be predefined.

Furthermore, lots of programs do NOT want that two-level structure.
They just want a sequence of characters, with one (not two!)
particular character that means "line break".  They want to have
code like:

    ... loop
        case Current_Char is
            ...

where a line break is treated similarly (or identically)
to ' '.  The GNAT front end is like that (the lexical
analysis, I mean), and it doesn't use Text_IO to read the
source text.

- Bob

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

[Robert A Duff]

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

> IMO, RSX and VMS were precursors of type-safe (one could say an OO) file
> system which never came to life.

I'd love to see a type-safe file system.  I've thought a lot about
how to design such a thing, and I don't think it's easy.  Ada types
don't work, because they vanish when the program exits, whereas files
out-live programs.

And I don't see VMS files as being a good basis for that.  If they're
the "precursor" as you say, they are extremely primitive.  And yet
super complicated.

I never used RSX-11.

- Bob

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

[Yannick Duchêne (Hibou57)]

Le Tue, 14 May 2013 21:35:55 +0200, Robert A Duff  
<bobduff@shell01.theworld.com> a écrit:

> Yes.  I think what's missing is an ability to initialize an object
> after creating it (either by declaring it, or via "new").  My hobby
> language has that.  And it distinguishes syntactically between
> initialization and assignment_statement.
> […]
> I think allowing to separate initialization from declaration
> can solve that.

Does your hobby language has static or runtime check to catch access to  
uninitialized variables?

I don't see the point with deferred initialization, it seems to be an  
object state finally (states, again). Either you can tell a variable was  
or was not initialized, and then it has a state and it is finally  
initialized before you suppose it is, or else it can't tell the variable  
was not initialized because it really initialize nothing at the  
declaration, and then it's perhaps unsafe.

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

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

[Yannick Duchêne (Hibou57)]

Le Tue, 14 May 2013 21:56:14 +0200, Robert A Duff  
<bobduff@shell01.theworld.com> a écrit:
> Furthermore, lots of programs do NOT want that two-level structure.
> They just want a sequence of characters, with one (not two!)
> particular character that means "line break".  They want to have
> code like:
>
>     ... loop
>         case Current_Char is
>             ...

That's a corner case, and why Ada should do pre‑tokenization for this  
single case? If end‑of‑line is made of two characters in some  
environments, then the end of line token is not a character, or else it's  
a character in a kind of internal character set (what most people surely  
do, indeed, and that's out of the standard).

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

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

[Yannick Duchêne (Hibou57)]

Le Tue, 14 May 2013 21:02:32 +0200, Randy Brukardt <randy@rrsoftware.com>  
a écrit:
> If the prototype implementation were to show only minor
> incompatibilities when processing existing Ada code (including the ACATS,
> AdaCore test suite,

AdaCore test suite? If that exist, that must be not public…

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

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

[G.B.]

On 14.05.13 10:32, Dmitry A. Kazakov wrote:
> You suggest that there could be a way to convince people like you by
> presenting some formalism? Seriously? You would reject the formalism using
> same methods you and others did before. We could not even agree on the
> notion of type! Not even on IMPROTANCE of types for Ada!

Agreement on the notion of type, or on importance of types for
Ada, is achieved precisely when you semi-formally establish
a possibility for others to understand your meaning. I meant it.

As is usual in semi-formal discourse, words ask for definitions.
Politely presuming that others find everything obvious cannot
is obviously not working.

One way to create a meaningful semi-formal basis is to add a
subscript to words, a subscript that identifies which of the
possible meanings the reader should assume.
In fact, the suffix "for Ada" in your "types for Ada" corresponds
with one such subscripting operation.

Then, if there is a single, consistent KAVOA notion of type,
if this notion is a prerequisite for your considerations,
then surely the KAVOA notion of type can be defined using
n declarative statments,

   {Stmt_1, ..., Stmt_n}.

Let the name of this notion of type be Type[∆]. Likewise,
if the Ada notion of type is defined by

   {Stmt_1', ..., Stmt_m'},

then let the name of this notion of type be Type[✇]. Use
any notation you like and that you and your readers understand,
but do use notation.

Then there is starting point for comparisons, for speaking
meaningfully about changes and their effects, etc., because
you and your readers see (from the subscript) the objects
of comparison, and the objects of change.

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

[Dmitry A. Kazakov]

On Wed, 15 May 2013 06:24:49 +0200, Yannick Duchêne (Hibou57) wrote:

> Le Tue, 14 May 2013 21:56:14 +0200, Robert A Duff  
> <bobduff@shell01.theworld.com> a écrit:
>> Furthermore, lots of programs do NOT want that two-level structure.
>> They just want a sequence of characters, with one (not two!)
>> particular character that means "line break".  They want to have
>> code like:
>>
>>     ... loop
>>         case Current_Char is
>>             ...
> 
> That's a corner case, and why Ada should do pre‑tokenization for this  
> single case?

It is not a tokenization. You turned abstraction upside down. The text file
is a sequence of lines. A line is a sequence of characters. Period.

If you have a broken OS, like Linux/Windows is, you cannot have this
abstraction. Instead you emulate it as a lower-level stream of octets with
escape sequences used to simulate lines. What is wrong with that? It
conflates representation with the interface.

> If end‑of‑line is made of two characters in some  
> environments, then the end of line token is not a character, or else it's  
> a character in a kind of internal character set (what most people surely  
> do, indeed, and that's out of the standard).

It is not how it was under VMS. It did not have such stuff in record
oriented files. Such files had each line kept with the character count. It
was not a stream of characters. Though under VMS you could read it as a
stream of octets if you wanted.

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

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

[Dmitry A. Kazakov]

On Tue, 14 May 2013 16:00:46 -0400, Robert A Duff wrote:

> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> writes:
> 
>> IMO, RSX and VMS were precursors of type-safe (one could say an OO) file
>> system which never came to life.
> 
> I'd love to see a type-safe file system.  I've thought a lot about
> how to design such a thing, and I don't think it's easy.  Ada types
> don't work, because they vanish when the program exits, whereas files
> out-live programs.

They would continue to live in the OS. Files could be viewed as persistent
objects.

I agree that in existing Ada would be difficult, because it does not
properly separate representation, which you would like to be able to change
as the OS evolves. E.g. record members should be operations etc.

Then Ada lacks protection against intentional misuse. It should allow
making private stuff memory protected.

There are general issues with typed OS interfaces. E.g. when putting stuff
into a DLL, it does not work well unless drastically limited to very
primitive set of subprograms and basic types like int and char *.

I think that CS in general is not ready for this, as any innovation in the
area of OS design was trumped down by Linux and Windows for decades. The
focus was shifted to services and garbage protocols.

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

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

[Peter C. Chapin]

On Tue, 14 May 2013, Dmitry A. Kazakov wrote:

>   procedure Foo;

This procedure does nothing unless it has side effects. If so, then those 
side effects entail operations on values of a particular type.

> Value is not a programming language term, it belongs to the application
> domain. Value is the meaning attributed to the state of a typed object in
> some context.
>
> E.g.
>
>   Salary : Buckazoid := 1;
>
> Salary is meant to have the value of 1 Buckazoid.

A type is a pair of sets: a set of values and a set of operations defined 
over those values (for example as functions taking items from the first 
set as a parameter). Either set can be empty. In any case "value" is most 
certainly a programming language term. You can't talk about a type without 
talking about the values that inhabit that type (again, could be an empty 
set in certain special cases).

Peter

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

[Peter C. Chapin]

On Wed, 15 May 2013, Dmitry A. Kazakov wrote:

> If you have a broken OS, like Linux/Windows is, you cannot have this 
> abstraction. Instead you emulate it as a lower-level stream of octets 
> with escape sequences used to simulate lines. What is wrong with that? 
> It conflates representation with the interface.

The genius of the Linux (and Windows) way of representing files is that 
the operating system does not need to know anything about the nature of 
the data being stored in the files. Thus new file types can be defined by 
applications without any OS changes. This does push the burden of 
interpreting the file's format into the application but the benefit is a 
more generic operating system. When one considers all the different kinds 
of files created by applications today, I can't imagine any other way 
working well.

Peter

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

[Dmitry A. Kazakov]

On Wed, 15 May 2013 11:14:09 +0200, G.B. wrote:

> Then there is starting point for comparisons, for speaking
> meaningfully about changes and their effects, etc., because
> you and your readers see (from the subscript) the objects
> of comparison, and the objects of change.

The starting point is that there is no such thing as Ada notion of type, or
C notion of type, for that matter. It would be as silly as "Ada notion of
grammar" or "Ada notion of number". There is an Ada type system of certain
properties, Ada grammar, Ada way of using numbers.

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

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

[Yannick Duchêne (Hibou57)]

Le Wed, 15 May 2013 13:31:36 +0200, Peter C. Chapin <PChapin@vtc.vsc.edu>  
a écrit:
> The genius of the Linux (and Windows) way of representing files is that  
> the operating system does not need to know anything about the nature of  
> the data being stored in the files. Thus new file types can be defined  
> by applications without any OS changes. This does push the burden of  
> interpreting the file's format into the application but the benefit is a  
> more generic operating system. When one considers all the different  
> kinds of files created by applications today, I can't imagine any other  
> way working well.

I may see a better options: what about multiple views for a file? File  
view drivers? Query interface to query what interface(s)/view(s) a file  
provides? A standard format to describe interfaces? Standardisation of a  
basic set of very common interface (which may be completed as the  
technologies evolves)?

Pushing this kind of responsibility to the applications, is the surest way  
to have a mess of non‑interoperable things, wasting duplicates,  
inconsistencies, data corruption, applications guessing all the time, etc  
(and that's indeed how it goes so far). Just imagine what if each  
applications was responsible of accessing devices or managing memory  
pages. The comparison is not that much excessive: nor POSIX nor Linux  
provides anything for mandatory locks on files (at least, Windows is  
cleaner on that aspect), and it only works between cooperative  
applications (modulo their bugs) and can be fully ignored accidentally or  
worst, on purpose, by any other application.

There is too much responsibilities left to applications in this area. The  
OS discharges itself from near to everything but storage devices access  
(or may be an OS is just a big device driver), which is just a way to say  
it provides near to no service at all here (except a stream of raw bytes),  
and each possible view must be a duplicated feature in each application  
(or multiple shared and overlapping non‑standardized libraries, which ends  
into others and similar issues).

Even determination of the MIME type of a file does not work well, and may  
have to be fixed by some application (just think of `file` and `xdg-mime`  
on Ubuntu, not always returning the same answer for a query). What the OS  
or environment does not provides, each application has to duplicate it,  
and may be wrong with or may miss some point.

That's one of my biggest (*) grief with OS (at least widespread OS, as I  
don't known others nor old ones).

(*) Another big one is about applications each believing it's the centre  
of the world, which comes with similar consequences: wasting with  
duplications, inconsistencies, poor UI behaviour standardisation,  
encumbered workspace, and so on.

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

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

[Dmitry A. Kazakov]

On Wed, 15 May 2013 07:31:36 -0400, Peter C. Chapin wrote:

> On Wed, 15 May 2013, Dmitry A. Kazakov wrote:
> 
>> If you have a broken OS, like Linux/Windows is, you cannot have this 
>> abstraction. Instead you emulate it as a lower-level stream of octets 
>> with escape sequences used to simulate lines. What is wrong with that? 
>> It conflates representation with the interface.
> 
> The genius of the Linux (and Windows) way of representing files is that 
> the operating system does not need to know anything about the nature of 
> the data being stored in the files.

E.g. in order to execute it. Right?

> Thus new file types can be defined by 
> applications without any OS changes. This does push the burden of 
> interpreting the file's format into the application but the benefit is a 
> more generic operating system.

Viruses and performance that makes i7 to perform as i486.

> When one considers all the different kinds 
> of files created by applications today, I can't imagine any other way 
> working well.
 
A much more efficient, safer, compacter system?

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

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

[Dmitry A. Kazakov]

On Wed, 15 May 2013 07:20:23 -0400, Peter C. Chapin wrote:

> On Tue, 14 May 2013, Dmitry A. Kazakov wrote:
> 
>>   procedure Foo;
> 
> This procedure does nothing unless it has side effects. If so, then those 
> side effects entail operations on values of a particular type.

Nevertheless it is an operation that does not refer to any particular type.
 
>> Value is not a programming language term, it belongs to the application
>> domain. Value is the meaning attributed to the state of a typed object in
>> some context.
>>
>> E.g.
>>
>>   Salary : Buckazoid := 1;
>>
>> Salary is meant to have the value of 1 Buckazoid.
> 
> A type is a pair of sets: a set of values and a set of operations defined 
> over those values (for example as functions taking items from the first 
> set as a parameter). Either set can be empty. In any case "value" is most 
> certainly a programming language term.

   type Employee is ...;

How is employee a language term?

   task type Driver is ...;

Show me an RM section which defines the values of this type.

And the simplest possible example why the language has nothing to do with
values is this:

   type Some_Transcendental_Numbers is (e, Pi, Euler);

What is the value of e?

> You can't talk about a type without 
> talking about the values that inhabit that type (again, could be an empty 
> set in certain special cases).

This is what I said in response to Randy. That type, operations, values
cannot be separated to each other. Neither is more or less fundamental than
other.

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

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

[J-P. Rosen]

Le 14/05/2013 21:56, Robert A Duff a �crit :
> "J-P. Rosen" <rosen@adalog.fr> writes:
>> ... I remember VMS had to invent new access
>> methods specifically for C, because the VMS view of a file was too high
>> level for C.
> 
> Interesting.  I don't see why -- VMS files can represent a
> "sequence of bytes", among other things.
It was long ago, but AFAIR, VMS had several forms of structured files,
that were very inconvenient for C - DEC added another one later for raw
bytes

> [...] And the Get_Line procedure requires a fixed-length string,
> and the length of that string is guaranteed to be both too short and too
> long.  (I'm talking about flaws in the original design, here, so Ada 83
> -- I realize a Get_Line function was later added.) 
I have written my own Get_Line function, which is perfectly Ada-83
compatible. True enough, the Ada-83 mantra was "Ada is so powerful, you
can write anything you need" - and then people complained that they had
to rewrite everything. That's why the library was considerably increased
later on. But on the principle, dealing with long lines was not really a
problem, and did not require buffers of arbitrary limited size.

> [...]
> Furthermore, lots of programs do NOT want that two-level structure.
> They just want a sequence of characters, with one (not two!)
> particular character that means "line break".  They want to have
> code like:
> 
>     ... loop
>         case Current_Char is
>             ...
> 
> where a line break is treated similarly (or identically)
> to ' '.  The GNAT front end is like that (the lexical
> analysis, I mean), and it doesn't use Text_IO to read the
> source text.
> 
The proper (and easy) way to check for the end of line is to call the
function mysteriously called End_Of_Line ;-). I don't see a problem with
that. If you want to replace end of lines with a particular character,
just write your custom Get_Char function (you'll have to write it anyway
to manage look-ahead characters).

On the opposite, I don't like languages that invent characters on the
fly. In Ada, you read the characters that are in the file. The end of
line is not a character in a sufficiently evolved operating system.

-- 
J-P. Rosen
Adalog
2 rue du Docteur Lombard, 92441 Issy-les-Moulineaux CEDEX
Tel: +33 1 45 29 21 52, Fax: +33 1 45 29 25 00
http://www.adalog.fr

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

[G.B.]

On 15.05.13 14:08, Dmitry A. Kazakov wrote:
> On Wed, 15 May 2013 11:14:09 +0200, G.B. wrote:
>
>> Then there is starting point for comparisons, for speaking
>> meaningfully about changes and their effects, etc., because
>> you and your readers see (from the subscript) the objects
>> of comparison, and the objects of change.
>
> The starting point is that there is no such thing as Ada notion of type, or
> C notion of type, for that matter. It would be as silly as "Ada notion of
> grammar" or "Ada notion of number". There is an Ada type system of certain
> properties, Ada grammar, Ada way of using numbers.

Ada does *not* define grammar.
Ada *does* define type.
Ada does *not* define KAVOA types.

Given this lack, it is important to fill in the blanks
(subscripts) with your definition in order be able to
contrast the definitions.

Statements of denial, signifying nothing.

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

[Dmitry A. Kazakov]

On Wed, 15 May 2013 16:43:25 +0200, G.B. wrote:

> Ada *does* define type.

It does not. Ada RM defines [informally] some system of types. Its
instances of are called in the RM "types". In any wider context, e.g.
discussion about desired or not language changes, they should denoted as
"Ada types", or "Ada 83 types" etc.

> Ada does *not* define KAVOA types.

Maybe. I have no idea what KAVOA type is.

Type is a set of values and operations involving these values.

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

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

[Jeffrey Carter]

On 05/15/2013 04:31 AM, Peter C. Chapin wrote:
>
> The genius of the Linux (and Windows) way of representing files is that the
> operating system does not need to know anything about the nature of the data
> being stored in the files. Thus new file types can be defined by applications
> without any OS changes. This does push the burden of interpreting the file's
> format into the application but the benefit is a more generic operating system.
> When one considers all the different kinds of files created by applications
> today, I can't imagine any other way working well.

Ada 83 had a philosophy of providing building blocks and letting the user use 
them to create what he wants. The language provided the means to create 
mathematical functions and unbounded arrays and queues and sets, so the language 
did not provide such things. This resulted in a proliferation of external 
libraries and negative comparisons to languages with large standard libraries.

In 1995 Ada was revised to include some of these things, and again in 2007 more 
of them, including hashed and ordered maps and sets, but the underlying building 
blocks of an O(log N) searchable structure and a hash table were not provided to 
the user. This represents the opposite philosophy to that of Ada 83: providing 
high-level abstractions but not the building blocks to build them.

(Of course, Ada 83 required a compiler implementer to have a bignum package, but 
not to make it available to users of the compiler, so the difference is not as 
clear as I'm pretending.)

Between these 2 extremes is a philosophy of providing building blocks and common 
high-level abstractions build from them.

Physically, a disk is a bunch of bytes; everything else is built on top of that. 
The Unix file concept provides the building blocks but no higher-level 
abstractions. VMS (which, IIRC, did not initially have a sequence-of-bytes way 
to access files) represented the other extreme. Presumably there are some common 
higher-level file types that it would be useful to have the OS provide in 
addition to the sequence-of-bytes view, just as it's useful to have a language 
provide common higher-level constructs as well as the building blocks to build them.

-- 
Jeff Carter
"Nobody expects the Spanish Inquisition!"
Monty Python's Flying Circus
22

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

[Eryndlia Mavourneen]

On Wednesday, May 15, 2013 1:15:07 PM UTC-5, Jeffrey Carter wrote:
> 
> Physically, a disk is a bunch of bytes; everything else is built on top of that. 
> 
> The Unix file concept provides the building blocks but no higher-level 
> abstractions. VMS (which, IIRC, did not initially have a sequence-of-bytes way 
> to access files) represented the other extreme. Presumably there are some common 
> higher-level file types that it would be useful to have the OS provide in 
> addition to the sequence-of-bytes view, just as it's useful to have a language 
> provide common higher-level constructs as well as the building blocks to build them.
> 

Actually, VMS and its predecessor RSX-11 (all flavors) provided a wide range of choices from 

1) physical block/sector device I/O to 

2) logical block/sector file I/O to 

3) variable-sized file record structure (sequential I/O) [the size was separate from the record but did not preclude the inclusion of terminator(s) or any other characters in the record] to 

4) fixed-length file record structure (sequential or direct I/O) to 

5) indexed-sequential file structure (sequential or indexed I/O using 1 or more indices).

RMS (Record Management Services) represented the last 3 (3-5) of these.
These choices are so complete that for many DB applications, they are all that is needed.  I have seen many personnel REQs for DB programmer or administrator that specified the DB as RMS.  I have used all 5 I/O modes and did not find any of them particularly difficult or cumbersome to use.  Even more so with Ada.

DEC's layered product Rdb provided for true relational DB capability.

Btw, VMS is still maintained and upgraded by HP.

[As an addendum -- I used DEC Ada and preferred it in some ways over Gnat.  Error messages are the main thing that comes to mind.  DEC Ada didn't just give you the error message but cross-referenced it to the specific LRM paragraph(s) that dealt with the situation.  Very helpful.]

Eryndlia Mavourneen

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

[Dmitry A. Kazakov]

On Wed, 15 May 2013 12:18:34 -0700 (PDT), Eryndlia Mavourneen wrote:

> [As an addendum -- I used DEC Ada and preferred it in some ways over Gnat. 
> Error messages are the main thing that comes to mind.  DEC Ada didn't just
> give you the error message but cross-referenced it to the specific LRM
> paragraph(s) that dealt with the situation.  Very helpful.]

Me too. DEC Ada was a great compiler as well as DEC C.

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

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

[Peter C. Chapin]

On Wed, 15 May 2013, Yannick Duchêne (Hibou57) wrote:

> I may see a better options: what about multiple views for a file? File 
> view drivers? Query interface to query what interface(s)/view(s) a file 
> provides? A standard format to describe interfaces? Standardisation of a 
> basic set of very common interface (which may be completed as the 
> technologies evolves)?
>
> Pushing this kind of responsibility to the applications, is the surest 
> way to have a mess of non‑interoperable things, wasting duplicates, 
> inconsistencies, data corruption, applications guessing all the time, 
> etc (and that's indeed how it goes so far).

I understand what you're saying. The issue ultimately comes down to 
deciding how high up the chain of abstraction one expects the operating 
system to go. We can probably all agree that the OS should be responsible 
for managing the hardware itself (via device drivers). We can also 
probably all agree that the application should deal with problems that are 
unique to it.

Yet who should deal with the structure of, say, a JPEG image? Should every 
application that wants to manipulate such images duplicate the code 
required to do so? Should the OS materialize the "JPEG file" abstraction 
directly in its API?

Of course in the real world JPEG images are manipulated by a library that 
multiple applications can use. Thus while the code *is* duplicated in 
each process as far as the OS can see, the programmers are not really 
writing that code freshly every time. In fact, in many systems that code 
could reside in a shared library... a kind of gray zone between the 
application and the OS.

Any OS that tried to provide a specialized JPEG file type is biting off a 
lot. It would be taking on the responsibility of providing every kind of 
specialized file type that could ever exist. To do that it would have to 
provide a low level "sequence of bytes" abstraction along with some kind 
of extension mechanism (shared libraries?) to allow users to add on the 
support they need.

Isn't that what we have now, more or less?

Peter

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

[Yannick Duchêne (Hibou57)]

Le Wed, 15 May 2013 21:57:57 +0200, Dmitry A. Kazakov  
<mailbox@dmitry-kazakov.de> a écrit:

> Me too. DEC Ada was a great compiler as well as DEC C.

What version of Ada does/did it support? Ada 95? Ada 2005? Why do you say  
“was”?


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

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

[Dmitry A. Kazakov]

On Wed, 15 May 2013 22:37:46 +0200, Yannick Duchêne (Hibou57) wrote:

> Le Wed, 15 May 2013 21:57:57 +0200, Dmitry A. Kazakov  
> <mailbox@dmitry-kazakov.de> a écrit:
> 
>> Me too. DEC Ada was a great compiler as well as DEC C.
> 
> What version of Ada does/did it support? Ada 95? Ada 2005?

Ada 83

> Why do you say “was”?

DEC is dead.

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

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

[Dmitry A. Kazakov]

On Wed, 15 May 2013 15:59:07 -0400, Peter C. Chapin wrote:

> Yet who should deal with the structure of, say, a JPEG image?

The implementation of the type if the OS were typed.

> Should every 
> application that wants to manipulate such images duplicate the code 
> required to do so?

The operations of the type could be shared.

> Should the OS materialize the "JPEG file" abstraction 
> directly in its API?

JPEG would implement the interface of some base image type.

It is not much different from how OSes handle drivers. You can register new
driver. A driver belongs to a class of devices (=implements some device
interface, e.g. block device).

The API of a driver is a kind of dispatching operation, e.g.
Read/Write/Open/Close/IOCTL. It is very rudimental and not properly defined
as a type, nonetheless.

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

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

[Peter C. Chapin]

On Wed, 15 May 2013, Dmitry A. Kazakov wrote:

>>>   procedure Foo;
>>
>> This procedure does nothing unless it has side effects. If so, then those
>> side effects entail operations on values of a particular type.
>
> Nevertheless it is an operation that does not refer to any particular type.

It doesn't refer to the type in the source text because of the limitations 
of the Ada language (specifically, side effects remain undocumented). 
SPARK rectifies that to some degree with global annotations. However, the 
operation is still an operation on values of some type.

>> A type is a pair of sets: a set of values and a set of operations defined
>> over those values (for example as functions taking items from the first
>> set as a parameter). Either set can be empty. In any case "value" is most
>> certainly a programming language term.
>
>   type Employee is ...;
>
> How is employee a language term?

Weren't we talking about "value" as a programming language term? I 
understand that to mean "value" as something used by people when talking 
about programming languages. "Employees" is just a name in some program... 
and specifically the name of a type. I don't follow what this has to do 
with a discussion about values.

>   task type Driver is ...;
>
> Show me an RM section which defines the values of this type.

The values of a task type are the code fragments that implement the 
task. Here I'm speaking in general terms, of course.

> And the simplest possible example why the language has nothing to do with
> values is this:
>
>   type Some_Transcendental_Numbers is (e, Pi, Euler);
>
> What is the value of e?

Some_Transcendental_Numbers is an enumeration type. One of it's values is 
'e'. There is no significance to 'e' other than that. At least at the 
level of types.

Peter

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

[Dmitry A. Kazakov]

On Wed, 15 May 2013 17:12:09 -0400, Peter C. Chapin wrote:

> On Wed, 15 May 2013, Dmitry A. Kazakov wrote:
> 
>>> A type is a pair of sets: a set of values and a set of operations defined
>>> over those values (for example as functions taking items from the first
>>> set as a parameter). Either set can be empty. In any case "value" is most
>>> certainly a programming language term.
>>
>>   type Employee is ...;
>>
>> How is employee a language term?
> 
> Weren't we talking about "value" as a programming language term?

You consider value being a language term. I objected, pointing out that
value is the meaning of some program state, the meaning which is always
outside the language and from the problem space. The only case when a value
can be an Ada term is when the program is an Ada compiler.

> I 
> understand that to mean "value" as something used by people when talking 
> about programming languages.

Yes.

> "Employees" is just a name in some program... 
> and specifically the name of a type. I don't follow what this has to do 
> with a discussion about values.

The type Employee has values denoting employees of some business in some
Ada program.

>>   task type Driver is ...;
>>
>> Show me an RM section which defines the values of this type.
> 
> The values of a task type are the code fragments that implement the 
> task. Here I'm speaking in general terms, of course.

So,

   X, Y : Driver;

have same values? You seem to confuse value for its representation. The
value of a task type is not even computable, or the value of clock. The
representation of a task value might be a combination of some code, TCB,
the state of system queues etc.

>> And the simplest possible example why the language has nothing to do with
>> values is this:
>>
>>   type Some_Transcendental_Numbers is (e, Pi, Euler);
>>
>> What is the value of e?
> 
> Some_Transcendental_Numbers is an enumeration type. One of it's values is 
> 'e'. There is no significance to 'e' other than that. At least at the 
> level of types.

And what significance has Ada.Numerics'

e : constant :=
         2.71828_18284_59045_23536_02874_71352_66249_77572_47093_69996;

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

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

[G.B.]

> [As an addendum -- I used DEC Ada and preferred it in some ways over Gnat.  Error messages are the main thing that comes to mind.  DEC Ada didn't just give you the error message but cross-referenced it to the specific LRM paragraph(s) that dealt with the situation.  Very helpful.]

Compilers using AdaMagic as their front end frequently
reference the LRM in error messages. Now that SofCheck,
maker of AdaMagic, has joined AdaCore, maybe GNAT will
more frequently do so, too, rather than just re-using
LRM terms in disguise, as in

"invalid prefix in selected component"

This error message is not about the component.

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

[Peter C. Chapin]

On Thu, 16 May 2013, Dmitry A. Kazakov wrote:

>> Weren't we talking about "value" as a programming language term?
>
> You consider value being a language term. I objected, pointing out that 
> value is the meaning of some program state, the meaning which is always 
> outside the language and from the problem space. The only case when a 
> value can be an Ada term is when the program is an Ada compiler.
>
>> I understand that to mean "value" as something used by people when 
>> talking about programming languages.
>
> Yes.

You said earlier, "value is the meaning of some program state..." So 
"value" is, indeed, a term used when discussing programming languages. 
That was my original contention. Recall that we were talking about types 
and values and their relationship. I again return to my original 
statement: a type is two sets, a set of values and a set of operations. 
Are you disagreeing with that? I honestly can't tell.

> So,
>
>   X, Y : Driver;
>
> have same values?

Yes, I would say so.

> You seem to confuse value for its representation. The value of a task 
> type is not even computable, or the value of clock. The representation 
> of a task value might be a combination of some code, TCB, the state of 
> system queues etc.

I actually don't think I'm all that confused. I borrow concepts that are 
standard in functional languages where functions are, indeed, first class 
values. There a function's value is its (source) code. Two different 
instances of the same function represent the same value just as two 
different instances of the integer literal "2" represent the same value.

The machine representation of a function---how it is converted to 
executable form---is at the compiler's discretion, of course. In some 
languages function types have only a single operation, that of 
"application" (calling). Some of the items you mentioned above exist to 
support the execution of that operation; they are not part of the value.

Ada tasks are not quite like functions but conceptually there are 
similarities. One important limitation of Ada is that every task type is 
inhabited with only a single value. It isn't possible to create multiple 
task bodies behind a task type definition. In contrast consider:

function F1(X : Integer) return String;
function F2(X : Integer) return String;

Here F1 and F2 have the same "function type." They are two different 
values that inhabit that type just as "2" and "3" are two different values 
inhabiting Integer.

But if you say

task type T is
   ...
end T;

You can only write one body to go with the type. Every instance of type T 
thus has the same value---the type has only one value.

This limitation doesn't change the concepts, it just reflects a limitation 
of Ada. In the more general case there would be "task operators" that 
would allow you to compose tasks to make new tasks (higher order tasks?) 
and you would be able to store different tasks into the same variable of 
task type provided all the tasks had the same type (but possibly different 
bodies). Of course this language isn't Ada.

That said, the Ada 2005 features of synchronized and protected interfaces 
are moving into this terrian. A full theoretical accounting of Ada task 
types would be a very interesting exercise (has it been done?).

> And what significance has Ada.Numerics'
>
> e : constant :=
>         2.71828_18284_59045_23536_02874_71352_66249_77572_47093_69996;

As I understand it, 'e' has type Universal_Float and the 2.718... is a 
value inhabiting that type. I guess I don't understand what point you are 
making here. I apologize if I cut too much context.

Peter

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

[Yannick Duchêne (Hibou57)]

Le Thu, 16 May 2013 13:31:58 +0200, Peter C. Chapin <PChapin@vtc.vsc.edu>  
a écrit:
> I again return to my original statement: a type is two sets, a set of  
> values and a set of operations.

There is nothing like operation as something distinct from values, at  
least formally. Operations as understood in procedural languages, is an  
interpretation, especially when it has side effects, it differs entirely.  
There is no operations, and there are at most functions, which are  
expressions which are values (a partially evaluated expression like a  
function is supposed to be most often unless constant, is still a value,  
this is just a set which is that of a domain, still a value).

(don't kick too hard if it happens I'm boring :D )

I feel there is a mix of formal definitions and language specific  
definitions, while both can't be mixed.

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

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

[Dmitry A. Kazakov]

On Thu, 16 May 2013 07:31:58 -0400, Peter C. Chapin wrote:

> On Thu, 16 May 2013, Dmitry A. Kazakov wrote:
> 
>>> Weren't we talking about "value" as a programming language term?
>>
>> You consider value being a language term. I objected, pointing out that 
>> value is the meaning of some program state, the meaning which is always 
>> outside the language and from the problem space. The only case when a 
>> value can be an Ada term is when the program is an Ada compiler.
>>
>>> I understand that to mean "value" as something used by people when 
>>> talking about programming languages.
>>
>> Yes.
> 
> You said earlier, "value is the meaning of some program state..." So 
> "value" is, indeed, a term used when discussing programming languages. 
> That was my original contention. Recall that we were talking about types 
> and values and their relationship. I again return to my original 
> statement: a type is two sets, a set of values and a set of operations. 
> Are you disagreeing with that?

No. Why should I?

>> So,
>>
>>   X, Y : Driver;
>>
>> have same values?
> 
> Yes, I would say so.

Really? X is an *equivalent* of Y?

>> You seem to confuse value for its representation. The value of a task 
>> type is not even computable, or the value of clock. The representation 
>> of a task value might be a combination of some code, TCB, the state of 
>> system queues etc.
> 
> I actually don't think I'm all that confused. I borrow concepts that are 
> standard in functional languages where functions are, indeed, first class 
> values. There a function's value is its (source) code. Two different 
> instances of the same function represent the same value just as two 
> different instances of the integer literal "2" represent the same value.

Because the literal 2 [of type Integer] denotes the same value in all
contexts. But X, Y : Driver clearly do not do that. If X and Y are not
equivalent how they could have the same value? Either the values are
different or else you need to bring some other stuff beyond types, values
and operations into the picture.

>> And what significance has Ada.Numerics'
>>
>> e : constant :=
>>         2.71828_18284_59045_23536_02874_71352_66249_77572_47093_69996;
> 
> As I understand it, 'e' has type Universal_Float and the 2.718... is a 
> value inhabiting that type. I guess I don't understand what point you are 
> making here.

The point is about the value of e. You said that when declared as I did, it
has no significance, just a random pattern of bits. Do I interpret you
correctly? Does this same logic apply to e of Ada.Numerics? If not where is
a difference? If you think that values should have "significance", then
what is significance? Why enumeration value does not have it and
Universal_Integer does?

P.S. What you call "significance" is the value. What you call "value" is a
representation.

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

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

[J-P. Rosen]

Le 16/05/2013 11:41, G.B. a �crit :
> Compilers using AdaMagic as their front end frequently
> reference the LRM in error messages. Now that SofCheck,
> maker of AdaMagic, has joined AdaCore, maybe GNAT will
> more frequently do so, too
I doubt it.

All Ada83 compilers were referencing the LRM. It was a deliberate
decision of the Gnat authors not to do so, because they felt that in
many cases, it was more confusing than helpful. In a few cases where a
reference is really needed, Gnat does output the reference. But not for
"missing semi-colon", as other compilers did.

-- 
J-P. Rosen
Adalog
2 rue du Docteur Lombard, 92441 Issy-les-Moulineaux CEDEX
Tel: +33 1 45 29 21 52, Fax: +33 1 45 29 25 00
http://www.adalog.fr

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

[Eryndlia Mavourneen]

On Wednesday, May 15, 2013 3:48:35 PM UTC-5, Dmitry A. Kazakov wrote:
> On Wed, 15 May 2013 22:37:46 +0200, Yannick Duchêne (Hibou57) wrote:
> > Le Wed, 15 May 2013 21:57:57 +0200, Dmitry A. Kazakov  
> > <mailbox@dmitry-kazakov.de> a écrit:
> 
>> Me too. DEC Ada was a great compiler as well as DEC C.
> 
> > What version of Ada does/did it support? Ada 95? Ada 2005?
> 
> Ada 83
> 
> > Why do you say “was”?
> 
> DEC is dead.

When VMS and the hardware it runs on (VAX and Alpha) were picked up by HP, HP dropped DEC Ada and adopted the VMS version of Gnat.

Eryndlia Mavourneen

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

[Eryndlia Mavourneen]

On Thursday, May 16, 2013 6:31:58 AM UTC-5, Peter C. Chapin wrote:
> ...
> In the more general case there would be "task operators" that 
> would allow you to compose tasks to make new tasks (higher order tasks?) 
> and you would be able to store different tasks into the same variable of 
> task type provided all the tasks had the same type (but possibly different 
> bodies). Of course this language isn't Ada.
> 
> That said, the Ada 2005 features of synchronized and protected interfaces 
> are moving into this terrian. A full theoretical accounting of Ada task 
> types would be a very interesting exercise (has it been done?).
> ...
> Peter

Yes, indeed!  In a project of my own that I work on in my nearly negligible spare time, I use a number of task interfaces representing possible features of a service and compose the specific service I desire using a mix of these interfaces.  Some interfaces are required by virtually every service, however most are not.  This is one method to trim the size of the individual services, instead of trying to shoe-horn many unused features into a single task.

Eryndlia Mavourneen

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

[Peter C. Chapin]

On Thu, 16 May 2013, Dmitry A. Kazakov wrote:

>>> So,
>>>
>>>   X, Y : Driver;
>>>
>>> have same values?
>>
>> Yes, I would say so.
>
> Really? X is an *equivalent* of Y?

Sure. If it were allowed the expression 'X = Y' should return True. I 
realize that equivalence of functions is a difficult concept in general (I 
believe it's undecidable to determine if two functions f_1 and f_2 are 
equivalent even if you can see the source code of both) but here since the 
code for both X and Y is, in fact, the very same program text, it seems 
clear that they are equivalent.

X and Y above of course may contain different state information as they 
run but that's all related to the operation of execution; it doesn't 
distinguish their "task values."

These concepts are all quite straightforward, it seems to me, in the 
context of functional languages. Of course Ada isn't a functional language 
and it has side effects, etc, so things do get a bit messier. I still 
contend, however, that the basic ideas still... er... apply.

> Because the literal 2 [of type Integer] denotes the same value in all
> contexts. But X, Y : Driver clearly do not do that. If X and Y are not
> equivalent how they could have the same value?

I guess this is where we disagree. To me X and Y do denote the same value 
in all contexts; they are equivalent.

> Either the values are different or else you need to bring some other 
> stuff beyond types, values and operations into the picture.

Are you referring to the execution state here? To my mind that dynamic 
information is just part of the operation of execution. It's necessary to 
make that operation work but, yes, I agree that it is a separate matter 
from the types and values, etc.

Modeling state in a clean way is slippery business. You might be able to 
bring it into the context of this discussion by treating the state of each 
task as a kind of mutable parameter to the task. As such there could be an 
implicit type for that parameter... some kind of record type, etc... but 
it does get messy.

>>> e : constant :=
>>>         2.71828_18284_59045_23536_02874_71352_66249_77572_47093_69996;
>>
>> As I understand it, 'e' has type Universal_Float and the 2.718... is a
>> value inhabiting that type. I guess I don't understand what point you are
>> making here.
>
> The point is about the value of e. You said that when declared as I did, it
> has no significance, just a random pattern of bits. Do I interpret you
> correctly? Does this same logic apply to e of Ada.Numerics? If not where is
> a difference?

We're talking about two different 'e's here. In the first case 'e' was an 
enumeration literal. The type in that example was suggestively named 
Transcendental_Constants (or something like that... I forget exactly), but 
any connection between 'e' and the mathematical value of e was purely in 
the mind of the programmer. In Ada terms 'e' was a value of that type but 
nothing beyond that. That's what I meant by it not having any 
significance.

In the second case 'e' is a named number bound to a value in the 
Universal_Float type that is clearly intended to be the mathematical e... 
at least to the closest degree permitted by the available values in that 
type (I guess in this case it's really limited by the amount of space the 
implementer wants to use when writing the declaration. Am I correct in 
saying that Universal_Float has infinite precision?)

I suppose I don't understand the point you were trying to make originally 
with the enumeration type. There 'e' was a value of the specified type. 
Was that it?

Peter

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

[Dmitry A. Kazakov]

On Thu, 16 May 2013 09:10:11 -0400, Peter C. Chapin wrote:

> On Thu, 16 May 2013, Dmitry A. Kazakov wrote:
> 
>>>> So,
>>>>
>>>>   X, Y : Driver;
>>>>
>>>> have same values?
>>>
>>> Yes, I would say so.
>>
>> Really? X is an *equivalent* of Y?
> 
> Sure. If it were allowed the expression 'X = Y' should return True.

If X嚙踝蕭Y, you don't need two instances of.

> I realize that equivalence of functions is a difficult concept in general

There is nothing difficult in that. A function is a set of pairs. Two sets
are equal when contain same elements.

> X and Y above of course may contain different state information as they 
> run but that's all related to the operation of execution; it doesn't 
> distinguish their "task values."

Of course it does. For example: it can happen that X'Terminated /=
Y'Terminated.

>> Because the literal 2 [of type Integer] denotes the same value in all
>> contexts. But X, Y : Driver clearly do not do that. If X and Y are not
>> equivalent how they could have the same value?
> 
> I guess this is where we disagree. To me X and Y do denote the same value 
> in all contexts; they are equivalent.

They are evidently not, which can be easily demonstrated by presenting a
program which would yield different results depending on whether X or Y is
used.
 
>> Either the values are different or else you need to bring some other 
>> stuff beyond types, values and operations into the picture.
> 
> Are you referring to the execution state here?

It is your concept, I am only giving you enough rope to hang yourselves...

> To my mind that dynamic 
> information is just part of the operation of execution. It's necessary to 
> make that operation work but, yes, I agree that it is a separate matter 
> from the types and values, etc.

Which means that your model is inadequate to describe the way programs
work, and more generally to programming.

>>>> e : constant :=
>>>>         2.71828_18284_59045_23536_02874_71352_66249_77572_47093_69996;
>>>
>>> As I understand it, 'e' has type Universal_Float and the 2.718... is a
>>> value inhabiting that type. I guess I don't understand what point you are
>>> making here.
>>
>> The point is about the value of e. You said that when declared as I did, it
>> has no significance, just a random pattern of bits. Do I interpret you
>> correctly? Does this same logic apply to e of Ada.Numerics? If not where is
>> a difference?
> 
> We're talking about two different 'e's here. In the first case 'e' was an 
> enumeration literal. The type in that example was suggestively named 
> Transcendental_Constants (or something like that... I forget exactly), but 
> any connection between 'e' and the mathematical value of e was purely in 
> the mind of the programmer.

How Universal_Integer is different?

> In Ada terms 'e' was a value of that type but 
> nothing beyond that. That's what I meant by it not having any 
> significance.
> 
> In the second case 'e' is a named number bound to a value in the 
> Universal_Float type that is clearly intended to be the mathematical e...

How it is more "clearly intended" than enumeration 'e'? 

Note that neither is mathematical e. They *model* e = as you said "purely
in the mind of the programmer." This is what value is, an idea behind a
computational state.

> at least to the closest degree permitted by the available values in that 
> type (I guess in this case it's really limited by the amount of space the 
> implementer wants to use when writing the declaration. Am I correct in 
> saying that Universal_Float has infinite precision?)

It has an indefinite precision.

> I suppose I don't understand the point you were trying to make originally 
> with the enumeration type. There 'e' was a value of the specified type. 
> Was that it?

The value of e was meant to represent the transcendental number e. The type
was meant to model real numbers. Similarly Ada.Numerics e is meant to
represent e. And Universal_Real is meant to model real numbers. e is not
Ada term. It is a term of mathematical analysis. Neither type is real, they
are only models of.

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

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

[G.B.]

On 16.05.13 15:54, Dmitry A. Kazakov wrote:
>> I realize that equivalence of functions is a difficult concept in general
> There is nothing difficult in that. A function is a set of pairs. Two sets
> are equal when contain same elements.

I think the difficulty is that eq is not computable. For example,
if f1 and f2 are any Ada compilers, produce an algorithm that computes

  eq(f1, f2)

Then, proceed to finding eq of procedures computing eq.

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

[Jeffrey Carter]

On 05/16/2013 05:45 AM, Eryndlia Mavourneen wrote:
>
> When VMS and the hardware it runs on (VAX and Alpha) were picked up by HP, HP
> dropped DEC Ada and adopted the VMS version of Gnat.

GNAT contains many features to make it compatible with DEC Ada programs that use 
implementation-dependent features of DEC Ada. An example is pragma Passive; 
others may be found by searching for "DEC Ada" in the GNAT RM. These exist 
because AdaCore received a contract to supply a version of GNAT as the VMS 
Ada-95 compiler, with the requirement that it accept all 
implementation-dependent features of DEC Ada.

I once used GNAT in Ada-83 mode as the development compiler for a system that 
was compiled using DEC Ada and run on VAX/VMS.

-- 
Jeff Carter
"I'm a kike, a yid, a heebie, a hook nose! I'm Kosher,
Mum! I'm a Red Sea pedestrian, and proud of it!"
Monty Python's Life of Brian
77

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

[Peter C. Chapin]

On Thu, 16 May 2013, G.B. wrote:

> On 16.05.13 15:54, Dmitry A. Kazakov wrote:

>>> I realize that equivalence of functions is a difficult concept in general
>> There is nothing difficult in that. A function is a set of pairs. Two sets
>> are equal when contain same elements.
>
> I think the difficulty is that eq is not computable. For example,
> if f1 and f2 are any Ada compilers, produce an algorithm that computes
>
>  eq(f1, f2)
>
> Then, proceed to finding eq of procedures computing eq.

The other problem with Dmitry's earlier suggestion is that the sets he's 
talking about could be infinite in size (at least in principle). Comparing 
infinite sets can't be done in finite time, of course, so it doesn't 
really solve the problem in the general case. This is part of being not 
computable. I believe computing the equivalence of functions is 
undecidable, but I don't have a proof off hand (maybe one could be looked 
up).

Peter

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

[Dmitry A. Kazakov]

On Thu, 16 May 2013 14:09:59 -0400, Peter C. Chapin wrote:

> On Thu, 16 May 2013, G.B. wrote:
> 
>> On 16.05.13 15:54, Dmitry A. Kazakov wrote:
> 
>>>> I realize that equivalence of functions is a difficult concept in general
>>> There is nothing difficult in that. A function is a set of pairs. Two sets
>>> are equal when contain same elements.
>>
>> I think the difficulty is that eq is not computable. For example,
>> if f1 and f2 are any Ada compilers, produce an algorithm that computes
>>
>>  eq(f1, f2)
>>
>> Then, proceed to finding eq of procedures computing eq.
> 
> The other problem with Dmitry's earlier suggestion is that the sets he's 
> talking about could be infinite in size (at least in principle).

Exactly, but it is a problem with your definition of value, not with mine. 

To me, as I said before, value does not belong to the language. Thus it is
not the language's problem to establish if two values are same. If the
programmer cares, he may declare operation "=" and implement it according
to the semantics of the problem space. If I wanted a type which values were
cardinal numbers aleph-0, aleph-1 etc, no problem with that.

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

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

[Niklas Holsti]

On 13-05-16 21:09 , Peter C. Chapin wrote:
> On Thu, 16 May 2013, G.B. wrote:
> 
>> On 16.05.13 15:54, Dmitry A. Kazakov wrote:
> 
>>>> I realize that equivalence of functions is a difficult concept in
>>>> general
>>> There is nothing difficult in that. A function is a set of pairs. Two
>>> sets
>>> are equal when contain same elements.
>>
>> I think the difficulty is that eq is not computable. For example,
>> if f1 and f2 are any Ada compilers, produce an algorithm that computes
>>
>>  eq(f1, f2)
>>
>> Then, proceed to finding eq of procedures computing eq.
> 
> The other problem with Dmitry's earlier suggestion is that the sets he's
> talking about could be infinite in size (at least in principle).
> Comparing infinite sets can't be done in finite time, of course,

But comparing finite descriptions (generator programs) of the sets could
perhaps be done in finite time.

> so it
> doesn't really solve the problem in the general case. This is part of
> being not computable. I believe computing the equivalence of functions
> is undecidable, but I don't have a proof off hand (maybe one could be
> looked up).

A proof seems simple enough, assuming that the set of inputs is infinite
and enumerable: if you want to decide whether f1 and f2 are equivalent,
make a program P that iteratively generates (enumerates) all possible
inputs x; computes f1(x) and f2(x); and stops if f1(x) /= f2(x). This
program P halts if and only if f1 /= f2. Since halting is undecidable,
so therefore is function equality.

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

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

[Georg Bauhaus]

On 16.05.13 21:16, Dmitry A. Kazakov wrote:
> If the
> programmer cares, he may declare operation "=" and implement it according
> to the semantics of the problem space.

The little "implement" in the preceding sentence might require
comparing functions, which again is part of a problem.

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

[Peter C. Chapin]

On Fri, 17 May 2013, Niklas Holsti wrote:

> A proof seems simple enough, assuming that the set of inputs is infinite 
> and enumerable: if you want to decide whether f1 and f2 are equivalent, 
> make a program P that iteratively generates (enumerates) all possible 
> inputs x; computes f1(x) and f2(x); and stops if f1(x) /= f2(x). This 
> program P halts if and only if f1 /= f2. Since halting is undecidable, 
> so therefore is function equality.

You've shown that the method of enumerating all possible argument values 
and testing f1(x) = f2(x) doesn't work. But perhaps there is some clever 
way to statically analyze the code of f1 and f2 to decide their 
equivalence without having to actually evaluate the functions for all 
possible inputs.

I did a quick Google search on this out of curiosity and it turns out 
there is a body of work in this area related to optimization. That makes 
sense. Optimizers would like to make transformations on a given function 
that generate provably equivalent functions (that are faster or smaller, 
etc). It's easy to see why people into optimization would care about this.

I could imagine some sort of conversation that takes a function to a kind 
of canonical form... maybe repeated applications of certain primitive 
transformations on the code... and then showing equivalence would be a 
matter of comparing the text of the canonical forms of the two functions. 
I doubt it can be done (in general), but it's not immediately obvious to 
me that it can't.

On the other hand, to prove undecidability one could use a reduction 
approach. Assume I had a Turing machine program that could take as input 
two functions (expressed also as Turing machine programs) <f1> and <f2>, 
and accept that input if the two functions are equivalent, rejecting it 
otherwise. Now show how one could transform an arbitrary instance of some 
known undecidable problem, using a Turing machine and in finite time, to 
an instance of the equivalence checking problem. If such a transformation 
could be found, the equivalence checking problem would also be undecidable 
since a solver for it would imply a solver for the original undecidable 
problem.

Niklas, your approach actually does the reduction in the wrong direction. 
You showed how one can transform an instance of the equivalence checking 
problem into an instance of the halting problem. However, that doesn't 
allow you to conclude equivalence checking is undecidable. Maybe that's 
just the wrong way to do it.

Peter

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

[Randy Brukardt]

[-- Warning: decoded text below may be mangled, UTF-8 assumed --]
[-- Attachment #1: Type: text/plain, Size: 752 bytes --]

"Yannick Duch�ne (Hibou57)" <yannick_duchene@yahoo.fr> wrote in message 
news:op.ww3ze4ejule2fv@cardamome...
>Le Tue, 14 May 2013 21:02:32 +0200, Randy Brukardt <randy@rrsoftware.com>
a �crit:
>> If the prototype implementation were to show only minor
>> incompatibilities when processing existing Ada code (including the ACATS,
>> AdaCore test suite,
>
>AdaCore test suite? If that exist, that must be not public.

Right, it's not public (I'm told it includes propriarty code of AdaCore 
customers). My point is that a prototype would have to perform well on any 
and all existing Ada code (whether it knew about it ahead of time or not) in 
order to "pass". It's not just about passing public test suites.

                            Randy.

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

[Randy Brukardt]

"Robert A Duff" <bobduff@shell01.TheWorld.com> wrote in message 
news:wcc61yl1hic.fsf@shell01.TheWorld.com...
> "Randy Brukardt" <randy@rrsoftware.com> writes:
...
>> We briefly tried that model when designing Claw, but it really didn't 
>> work,
>> because the underlying handle can be closed by some other operation and 
>> in
>> that case the object becomes closed (we called it "invalid") without any
>> explicit action in your code. For a windowing system, that other 
>> operation
>> can be the guy with the mouse, who can easily screw up all of your 
>> carefully
>> thought out code.
>
> So how does it work in CLAW?  Are you talking about some task
> writing into a window, while the user is asynchronously clicking
> on "close window"?  So that task must be constantly checking
> Is_Open (or handling an exception), and locking things to make
> sure there are no race conditions?

Practically, operations outside of "action routines" always have to be 
prepared for an operation to raise Not_Valid_Error (with appropriate 
handlers). Pretesting with Is_Valid doesn't work because it's a race 
condition (that's a mistake I made in some of my early Claw programs - I 
learned about the race conditions the hard way).

Claw does a lot of internal locking so that common operations are safe. 
Action routines (that is, call-backs from Claw that handle action in the 
GUI) lock their parameters so that they can't change state during the 
execution of the routines. That eliminates a lot of problems, but in rare 
instances cause deadlock (which tended to be reported as a bug in Claw - 
which wasted a lot of our support time early one), so we had to used timed 
locks that expire and raise a special exception (if Windows doesn't respond 
in 10 seconds, there's either a deadlock or Windows itself has crashed).

I wasn't completely satisfied with the result, but of course by then we had 
too many customers using Claw to change its basic design. GWindows took a 
different approach, essentially requiring that only a single task can use 
the GUI. I thought (and still think) that's too limiting for a language like 
Ada with first-class tasking. But it does avoid the deadlock issues.

                                               Randy.



>> Another issue is that doing that means that you are limited to Ada's 
>> scopes
>> for managing objects, which means that you're limited in how you can set 
>> up
>> and tear down structures.
>
> I think allowing to separate initialization from declaration
> can solve that.
>
>>...(You can always get around those problems by
>> essentially making your clients use new/unchecked_deallocation for
>> everything -- but I don't consider that a step forward. I'd rather have
>> "invalid" objects than force people to use access types.)
>
> Agreed -- heap allocation solves the problem, but creates other
> problems.
>
> - Bob 

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

[Niklas Holsti]

On 13-05-17 02:20 , Peter C. Chapin wrote:
> On Fri, 17 May 2013, Niklas Holsti wrote:
> 
>> A proof seems simple enough, assuming that the set of inputs is
>> infinite and enumerable: if you want to decide whether f1 and f2 are
>> equivalent, make a program P that iteratively generates (enumerates)
>> all possible inputs x; computes f1(x) and f2(x); and stops if f1(x) /=
>> f2(x). This program P halts if and only if f1 /= f2. Since halting is
>> undecidable, so therefore is function equality.
> 
> You've shown that the method of enumerating all possible argument values
> and testing f1(x) = f2(x) doesn't work.

Yes, my argument is wrong (the reduction should go the other way). I
tried to cancel my post, but too late.... sorry.

I should not try to write proofs of undecidability at one hour past
midnight.

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

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

[Georg Bauhaus]

On 17.05.13 01:20, Peter C. Chapin wrote:
> On Fri, 17 May 2013, Niklas Holsti wrote:
>
>> A proof ...


Here is one (hint?), from 0122063821 Ch 16, 4. I am abbreviating,
as I guess you academics wouldn't want to see the level of detail
and context that the authors have added for laymen like myself:

Let

  eq : N[⊥] × N[⊥] → N[⊥]

  eq(x, y) = { 1  if x = y
             { 0  if x /= y

(eq is not monotonic, compare eq(⊥, ⊥) to eq(⊥, 0).) Let Φ[⊥] be
the strict extension of the universal function Φ(x, y) (which
takes y to be a program number), let ZERO[⊥] be the strict extension
of ZERO(x) = 0.

  HALT(x, y) = eq(0, ZERO[⊥]( Φ[⊥](x, y) ))

"If ZERO[⊥] and Φ[⊥] are partially computable, then eq certainly
is not".

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

[Dmitry A. Kazakov]

On Thu, 16 May 2013 23:59:14 +0200, Georg Bauhaus wrote:

> On 16.05.13 21:16, Dmitry A. Kazakov wrote:
>> If the
>> programmer cares, he may declare operation "=" and implement it according
>> to the semantics of the problem space.
> 
> The little "implement" in the preceding sentence might require
> comparing functions, which again is part of a problem.

No more than implementing a flight control system, a database engine, an
image processing software etc.

All not the language's business, which was the point.

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