Untyped Ada?

Untyped Ada?

[Phaedrus]

It's a slow Monday, so it's time to ask non-pertinent, and possibly 
impertinent, question:

If a non-typed or weakly typed version of Ada were available, would you use 
it?

A) Never!  My code is perfect, and I never, ever have to convert types!
B) Maybe for prototypes.
C) Late at night when I thought nobody could see me.  With the curtains 
drawn.  And under an assumed name.
D) Proudly, and often, and in public!  Who cares what the neighbors think?

Cheers!
Brian

Re: Untyped Ada?

[Randy Brukardt]

"Phaedrus" <phaedrusalt@hotmail.com> wrote in message
news:q5CdnepU0ZzTxmzanZ2dnUVZ_t-nnZ2d@earthlink.com...
> If a non-typed or weakly typed version of Ada were available, would you
use
> it?

This seems like a poorly framed question. I wonder if you really mean a
"dynamically typed" version of Ada (like Python), which would be an
interesting question.

But your actual question is essentially an anything goes language (still
static, but no checking). It would be worse than C with Ada syntax, and I
can't imagine the point. Ada's compile-time checking is (one of) its
advantages over the great mass of languages - it is is not a problem in
practice.

Still, I'd never say "never" (that's silly - how do I know what I'll be
doing in 20 years?).

                         Randy.

Re: Untyped Ada?

[tmoran]

> If a non-typed or weakly typed version of Ada were available, would you use
> it?
>
> A) Never!  My code is perfect, and I never, ever have to convert types!

Never!  My code is imperfect, and Ada often points out my errors so that
I can correct them.

Re: Untyped Ada?

[Dmitry A. Kazakov]

On Mon, 31 Mar 2008 14:44:43 -0800, Phaedrus wrote:

> It's a slow Monday, so it's time to ask non-pertinent, and possibly 
> impertinent, question:
> 
> If a non-typed or weakly typed version of Ada were available, would you use 
> it?
> 
> A) Never!  My code is perfect, and I never, ever have to convert types!
> B) Maybe for prototypes.
> C) Late at night when I thought nobody could see me.  With the curtains 
> drawn.  And under an assumed name.
> D) Proudly, and often, and in public!  Who cares what the neighbors think?

Any dynamically typed system is a statically typed system where all objects
are instances of the same type which has all possible methods. So there is
no choice anyway.

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

Re: Untyped Ada?

[Jean-Pierre Rosen]

Phaedrus a �crit :
> It's a slow Monday, so it's time to ask non-pertinent, and possibly 
> impertinent, question:
> 
> If a non-typed or weakly typed version of Ada were available, would you use 
> it?
> 
There is a contradiction in the above sentence. If it is weakly typed, 
it's not Ada ;-)

-- 
---------------------------------------------------------
            J-P. Rosen (rosen@adalog.fr)
Visit Adalog's web site at http://www.adalog.fr

Re: Untyped Ada?

[Phaedrus]

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

Don't you think that semantics make for poor discussions?

Brian
"Jean-Pierre Rosen" <rosen@adalog.fr> wrote in message 
news:korssf.6gl.ln@hunter.axlog.fr...
> Phaedrus a �crit :
>> It's a slow Monday, so it's time to ask non-pertinent, and possibly 
>> impertinent, question:
>>
>> If a non-typed or weakly typed version of Ada were available, would you 
>> use it?
>>
> There is a contradiction in the above sentence. If it is weakly typed, 
> it's not Ada ;-)
>
> -- 
> ---------------------------------------------------------
>            J-P. Rosen (rosen@adalog.fr)
> Visit Adalog's web site at http://www.adalog.fr 

Re: Untyped Ada?

[Ludovic Brenta]

"Phaedrus" <phaedrusalt@hotmail.com> writes:

> Don't you think that semantics make for poor discussions?

Then let's discuss form: please, do not top-post.

-- 
Ludovic Brenta.
A: Because it messes up the order in which people normally read text.
Q: Why is top-posting such a bad thing?
A: Top-posting.
Q: What is the most annoying thing in e-mail?

Re: Untyped Ada?

[Pascal Obry]

Never, what's the point of loosing one of the most important Ada strength!

Pascal.


-- 

--|------------------------------------------------------
--| Pascal Obry                           Team-Ada Member
--| 45, rue Gabriel Peri - 78114 Magny Les Hameaux FRANCE
--|------------------------------------------------------
--|              http://www.obry.net
--| "The best way to travel is by means of imagination"
--|
--| gpg --keyserver wwwkeys.pgp.net --recv-key C1082595

Re: Untyped Ada?

[Phaedrus]

Certainly it is an important part of Ada, but I wasn't suggesting that it be 
deleted entirely.  However, it might be handy to have a less-strongly typed 
version of Ada, for instance to create prototypes faster and easier.  Then, 
aspects of the prototype could be migrated into a "fully typed" arena once 
the "quick and dirty" prototype was completed.

Just thinking a little bit outside the ol' box, here...

Brian


"Pascal Obry" <pascal@obry.net> wrote in message 
news:47F26C46.3010607@obry.net...
>
> Never, what's the point of loosing one of the most important Ada strength!
>
> Pascal.
>
>
> -- 
>
> --|------------------------------------------------------
> --| Pascal Obry                           Team-Ada Member
> --| 45, rue Gabriel Peri - 78114 Magny Les Hameaux FRANCE
> --|------------------------------------------------------
> --|              http://www.obry.net
> --| "The best way to travel is by means of imagination"
> --|
> --| gpg --keyserver wwwkeys.pgp.net --recv-key C1082595 

Re: Untyped Ada?

[Dmitry A. Kazakov]

On Tue, 1 Apr 2008 14:00:15 -0800, Phaedrus wrote:

> Certainly it is an important part of Ada, but I wasn't suggesting that it be 
> deleted entirely.  However, it might be handy to have a less-strongly typed 
> version of Ada, for instance to create prototypes faster and easier.  Then, 
> aspects of the prototype could be migrated into a "fully typed" arena once 
> the "quick and dirty" prototype was completed.

Type error is a bug. To have it undetected makes nothing quicker or easier.

As others have suggested, you are likely confusing weak typing with dynamic
[yet strong] typing. Maybe you have type inference in mind, maybe,
non-manifestedly typed systems, maybe, agile/extreme programming...

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

Re: Untyped Ada?

[Graham]

On Apr 1, 11:00 pm, "Phaedrus" <phaedrus...@hotmail.com> wrote:
> Certainly it is an important part of Ada, but I wasn't suggesting that it be
> deleted entirely.  However, it might be handy to have a less-strongly typed
> version of Ada, for instance to create prototypes faster and easier.  Then,
> aspects of the prototype could be migrated into a "fully typed" arena once
> the "quick and dirty" prototype was completed.
>
> Just thinking a little bit outside the ol' box, here...
>
> Brian
>
>

I haven't been using Ada for all that long, but I have been thinking
that a kinder, gentler version would be nice in some circumstances.
Not necessarily *no* type-checking, but the ability to mix, say,
integers, fixed-point types and floats in an equation without
cluttering up the code with conversions.

I dare say that you wouldn't want to program a missile in such a loose
way, but for the kinds of things I'm involved in - financial apps and
simulations - the level of strictness of Ada would be a turn-off for
many developers. And, from what I can see, the main problem with Ada
is its lack of take-up outside its core areas of avionics and real-
time systems.

Sorting out string handling out would be nice, too.

Graham

Re: Untyped Ada?

[Pascal Obry]

Graham,

> I dare say that you wouldn't want to program a missile in such a loose
> way, but for the kinds of things I'm involved in - financial apps and
> simulations - the level of strictness of Ada would be a turn-off for
> many developers. And, from what I can see, the main problem with Ada
> is its lack of take-up outside its core areas of avionics and real-
> time systems.

What's for? Why do you think it will help in the simulation case?

I've been in the simulation area. I've seen code in C++ where there is 
no such check... and I've found things like that:

    for (int k=0; k<MAX_VAL; k=k+0.1) { }

No kidding, this IS real code found in a real .cxx file in an important 
simulation!

Nice way of mixing integer and floating point. If you are looking for a 
language that seem attractive just to have the joy to play with a 
debugger then do not count on my vote.

Again we do not want to change things that are helping developers using 
Ada today. As many have expressed here, the string typing is a strength 
of Ada. We have seen zero convincing arguments to break this!

> Sorting out string handling out would be nice, too.

Probably something to do in this area I agree.

Pascal.

-- 

--|------------------------------------------------------
--| Pascal Obry                           Team-Ada Member
--| 45, rue Gabriel Peri - 78114 Magny Les Hameaux FRANCE
--|------------------------------------------------------
--|              http://www.obry.net
--| "The best way to travel is by means of imagination"
--|
--| gpg --keyserver wwwkeys.pgp.net --recv-key C1082595

Re: Ada.Bounded_Strings

[Adam Beneschan]

On Apr 4, 9:10 am, Pascal Obry <pas...@obry.net> wrote:

> > Sorting out string handling out would be nice, too.
>
> Probably something to do in this area I agree.

OK, this is *really* beating a dead horse, but...

When I read this and was thinking randomly about Ada's string
handling, I got to wondering why Bounded_Strings was defined as a
generic, rather than declaring a discriminated type with the maximum
length as the discriminant.  I don't know why I hadn't thought of this
before, in the last 13 years, but I figured someone else had probably
asked that, so sure enough after a bit of searching I ended up finding
the answer in the Ada 95 Rationale.  The problem is, the answer
doesn't make a whit of sense to me.

The idea was to declare a non-generic package and a Bounded_String
type that looked like:

    type Bounded_String (Max_Length : Positive) is record
        Length : Natural;
        Data   : String(1..Max_Length);
    end record;

The disadvantage of this approach was given as this: "[P]redefined
assignment and equality for discriminated Bounded_String do not have
the desired behavior.  Assignment makes sense when the maximum lengths
of source and target are different, as long as the source's current
length is no greater than the target's maximum length, yet predefined
":=" would raise Constraint_Error on the discriminant mismatch".

The reason this doesn't make sense to me is, how does the generic
definition solve the problem?  If you have two different maximum
lengths, then you have to instantiate Bounded_Strings twice to get
types with different maximum lengths; and then the Bounded_String
types are separate types and you can't do an assignment anyway.  So I
don't see why this was considered a disadvantage of the discriminant
approach.  (Plus, with a discriminant definition you could at least
write an assignment *procedure* with one OUT parameter, but you can't
do that with generics, except by defining a second generic package
that takes two instances of Bounded_Strings as formal parameters,
which would then have to be instantiated for every combination of two
lengths for which you'd want to do assignment.)

I realize I'm at least a decade too late in asking this, but in case
someone has a good memory, I was wondering if someone could explain
this to me?

And would it be useful to add a package like this now?  (I'm thinking
of this because Graham alluded to Ada's not being adopted in business
settings, and I'm wondering whether this kind of type would seem more
comfortable and familiar to COBOL-type programmers than an
Unbounded_String type.  But I'm just guessing---I really wouldn't
know.)

                                 -- thanks, Adam

Re: Ada.Strings.Bounded

[Adam Beneschan]

On Apr 4, 2:09 pm, Adam Beneschan <a...@irvine.com> wrote:
> On Apr 4, 9:10 am, Pascal Obry <pas...@obry.net> wrote:
>
> > > Sorting out string handling out would be nice, too.
>
> > Probably something to do in this area I agree.
>
> OK, this is *really* beating a dead horse, but...
>
> When I read this and was thinking randomly about Ada's string
> handling, I got to wondering why Bounded_Strings was defined as a
> generic

I got sloppy with the names, of course.  The package name is
Ada.Strings.Bounded, and the generic I'm referring to is the nested
generic package Generic_Bounded_Length.  Please imagine the
appropriate substitutions in the rest of my post.  Hopefully you can
all tell what I meant.  I guess that tells you how often I use this.

                                 -- Adam

Re: Ada.Strings.Bounded

[Gautier]

Adam Beneschan:

 > When I read this and was thinking randomly about Ada's string
 > handling, I got to wondering why Bounded_Strings was defined as a
 > generic, rather than declaring a discriminated type with the maximum
 > length as the discriminant.

Do you mean something like that ?

------------------------------------------------------------------------------
--  File:           BorString.ads
--  Description:    Variable-size, bounded strings as in early Borland Pascals
--                      Essentially for quick portability purposes.
--  Date / Version: 14-May-2001 ; 4-May-2000
--  Author:         Gautier de Montmollin
--  Portability:    Full: pure Ada 83. Nearest Ada 95+ package: the
--                  generic Ada.Strings.Bounded .
------------------------------------------------------------------------------

package BorStrings is

   type BorString( maxlength: positive ) is private;

   -- Idea: you can convert to string for _functional_ manipulations
   function To_String( b:BorString ) return String;
   -- ... then, put the result in a BorString if needed
   procedure Put( b : in out BorString; c: Character );
   procedure Put( b : in out BorString; s: String );
   procedure Put( bd: in out BorString; bs: BorString );
   -- Note: with the "&" concatenators defined below, you can do it
   -- straigthforward !

   -- * Procedures and functions that are in Turbo Pascal and later:
   --     Concat   Copy   Delete   Insert   Length   Pos
   -- * We add RPos for searching a string from the _right_

   --        Concat: use the "&" operator instead! NB: TP has "+"
   function  Copy(b: BorString; index: Integer; count: Integer) return String;
   procedure Delete( b: in out BorString; index: Positive; count: Positive);
   procedure Insert( source: String; b: in out BorString; index: Integer);
   procedure Insert( source: BorString; b: in out BorString; index: Integer);
   function  Length( b: BorString ) return Natural;
   function  Pos( substr: String; b: BorString) return Natural;
   function  RPos( substr: String; b: BorString) return Natural;

   -- "&" operators returning a BorString of _same_ maxlength as the input
   -- so you can write  b:= b & " "  or b:= "[" & b & "]" !

   function  "&" ( c: Character; b: BorString) return BorString;
   function  "&" ( s: String; b: BorString) return BorString;
   function  "&" ( b: BorString; c: Character) return BorString;
   function  "&" ( b: BorString; s: String) return BorString;

   -- same, returning strings (experimental: can cause ambiguities)

   function  "&" ( c: Character; b: BorString) return String;
   function  "&" ( s: String; b: BorString) return String;
   function  "&" ( b: BorString; c: Character) return String;
   function  "&" ( b: BorString; s: String) return String;

   function Eq ( b1,b2: BorString ) return Boolean;
   function Eq ( b1: BorString; s2: String ) return Boolean;

   string_overflow: exception;

   pragma Inline(To_String);

private
   type BorString( maxlength: positive ) is record
     length: Natural:= 0;
     s: String( 1..maxlength );
   end record;
   -- NB: length allows longer strings than the "s[0]" in T/B-Pascal

end BorStrings;

______________________________________________________________
Gautier         -- http://www.mysunrise.ch/users/gdm/index.htm
Ada programming -- http://www.mysunrise.ch/users/gdm/gsoft.htm

NB: For a direct answer, e-mail address on the Web site!

Re: Ada.Strings.Bounded

[Pascal Obry]

Gautier,

> Do you mean something like that ?

No quite as:

    B1 : BorString (10);
    B2 : BorString (20);

    B1 := B2;
    --  will raises constraint error

With Unbounded_String we are close to something "usable".

    U1 : Unbounded_String;
    U2 : Unbounded_String;

    U1 := U2;

Works fine! But then it becomes a bit messy when converting back and 
forth with the string type.

    U1 := To_Unbounded_String ("whatever");

    Put_Line (To_String (U1));

Not a big deal, but if we can find a nice way to tell that such routine 
must be used for conversion between type it will be quite handy.

    type Unbounded_String is ...;

    function To_String (U : Unbounded_String) return String;

    for Unbounded_String'Conversion (String) use To_String;

Just to get the idea, then one could write:

    Put_Line (U1);

Of course this raises some questions:

    What to do if we have Put_Line defined for String and
    Unbounded_String? Which version gets called?

...

Anyway that's just some wild thoughts :)

Pascal.

-- 

--|------------------------------------------------------
--| Pascal Obry                           Team-Ada Member
--| 45, rue Gabriel Peri - 78114 Magny Les Hameaux FRANCE
--|------------------------------------------------------
--|              http://www.obry.net
--| "The best way to travel is by means of imagination"
--|
--| gpg --keyserver wwwkeys.pgp.net --recv-key C1082595

Re: Ada.Strings.Bounded

[Dmitry A. Kazakov]

On Sat, 05 Apr 2008 11:43:39 +0200, Pascal Obry wrote:

> Works fine! But then it becomes a bit messy when converting back and 
> forth with the string type.
> 
>     U1 := To_Unbounded_String ("whatever");
> 
>     Put_Line (To_String (U1));
> 
> Not a big deal, but if we can find a nice way to tell that such routine 
> must be used for conversion between type it will be quite handy.
> 
>     type Unbounded_String is ...;
> 
>     function To_String (U : Unbounded_String) return String;
> 
>     for Unbounded_String'Conversion (String) use To_String;

No, that would be a can of worms. Arbitrary type conversions automatically
applied is a mess. Below you immediately spot the problem of conversions
preferences. Because conversions are arbitrary, there is no any order
defined on the types to make a choice.

What is actually needed is to say that Unbounded_String is a member of
String'Class and you wanted to inherit everything form String.

The implementation of inheritance (by the compiler) will require you to
provide two *private* conversion functions when the types are untagged.
Note that you need two conversions: a forward conversion for in-parameters
and a backward conversion for out-ones. In out parameters will use both
(copy-in, copy-out).

For tagged [actually, by-reference] types the compiler can generate
conversions because they are necessarily view conversions.

> Just to get the idea, then one could write:
> 
>     Put_Line (U1);
> 
> Of course this raises some questions:
> 
>     What to do if we have Put_Line defined for String and
>     Unbounded_String? Which version gets called?

It will one of Unbounded_String, because that will be an override.

Note though, that Put_Line (File, String) will open further questions. Is
it primitive in File or in String? Clearly it should be in both. This is
how multiple dispatch issue comes in.

> Anyway that's just some wild thoughts :)

It is not wild, it is how Ada types system should be completed.

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

Re: Ada.Strings.Bounded

[Gautier]

Pascal Obry wrote:

...
> With Unbounded_String we are close to something "usable".

That's clear. I think Adam's question was really specific to the bounded 
strings. Unbounded_String is the most comfortable and the safest, but needs 
dynamic allocation behind the scenes, which can be a handicap on some special 
situations (performance-critical, systems without dynamic allocation,...).

>    U1 : Unbounded_String;
>    U2 : Unbounded_String;
> 
>    U1 := U2;
> 
> Works fine! But then it becomes a bit messy when converting back and 
> forth with the string type.
> 
>    U1 := To_Unbounded_String ("whatever");
> 
>    Put_Line (To_String (U1));
> 
> Not a big deal, but if we can find a nice way to tell that such routine 
> must be used for conversion between type it will be quite handy.
> 
>    type Unbounded_String is ...;
> 
>    function To_String (U : Unbounded_String) return String;
> 
>    for Unbounded_String'Conversion (String) use To_String;
> 
> Just to get the idea, then one could write:
> 
>    Put_Line (U1);
> 
> Of course this raises some questions:
> 
>    What to do if we have Put_Line defined for String and
>    Unbounded_String? Which version gets called?
> 
> ...
> 
> Anyway that's just some wild thoughts :)

I agree with Dmitry that it would lead to confusing situations, something that 
Ada normally tries to avoid...
What I'm doing to make life easier is to paste the following lines in my sources

   function S (Source : Ada.Strings.Unbounded.Unbounded_String) return String
     renames Ada.Strings.Unbounded.To_String;
   function U (Source : String) return Ada.Strings.Unbounded.Unbounded_String
     renames Ada.Strings.Unbounded.To_Unbounded_String;

After the sources only need short S(...)'s and U(...)'s which are ok to me:

   external_packer: array(External) of Unbounded_String:=
     ( U("zip.exe"),
       U("7z.exe"),
       U("kzip.exe")
     );
...
   return "External: " & S(external_title(a)) & ", " & S(external_options(a));
...
       e.name:= U(unique_name);
..., etc. etc.
______________________________________________________________
Gautier         -- http://www.mysunrise.ch/users/gdm/index.htm
Ada programming -- http://www.mysunrise.ch/users/gdm/gsoft.htm

NB: For a direct answer, e-mail address on the Web site!

Re: Ada.Strings.Bounded

[Pascal Obry]

Gautier,

>   function S (Source : Ada.Strings.Unbounded.Unbounded_String) return 
> String
>     renames Ada.Strings.Unbounded.To_String;
>   function U (Source : String) return 
> Ada.Strings.Unbounded.Unbounded_String
>     renames Ada.Strings.Unbounded.To_Unbounded_String;

I'm doing the same with operator "+" and "-", but I'm not happy with 
that. You do not need the parenthesis with operators:

   external_packer: array(External) of Unbounded_String:=
     ( +"zip.exe",
       +"7z.exe",
       +"kzip.exe");

Better than nothing...

Pascal.

-- 

--|------------------------------------------------------
--| Pascal Obry                           Team-Ada Member
--| 45, rue Gabriel Peri - 78114 Magny Les Hameaux FRANCE
--|------------------------------------------------------
--|              http://www.obry.net
--| "The best way to travel is by means of imagination"
--|
--| gpg --keyserver wwwkeys.pgp.net --recv-key C1082595

Re: Ada.Strings.Bounded

[Randy Brukardt]

"Pascal Obry" <pascal@obry.net> wrote in message
news:47F76D31.2090009@obry.net...
> Gautier,
>
> >   function S (Source : Ada.Strings.Unbounded.Unbounded_String) return
> > String
> >     renames Ada.Strings.Unbounded.To_String;
> >   function U (Source : String) return
> > Ada.Strings.Unbounded.Unbounded_String
> >     renames Ada.Strings.Unbounded.To_Unbounded_String;
>
> I'm doing the same with operator "+" and "-", but I'm not happy with
> that. You do not need the parenthesis with operators:

The only useful use for "+" in Ada is for conversions. So it is a common
convention (I use it sometimes). We actually considered adding that rename
to the strings packages, but enough people thought it was ugly that it
wasn't done. (It needs getting used to, thus the hope of making the intent
clearer by including it in the packages.)

We also briefly considered adding an operator symbol specifically for this
purpose. Something like
   function "#" (Source : String) return Unbounded_String;
But the people who don't think "+" is ugly were against this, because we
already have such an operator and thus don't need another one. Thus a
deadlock. Sigh.

>    external_packer: array(External) of Unbounded_String:=
>      ( +"zip.exe",
>        +"7z.exe",
>        +"kzip.exe");
>
> Better than nothing...

I agree, and it doesn't look so ugly if you can think of unary "+" as the
conversion operator. (Personally, I'd prefer a different symbol for this
purpose, but "+" has the advantage of actually working now.)

                               Randy.

Re: Ada.Strings.Bounded

[Adam Beneschan]

On Apr 5, 5:31 pm, "Randy Brukardt" <ra...@rrsoftware.com> wrote:
> "Pascal Obry" <pas...@obry.net> wrote in message
>
> news:47F76D31.2090009@obry.net...
>
> > Gautier,
>
> > >   function S (Source : Ada.Strings.Unbounded.Unbounded_String) return
> > > String
> > >     renames Ada.Strings.Unbounded.To_String;
> > >   function U (Source : String) return
> > > Ada.Strings.Unbounded.Unbounded_String
> > >     renames Ada.Strings.Unbounded.To_Unbounded_String;
>
> > I'm doing the same with operator "+" and "-", but I'm not happy with
> > that. You do not need the parenthesis with operators:
>
> The only useful use for "+" in Ada is for conversions.

Well, I can think of one other potentially useful use: with a numeric
argument (especially a numeric literal, or something like pi).  It
doesn't have any effect but could serve to make things clearer in some
mathematical cases.  Maybe you'd call a bounded integration routine
with +1.0 and -1.0 as the arguments.

OK, so that's not much of a use.  On the other hand, the idea that "+"
represents the identity function is ingrained enough in me that I've
resisted using it for a conversion operator even though others around
me have been doing that.  Call it an obstinate adherence to
meaningless purity or whatever.  But like Randy, I would have
preferred adding one (maybe even two) operator symbols that would have
no meaning except that the user could define them, although I'm not
sure about "#" since that already has a use (in based numeric
literals).  I'd prefer something not currently used at all, like "@"
or "!" or tilde.  Of course, it apparently isn't going to happen
anyway so there's not much point arguing about which character would
be best.

                               -- Adam

Re: Ada.Strings.Bounded

[Dmitry A. Kazakov]

On Mon, 7 Apr 2008 07:57:55 -0700 (PDT), Adam Beneschan wrote:

> But like Randy, I would have
> preferred adding one (maybe even two) operator symbols that would have
> no meaning except that the user could define them, although I'm not
> sure about "#" since that already has a use (in based numeric
> literals).  I'd prefer something not currently used at all, like "@"
> or "!" or tilde.

May I suggest Unicode Character 'NO-BREAK SPACE' (U+00A0)?

Sorry, just could not resist (:-))

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

Re: Ada.Strings.Bounded

[stefan-lucks]

> > The only useful use for "+" in Ada is for conversions.
> 
> OK, so that's not much of a use.  On the other hand, the idea that "+"
> represents the identity function is ingrained enough in me that I've
> resisted using it for a conversion operator even though others around
> me have been doing that.  Call it an obstinate adherence to
> meaningless purity or whatever.  But like Randy, I would have
> preferred adding one (maybe even two) operator symbols that would have
> no meaning except that the user could define them, although I'm not
> sure about "#" since that already has a use (in based numeric
> literals).  I'd prefer something not currently used at all, like "@"
> or "!" or tilde.  Of course, it apparently isn't going to happen
> anyway so there's not much point arguing about which character would
> be best.

Two natural candidates which come into my mind would be an unary '&' and 
the '%'-sign:

  '%' (percent) indicates some kind of conversion anyway (though usually 
      in postfix notation, not as a prefix, "75 %" for 75/100). 

  '&' is something you can even now use for conversion into strings and 
      the like:
        declare an appropriate function 
            function "&" (X: String; Y: Some_Type) return String;
        and then just write 
	    "" & A;
        wherever you need A being converted into a string. 
      A unary "&" would be handy -- prepending the empty string clearly is 
      artificial. 

So long

Stefan

-- 
------ Stefan Lucks   --  Bauhaus-University Weimar  --   Germany  ------
               Stefan dot Lucks at uni minus weimar dot de
------  I  love  the  taste  of  Cryptanalysis  in  the  morning!  ------

Re: Ada.Strings.Bounded

[(see below)]

On 07/04/2008 17:34, in article
Pine.LNX.4.64.0804071812200.15920@medsec1.medien.uni-weimar.de,
"stefan-lucks@see-the.signature" <stefan-lucks@see-the.signature> wrote:

>>> The only useful use for "+" in Ada is for conversions.
>> 
>> OK, so that's not much of a use.  On the other hand, the idea that "+"
>> represents the identity function is ingrained enough in me that I've
>> resisted using it for a conversion operator even though others around
>> me have been doing that.  Call it an obstinate adherence to
>> meaningless purity or whatever.  But like Randy, I would have
>> preferred adding one (maybe even two) operator symbols that would have
>> no meaning except that the user could define them, although I'm not
>> sure about "#" since that already has a use (in based numeric
>> literals).  I'd prefer something not currently used at all, like "@"
>> or "!" or tilde.  Of course, it apparently isn't going to happen
>> anyway so there's not much point arguing about which character would
>> be best.
> 
> Two natural candidates which come into my mind would be an unary '&' and
> the '%'-sign:
> 
>   '%' (percent) indicates some kind of conversion anyway (though usually
>       in postfix notation, not as a prefix, "75 %" for 75/100).

Potential problems there with string literals (see RM: J.2 Allowed
Replacements of Characters)?

-- 
Bill Findlay
<surname><forename> chez blueyonder.co.uk

Re: Ada.Strings.Bounded

[Eric Hughes]

On Apr 5, 3:43 am, Pascal Obry <pas...@obry.net> wrote:
>     What to do if we have Put_Line defined for String and
>     Unbounded_String? Which version gets called?

I know this answer is a bit heretical, but the answer I'd pick is
"either one".  Non-deterministic execution, if you'd like the
technical term.  Which in practice means that the compiler can pick a
deterministic path and just use that one.

The reason for this is that String and Unbounded_String are not
arbitrarily related in conception.  Ada, as presently constituted, is
unable of representing the details of this relationship.  Users of
these types know what they're supposed to do, but the language does
not capture this.  A correct implementation of Put_Line should have
the property that the result of Put_Line on a String is the same as
the result of Put_Line on an Unbounded_String converted from the same
String.  This is the substance of algebraic specification.  So,
assuming (contrary to fact) such a specification, it should not matter
for correctness which version executed.

It would affect performance, true.  But it's performance about
symbolic manipulations (in the representation of the type) with
symbols that do not appear in the language itself.  Since these
symbols do not appear in the definition of String, it's the wrong path
to try to specify performance choices _at this level of abstraction_.
Some form of (expanded) representation clause is the right place to do
this.  Representation clauses are the natural way in Ada to specify
implementation choices.

Back the larger type issue, the ARM contains the types
universal_integer, universal_real, universal_fixed; these are listed
as predefined in ARM 3.2.1/10.  (Erratum: not all the predefined types
are listed here.)  I find it droll that the term "predefined" is not
defined.  It doesn't need to be, really, though.  "Everybody knows"
what numbers are supposed to do.  The axioms of arithmetic are well-
known, even if all the ordinary numbers of mathematics are
unimplementable on computers (only bounded-length representations are,
even if the bound is indefinite).

I believe many of the issues involving strings could be addressed by
introducing a predefined type universal_string.  And then the hard
part: making everything work out right.  _Inter alia_, all conversions
between string types would have to preserve the underlying
universal_string value.  I would raise Length_Error if a silent
truncation were to occur, under the theory that truncation is an
operation on values (as distinguished from objects and variables) that
should *never* be made silently.  And having universal_string should
eliminate most of those unary conversion operators to move between
different string types.

As not-too-much of an aside, this is why the ordinary Strings package
is fatally flawed, because its padding manipulations are just NOT how
universal_string values act.  Padding is a bastard child of an
implementation choice (fixed length array) and a discrimination
between characters that matter and the padding character, which
doesn't.  That package should really be named Padded_Strings.

Now, my real hope is that universal_string wouldn't need to be
predefined at all, but specified algebraically or logically within a
future version of Ada.  But for now the next step is to start with a
predefined type.

Eric

Re: Ada.Strings.Bounded

[Georg Bauhaus]

Eric Hughes wrote:
> On Apr 5, 3:43 am, Pascal Obry <pas...@obry.net> wrote:
>>     What to do if we have Put_Line defined for String and
>>     Unbounded_String? Which version gets called?
> 
> I know this answer is a bit heretical, but the answer I'd pick is
> "either one".  Non-deterministic execution, if you'd like the
> technical term.  Which in practice means that the compiler can pick a
> deterministic path and just use that one.
> 
> The reason for this is that String and Unbounded_String are not
> arbitrarily related in conception.  Ada, as presently constituted, is
> unable of representing the details of this relationship.  Users of
> these types know what they're supposed to do, but the language does
> not capture this.  A correct implementation of Put_Line should have
> the property that the result of Put_Line on a String is the same as
> the result of Put_Line on an Unbounded_String converted from the same
> String.  This is the substance of algebraic specification.  So,
> assuming (contrary to fact) such a specification, it should not matter
> for correctness which version executed.
> 
> It would affect performance, true.  But it's performance about
> symbolic manipulations (in the representation of the type) with
> symbols that do not appear in the language itself.  Since these
> symbols do not appear in the definition of String, it's the wrong path
> to try to specify performance choices _at this level of abstraction_.
> Some form of (expanded) representation clause is the right place to do
> this.  Representation clauses are the natural way in Ada to specify
> implementation choices.
> 
> Back the larger type issue, the ARM contains the types
> universal_integer, universal_real, universal_fixed; these are listed
> as predefined in ARM 3.2.1/10.  (Erratum: not all the predefined types
> are listed here.)  I find it droll that the term "predefined" is not
> defined.  It doesn't need to be, really, though.  "Everybody knows"
> what numbers are supposed to do.  The axioms of arithmetic are well-
> known, even if all the ordinary numbers of mathematics are
> unimplementable on computers (only bounded-length representations are,
> even if the bound is indefinite).
> 
> I believe many of the issues involving strings could be addressed by
> introducing a predefined type universal_string.  And then the hard
> part: making everything work out right.  _Inter alia_, all conversions
> between string types would have to preserve the underlying
> universal_string value.  I would raise Length_Error if a silent
> truncation were to occur, under the theory that truncation is an
> operation on values (as distinguished from objects and variables) that
> should *never* be made silently.  And having universal_string should
> eliminate most of those unary conversion operators to move between
> different string types.

The fixed String is an array, a basic and central piece of Ada.
Unbounded_String is not an array.

Both types use the word "string" in their name, which is
unfortunate.  They are two very different constructions.
We can use Unbounded_String objects in ways that
are not available with strings: they are lists rather
than fixed arrays.

Seen from this point of view, a more general question is,
do we have standard ways of converting between arrays and lists?
Should these conversions be captured by some "predefined" notion
of universal_array? (Maybe you will find ideas by Dmitry Kazakov
instructive.)

Unfortunately, programming always deals with storage, memory,
and times, in particular when a systems programming language
like Ada is used, and when credit is given to the fact that
programs mean operations of a computer with storage cells,
instructions, and clock ticks. I can imagine values of some
underlying universal_array as part of a nice clean
ivory tower model of mathematical reductionism. Nasty real
world computers ;)

The APL world is different and offers another hint. Maybe
Ada fixed Strings let us think they somehow must have one
dimension, but not 2, 3, or N. Why?
And should universal_array be made capable enough to convert
arrays to lists and vice versa per dimension?

Re: Ada.Strings.Bounded

[Eric Hughes]

On Apr 12, 1:46 pm, Georg Bauhaus <rm.tsoh.plus-
bug.bauh...@maps.futureapps.de> wrote:
> The fixed String is an array, a basic and central piece of Ada.
> Unbounded_String is not an array.

Sure, you can have your array; I have no issue at all with that.  But
Ada.Strings.String is just not a string, not in the way it does
padding, not in its absence of concatenation.

> Both types use the word "string" in their name, which is
> unfortunate.

I consider it more than unfortunate.  I consider it just plain wrong.


> Seen from this point of view, a more general question is,
> do we have standard ways of converting between arrays and lists?
> Should these conversions be captured by some "predefined" notion
> of universal_array?

No.  But this answer is one that hinges on the specifics of the
question, not on generalities.  Arrays have a fixed number of
elements; lists do not.  This is more than a matter of
implementation.  It's a question of specification.

Now these two types do share the property that they are indexable.  A
proper set of universal declarations should be able to capture this
similarity.  This requires a partial specification, in my view, and
that subject is beyond the scope of this message, except to say that
partial specifications and universal types are orthogonal concepts.

Hidden in your question, though, is another issue.  I don't believe
that conversions should be automatic.  I believe they should be
explicitly declared and explicitly defined.

> Unfortunately, programming always deals with storage, memory,
> and times, in particular when a systems programming language
> like Ada is used, and when credit is given to the fact that
> programs mean operations of a computer with storage cells,
> instructions, and clock ticks. I can imagine values of some
> underlying universal_array as part of a nice clean
> ivory tower model of mathematical reductionism. Nasty real
> world computers ;)

There's a pattern in dealing with this issue that deserves
standardization with respect to universal types.
   -- When return is ordinary, then the result adheres to the
universal definition.
   -- When return is exceptional, then there is no requirement that
there's any adherence.
Thus exceptions kick you out of the mathematical assumptions into the
real world, and they do so in a reasonably controlled way.

Eric

Re: Ada.Strings.Bounded

[Robert A Duff]

Eric Hughes <eric.eh9@gmail.com> writes:

> On Apr 12, 1:46 pm, Georg Bauhaus <rm.tsoh.plus-
> bug.bauh...@maps.futureapps.de> wrote:
>> The fixed String is an array, a basic and central piece of Ada.
>> Unbounded_String is not an array.
>
> Sure, you can have your array; I have no issue at all with that.  But
> Ada.Strings.String is just not a string, not in the way it does
> padding, not in its absence of concatenation.

There is no such thing as Ada.Strings.String.  I thought maybe you meant
the package Ada.Strings.Fixed, but that package has no type.  It uses
the predefined type String (which is declared in Standard, and
therefore visible everywhere), and it _does_ have concatenation ops.
So I don't understand what you mean.

I agree that blank-padding is a nearly useless thing to do.
But you can do a lot with fixed-length strings, so long
as you program them in a mostly-functional style.

>> Both types use the word "string" in their name, which is
>> unfortunate.
>
> I consider it more than unfortunate.  I consider it just plain wrong.

String and Unbounded_String are both strings of characters,
so I don't see why it's "plain wrong".  It might be better
to call them Fixed_String and String, I suppose -- the
reason for the names is historical (String predates Unbounded_String).

Adding some (near-useless) operations on String that do blank-padding
doesn't suddenly make String not a string type.

- Bob

Re: Ada.Strings.Bounded

[Eric Hughes]

On Apr 13, 2:10 pm, Robert A Duff <bobd...@shell01.TheWorld.com>
wrote:
> There is no such thing as Ada.Strings.String.  I thought maybe you meant
> the package Ada.Strings.Fixed, but that package has no type.  It uses
> the predefined type String (which is declared in Standard, and
> therefore visible everywhere), and it _does_ have concatenation ops.
> So I don't understand what you mean.

I meant .Fixed and I meant the regular String type.  And I forgot that
concatenation isn't declared.  Blah.  Sorry for generating confusion.
For my own part, I only use String for string literals.

> I agree that blank-padding is a nearly useless thing to do.
> But you can do a lot with fixed-length strings, so long
> as you program them in a mostly-functional style.

I'm not denying any of that.  My critique is pretty much solely about
names.

> String and Unbounded_String are both strings of characters,
> so I don't see why it's "plain wrong". [...]
> Adding some (near-useless) operations on String that do blank-padding
> doesn't suddenly make String not a string type.

No, but it does create a violation of axioms that define
universal_string.  Such axioms are essentially those of a semigroup
with the trivial inverse operation where only the empty string has an
inverse.  (Perhaps we might also say "maximally non-invertible
semigroup".  )  You start adding padding manipulations in there and
these axioms are no longer true.

Speaking formally, which I was trying to do (but failing in the
details), almost-a-string is a subset of not-a-string.  Axiom
satisfaction has sharp boundaries that don't usually coincide with
ordinary conceptual boundaries.  Informally, sure, they're both
strings.  But the Ada String type, with its padding, does not satisfy
the axioms of universal_string.  The problem is that it's a fixed
array, not a fixed array allocation with a variable length like
Bounded_String.  If I assign the value "A", a String of length 1, to a
String(2), the length of its value as a universal_string changes from
1 to 2.  So even simple assignment violates the axioms.

I'm not denying that having an informally-a-string type which is a
fixed-length array is useful and efficient.  It's just not a possible
implementation of universal_string.  And it's not like you can't
interconvert, but you should probably not do so silently, because
you're not satisfying a set of common axioms.

The problem that was the nexus of the original discussion is that
string literals are of type String and not deemed elements of
universal_string.

There's a second problem, one of usability, that the default string
type ought to be Unbounded_String, because it's closest to
universal_string and would create the fewest surprises (manifested in
exceptions raised).  That's really another discussion, though.

Eric

Re: Ada.Strings.Bounded

[Dmitry A. Kazakov]

On Sun, 13 Apr 2008 16:52:00 -0700 (PDT), Eric Hughes wrote:

> Speaking formally, which I was trying to do (but failing in the
> details), almost-a-string is a subset of not-a-string.  Axiom
> satisfaction has sharp boundaries that don't usually coincide with
> ordinary conceptual boundaries.  Informally, sure, they're both
> strings.  But the Ada String type, with its padding, does not satisfy
> the axioms of universal_string.  The problem is that it's a fixed
> array, not a fixed array allocation with a variable length like
> Bounded_String.  If I assign the value "A", a String of length 1, to a
> String(2), the length of its value as a universal_string changes from
> 1 to 2.  So even simple assignment violates the axioms.

If we had universal_string, it would have no assignment anyway, because all
universal objects are immutable.

There is a difference between types and their constrained subtypes in terms
of substitutability. That's why the language has Constraint_Error defined.
The contracts extended by Constraint_Error aren't violated and everything
is fine.

> The problem that was the nexus of the original discussion is that
> string literals are of type String and not deemed elements of
> universal_string.

I don't see any harm here. You cannot assign literals.

BTW, there are funny language rules which prevent things like this:

   type Integer is range -5..5;  -- On some tiny machine

   L : constant := ("abcd" & "defg"  & "defg")'Length / 3;
       -- Illegal anyway

So you cannot exploit the limitation of the string index being Positive in
order to construct strings longer than the index at compile time.

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

Re: Ada.Strings.Bounded

[Eric Hughes]

On Apr 14, 2:00 am, "Dmitry A. Kazakov" <mail...@dmitry-kazakov.de>
wrote:
> If we had universal_string, it would have no assignment anyway, because all
> universal objects are immutable.

Sure, because you can't declare a variable of a universal type.  But
this critique misses the point, which is about the relationship of
types that partially implement a universal type.

> There is a difference between types and their constrained subtypes in terms
> of substitutability. That's why the language has Constraint_Error defined.
> The contracts extended by Constraint_Error aren't violated and everything
> is fine.

Sure, but again not the point.  The relationship between a universal
type and an implemented type is NOT the same as that between two
implemented types.

Eric

Re: Ada.Strings.Bounded

[Dmitry A. Kazakov]

On Mon, 14 Apr 2008 08:25:41 -0700 (PDT), Eric Hughes wrote:

> On Apr 14, 2:00 am, "Dmitry A. Kazakov" <mail...@dmitry-kazakov.de>
> wrote:

>> There is a difference between types and their constrained subtypes in terms
>> of substitutability. That's why the language has Constraint_Error defined.
>> The contracts extended by Constraint_Error aren't violated and everything
>> is fine.
> 
> Sure, but again not the point.  The relationship between a universal
> type and an implemented type is NOT the same as that between two
> implemented types.

Certainly, but I don't see why should we care about an non-implemented
type. Well, an application dealing with mathematical objects might be
interesting in modeling N, but it is not the language concern. The same way
as Ada does not care about types of organic molecules...

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

Re: Ada.Strings.Bounded

[Eric Hughes]

On Apr 14, 12:36 pm, "Dmitry A. Kazakov" <mail...@dmitry-kazakov.de>
wrote:
> Certainly, but I don't see why should we care about an non-implemented
> type.

Because they make better tools of thought.  Assuming a prospective "-
oid" morphism, universal types provide one half of a type
description.  Representation issues, such as number of bits in an
integer, become an orthogonal issue.  Separation of concerns is
something Ada got right uniquely among programming languages, but
there remain other kinds of concerns yet to separate.

Eric

Re: Ada.Strings.Bounded

[Dmitry A. Kazakov]

On Sat, 12 Apr 2008 11:50:56 -0700 (PDT), Eric Hughes wrote:

> I believe many of the issues involving strings could be addressed by
> introducing a predefined type universal_string.

I don't see it this way. You have mentioned universal_integer, which is
already here. So a comparable case would be Integer vs. BigNum. The latter
(arbitrary-precision arithmetic) plays same role for integers as
Unbounded_String does for strings. Now, if ARM had BigNum defined, we would
experience exactly same problems with both, as we have with Strings and
Unbounded_String.

> Now, my real hope is that universal_string wouldn't need to be
> predefined at all, but specified algebraically or logically within a
> future version of Ada.

I can only agree with that.

But note, that in order to do so, you will need slices, indices and sets of
indices (ranges is an example of) defined algebraically as well. Presently
Ada lacks them.

The bottom line, instead of patching it here and there, the language type
system should be redesigned. Hacks need to be replaced by sound
concepts.[*]  Unfortunately Ada community has little interest in that.

----------
* By this I don't mean backward incompatibility. Actually it is the hacks,
which are responsible for most of incompatibilities, as they tend to
introduce strange syntax, new reserved words and confusing semantics. 

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

Re: Ada.Strings.Bounded

[Eric Hughes]

On Apr 12, 3:09 pm, "Dmitry A. Kazakov" <mail...@dmitry-kazakov.de>
wrote:
> So a comparable case would be Integer vs. BigNum. The latter
> (arbitrary-precision arithmetic) plays same role for integers as
> Unbounded_String does for strings. Now, if ARM had BigNum defined, we would
> experience exactly same problems with both, as we have with Strings and
> Unbounded_String.

Well, yes; that's a good second example, although let's call it
Unbounded_Integer.  The mechanisms are identical for dealing with
universal_string/String/Unbounded_String and univeral_integer/Integer/
Unbounded_Integer.  In the first case we have (0=absent,1=present)
0/1/1 and in the second we have 1/1/0.  In the first case we have
endless type conversions to do ordinary work.  In the second we have
an absence in the standard.


On Sat, 12 Apr 2008 11:50:56 -0700 (PDT), Eric Hughes wrote:
> I believe many of the issues involving strings could be addressed by
> introducing a predefined type universal_string.

On Apr 12, 3:09 pm, "Dmitry A. Kazakov" <mail...@dmitry-kazakov.de>
wrote:
> I don't see it this way.

I have a strong counterclaim--I don't think it can be solved without
introducing such a type.

Here's the real rub: universal_integer and universal_string are each
_unimplementable_ as executable types.  As abstract mathematical
types, they're perfectly well-defined.  The origin of the difference
is that universal types have no possible bound in size.  Since every
computer type has such a bound, there's a fundamental disjunct between
these two.  An unbounded type actually does have a bound--it throws an
exception when its internal bounds are exceeded.  A hypothetical
implementation of a universal type would be unable *in principle* to
throw such an exception.  This is clearly contrary to fact, where
every program can run out of memory.

If this sounds like my idea for partial type specification (one
without code), it should.  These ideas come from the same perspective.

There's no concept (except _ad hoc_ in the ARM) of what a universal,
unimplementable type is; there's certainly no way of declaring one.
So here's the very beginning of a proposal.  To declare and define
such a type:

    universal_type_definition ::= *universal* *type*
defining_identifier [known_discriminant_part] *;*

Notice the absence of the keyword "is".  Also notice that the
declaration and definition are the same.  The point is that a
universal type _is not_ anything insofar as record declaration or
anything else that might act as a representation.  A universal type
can not have a representation (not just "may not").  If it had a
representation, it would not be universal.  This is not merely a
practicality; this is categorical.

Now like other types, you could declare operations on universal
types.  But every such operation would also be unimplementable, so
they're declaration-only.  They cannot be defined, since there's no
representation to work with.

As with an interface, an ordinary type T could derive from a universal
type U.  It could override operations from the universal type.  But
since U has no implementation, such a derivation has no effect on the
representation of T.  The result of overriding would be to bind both
the syntax and semantics of U to that of T.  With only a single such
T, an overriding declaration would be meaningless and of no effect.
With two such declarations, however, the benefits begin.  The meaning
of such a pair of declarations says that the semantics of the two
operations are identical when values of one type are substituted for
that of the other _when those values are considered as universal
values_ (and thus not as represented values within an implementation).

With such a syntax, you obtain the ability to make a well-formed
formula with clearly defined semantics.  It says nothing about
compilation.  I consider this an advantage, as it is the essence of
separate compilation.  Getting to an unambiguous expression is the
first step.

Now, about compilation, a formula with well-defined semantics does not
(in general) have well-defined pragmatics.  The formula itself does
not specify how long execution should take, what functions must be
called, etc.  All the formula as such says is what the results should
be.  A simple example:

   universal type U ;
   function op( U Object ) return U ;
   type T1 is private and U ;
   type T2 is private and U ;
   overriding function op( T1 Object ) return T1 ;
   overriding function op( T2 Object ) return T2 ;
   function U( T2 Object ) return T1 ;
   T2 x ;
   T1 y1 := T1.op( U( x ) ) ;
   T1 y2 := U( T2.op( x ) ) ;
   T1 y := x.op ;

The expressions for y1 and y2 should be interchangeable as
implementations for the expression for y.  The point of the
declarations is to give unambiguous semantics to the expression
"x.op", so that it does not matter to the correctness of the program
what implementation expression the compiler chooses.  If Usenet had
better formatting, I'd draw a commutative diagram as an illustration.

There's special meaning behind the conversion function U.  Its
mandatory semantics is to convert an object of T2 to one of T1, such
that their values are equal as universal values.

Eric

Re: Ada.Strings.Bounded

[Robert A Duff]

Eric Hughes <eric.eh9@gmail.com> writes:

> On Apr 12, 3:09 pm, "Dmitry A. Kazakov" <mail...@dmitry-kazakov.de>
> wrote:
>> So a comparable case would be Integer vs. BigNum. The latter
>> (arbitrary-precision arithmetic) plays same role for integers as
>> Unbounded_String does for strings.

The analogy is not perfect.  You can create arbitrarily large strings
(within the limits of available memory, and the bounds of Integer,
which is pretty big).  It's just that any particular string object
cannot change length.  Integers are much more restricted -- you can't
create an integer bigger than some implementation-defined limit,
such as 32 or 64 bits.

>...Now, if ARM had BigNum defined, we would
>> experience exactly same problems with both, as we have with Strings and
>> Unbounded_String.
>
> Well, yes; that's a good second example, although let's call it
> Unbounded_Integer.  The mechanisms are identical for dealing with
> universal_string/String/Unbounded_String and univeral_integer/Integer/
> Unbounded_Integer.  In the first case we have (0=absent,1=present)
> 0/1/1 and in the second we have 1/1/0.  In the first case we have
> endless type conversions to do ordinary work.  In the second we have
> an absence in the standard.

It's particularly annoying that Ada doesn't allow bignums,
because every Ada implementation must support a bignum package
-- compile-time arithmetic (static expressions) require it.
So every Ada implementer has to go to all that trouble,
but can't provide that functionality to users at run time -- at
least, not in a standard way.

> On Sat, 12 Apr 2008 11:50:56 -0700 (PDT), Eric Hughes wrote:
>> I believe many of the issues involving strings could be addressed by
>> introducing a predefined type universal_string.
>
> On Apr 12, 3:09 pm, "Dmitry A. Kazakov" <mail...@dmitry-kazakov.de>
> wrote:
>> I don't see it this way.
>
> I have a strong counterclaim--I don't think it can be solved without
> introducing such a type.

> Here's the real rub: universal_integer and universal_string are each
> _unimplementable_ as executable types.  As abstract mathematical
> types, they're perfectly well-defined.  The origin of the difference
> is that universal types have no possible bound in size.  Since every
> computer type has such a bound, there's a fundamental disjunct between
> these two.  An unbounded type actually does have a bound--it throws an
> exception when its internal bounds are exceeded.  A hypothetical
> implementation of a universal type would be unable *in principle* to
> throw such an exception.  This is clearly contrary to fact, where
> every program can run out of memory.

Well, the limits on bignums are fundamentally different from the limits
on Ada's integer types.  In a language with bignums, the _language_
places no limit on the size of integers.  An implementation can
of course run out of memory, but that's not a limit on the size
of any particular integer type, and the "limit" depends not only
on how much memory you have, but also on how much you're using for
something else.

Unbounded strings would be similar, if they were indexed by bignums.

> If this sounds like my idea for partial type specification (one
> without code), it should.  These ideas come from the same perspective.
>
> There's no concept (except _ad hoc_ in the ARM) of what a universal,
> unimplementable type is; there's certainly no way of declaring one.
> So here's the very beginning of a proposal.  To declare and define
> such a type:
>
>     universal_type_definition ::= *universal* *type*
> defining_identifier [known_discriminant_part] *;*

I don't quite understand all this stuff about user-defined
universal types (you give syntax, but didn't fully explain
the semantics).  But anyway, you seem to be inventing something
like abstract types, and/or class-wide types.

Note that universal_integer is conceptually the same thing
as root_integer'Class.  The RM doesn't say that, but the
language designers had that analogy in mind.

>    universal type U ;
>    function op( U Object ) return U ;
>    type T1 is private and U ;
>    type T2 is private and U ;
>    overriding function op( T1 Object ) return T1 ;
>    overriding function op( T2 Object ) return T2 ;
>    function U( T2 Object ) return T1 ;
>    T2 x ;
>    T1 y1 := T1.op( U( x ) ) ;
>    T1 y2 := U( T2.op( x ) ) ;
>    T1 y := x.op ;

The above is an odd mixture of C-like syntax and Ada-like syntax.
Surely "is private and U" should be "is new U with private".
And "T2 x;" should be "X: T2;"

> The expressions for y1 and y2 should be interchangeable as
> implementations for the expression for y.  The point of the
> declarations is to give unambiguous semantics to the expression
> "x.op", so that it does not matter to the correctness of the program
> what implementation expression the compiler chooses.  If Usenet had
> better formatting, I'd draw a commutative diagram as an illustration.

I don't see any semantics, unambiguous or otherwise, in the above.
Sorry -- I just can't guess what it means.

> There's special meaning behind the conversion function U.  Its
> mandatory semantics is to convert an object of T2 to one of T1, such
> that their values are equal as universal values.

I don't know what "equal as universal values" means, either.

Anyway, the problem with Unbounded_Strings, as I see it,
is that Ada doesn't allow user-defined types to use all
the same notations as the built-in ones.  Literals,
indexing, etc.

- Bob

Re: Ada.Strings.Bounded

[Eric Hughes]

On Apr 13, 2:02 pm, Robert A Duff <bobd...@shell01.TheWorld.com>
wrote:
> The analogy is not perfect.  You can create arbitrarily large strings
> (within the limits of available memory, and the bounds of Integer,
> which is pretty big).  It's just that any particular string object
> cannot change length.  Integers are much more restricted -- you can't
> create an integer bigger than some implementation-defined limit,
> such as 32 or 64 bits.

The perspective I have is that of the relationship between groupoids
and groups (and for strings, semigroupoids and semigroups).  A
groupoid, briefly, is just like a group except that its binary
operation is a partial function rather than a total function.  The
inverse function is also partial.  This terminology means that the
binary operation isn't defined on certain pairs.  The groupoid axioms
agree with the group axioms with the proviso that this is only
required where all the groupoid operations are defined.  There also
axioms to ensure that the operation is defined where it's possible to
define it symbolically.

The canonical example of a groupoid is a checkerboard.  This is
clearly like an infinite, bi-colored plane pattern, but it doesn't
have translational group symmetries because of the boundaries.  It
does have, however, translational groupoid symmetries.

From this perspective, the analogy is exact.  Raising an exception is
the computer-language way of indicating the difference between the
domain of a total function and that of a partial function.  Arithmetic
out-of-bounds raises Constraint_Error.  Concatenating strings to make
one that's too large raises Storage_Error.  If you don't get these
exceptions, your operations are known to satisfy the defining axioms
of the type.

I don't know if anybody has developed an "-oid" morphism for category
theory that takes an axiomatic theory and maps it to its "theory-oid"
version.  This is the mathematics for a proper formal theory of the
relationship between universal types and programming-language types.
(Note: when the set of elements of a universal type are finite, the "-
oid" morphism would be the identity.)  Yet I don't think there's a
practical reason to wait for this bit of research.  Map partial
function non-definition to an exception and otherwise assume that any
defining axioms are satisfied.


Switching subjects slightly, your comment points out (to me, at least)
a small deficiency in Ada's Integer types.  I think it should be
possible to define
   type Really_Long_Natural is range 0 .. 2**256 - 1 ;
with a mandate that it always compile.  This is the proper analogue
within integer types (as I think you took it) to fixed length
strings.  In this meaning, a more direct one, the analogue of an
integer is a string of length 1.  (BTW, such a type would be useful
for implementing symmetric ciphers.)

As you point out, there's already a bignum facility within a compiler,
so doing bignum arithmetic with fixed bounds should also be possible.
Indeed, evaluating the range expression itself requires that
facility.  The same bignum facility, with small modifications, could
also serve as the implementation basis of Unbounded_Integer, presented
as a library function rather than a native type.


> Well, the limits on bignums are fundamentally different from the limits
> on Ada's integer types.  In a language with bignums, the _language_
> places no limit on the size of integers.  An implementation can
> of course run out of memory, [...]
> Unbounded strings would be similar, if they were indexed by bignums.

I take this as a report of a language defect.  An unbounded string
*must* to be indexed by an unbounded natural.  If it's not, then the
string is bounded or it's not a string (since it would then break the
indexing axioms).  Changing this shouldn't create any backward-
compatibility problems for existing code, since there's a natural
inclusion map on values from word-length-limited Naturals into
unbounded Naturals.

Caveat: For the above to make sense, the phrase "unbounded string"
preceding does not mean "Ada.Strings.Unbounded_String", but rather the
well-defined-but-not-implemementable (i.e. universal) type
universal_string.

> I don't quite understand all this stuff about user-defined
> universal types (you give syntax, but didn't fully explain
> the semantics).  But anyway, you seem to be inventing something
> like abstract types, and/or class-wide types.

I wasn't trying to completely precise because of space limitations.
But let me say outright that I am sure this idea is not an abstract
type and not a class-wide type.  For an Ada-relevant means of entry to
this idea, here's a quotation from ARM 4.5.3/1:
> The binary adding operators + (addition) and - (subtraction)
> are predefined for every specific numeric type T with their
> conventional meaning.
So where does the "conventional meaning" come from?  Imprecisely, it's
been around as long as history.  Recall, Euclid had a proof that there
was no largest number.  Precisely, it dates to the earliest days of
modern formal logic, say, the late nineteenth century.  Neither of
these definitions have anything to do with programming languages.  But
that's the key to the whole puzzle.  The mental ideas that constitute
types as values and their manipulations originate outside computers
and their programming languages.  The way that humanity has found to
think precisely about these is with the tools of formal logic.

> Note that universal_integer is conceptually the same thing
> as root_integer'Class.  The RM doesn't say that, but the
> language designers had that analogy in mind.

As I've said in so many words just above, I believe this analogy is
infelicitous.  (I really do _not_ mean "wrong" here.)  It takes the
discussion inward to more programming language ideas and leads to
infinite regress--and lack of progress.

My idea of universal_integer is the following.  Start with the symbol
"0" and the unary function "S".  All the terms (in the predicate
calculus sense) of these two symbols constitute the set of integers.
By doing this, I eliminate non-standard models.  Add the axioms of
Peano arithmetic to get addition.  Add the rest of the axioms of
arithmetic to get its ordinary operator behavior.  That set of terms
with such axioms constitute universal_integer.

There's a canonical injective interpretation mapping from Ada's
Integer into universal_integer.  This is the value map.  It is not an
identity map, because the domain and range are not the same.  This
point is subtle and critical.  The domain is the valid values of Ada's
type Integer *as it is defined in the ARM* and its range is set of
symbols paired with a set of axioms.  These aren't the same.  They
cannot possibly be the same.  Any programming language has to down-
convert the total functions of a universal type to partial functions
of an implementable one.

There's a corresponding representation mapping in the other direction;
it's a partial function (necessarily).


> The above is an odd mixture of C-like syntax and Ada-like syntax.
> And "T2 x;" should be "X: T2;"

Yeah, my slip.  I've been on a C++ project lately.

> Surely "is private and U" should be "is new U with private".

But this one I meant.  A universal type should not be directly derived
from a universal type.  So I lifted the interface syntax.  Why
shouldn't you derive from a universal type?  Because it's not
implementable!  Universal types have a whole set of interrelationships
I'm avoiding; entirely within the set of universal types there's
something just like derivation.

So I can now outline what the relationship ought to be:
-- The set of values of an implemented type is
      a _subset_ of the terms of the universal type.
-- The set of operators on an implemented type
      _satisfy_ the axioms of the universal type.
Satisfaction here is framed in terms of preconditions, postconditions,
and invariants, in other words, all the specification apparatus of
program correctness.

> I don't know what "equal as universal values" means, either.

It means (now that I've put out some apparatus) that the values of the
interpretations maps are equal as terms of the universal type.
Symbolically, its the predicate "interpretation( y1 ) =
interpretation( y2 )", where "interpretation" is a (mathematical)
function Ada.Integer --> universal_integer.

Eric

Re: Ada.Strings.Bounded

[Dmitry A. Kazakov]

On Sun, 13 Apr 2008 16:20:24 -0700 (PDT), Eric Hughes wrote:

> Why
> shouldn't you derive from a universal type?  Because it's not
> implementable!

One does not imply another. If you are aiming at Liskov substitutability
principle, you should also remember how it is defined. It is in terms of
*provable* propositions. Pragmatically, the program is correct even if
there exist unreachable states where it could crash. However, LSP does not
work anyway.

> So I can now outline what the relationship ought to be:
> -- The set of values of an implemented type is
>       a _subset_ of the terms of the universal type.

Counterexample: NaN of Float.

(The set of values of a derived type is neither subset or superset. It is a
different set. There could be mappings defined between these two sets in
order to achieve substitutability. Such mappings could be injective, or
not)

> -- The set of operators on an implemented type
>       _satisfy_ the axioms of the universal type.

This cannot work because any implementation is necessarily a DFA.

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

Re: Ada.Strings.Bounded

[Eric Hughes]

On Apr 14, 3:07 am, "Dmitry A. Kazakov" <mail...@dmitry-kazakov.de>
wrote:
> If you are aiming at Liskov substitutability
> principle,

But I'm not aiming for that.  It's related, to be sure, but it's not
the same.  If you don't acknowledge that a universal type is a
different creature than an ordinary type, then you would have to see
only preexisting relationships.

> > So I can now outline what the relationship ought to be:
> > -- The set of values of an implemented type is
> >       a _subset_ of the terms of the universal type.
>
> Counterexample: NaN of Float.

I take from what you're saying that the ordinary way of bringing
floating point arithmetic into a language is not an implementation of
universal Real numbers.  That's true.

We can talk about optimal encodings and less-than-optimal encodings,
if you'd like, but I really don't see how the exceptional values of
floating point numbers violate the spirit of the rule.  NaN, but even
more so overflow and underflow, even though they're defined for
hardware implementations, could well be forbidden as accessible values
from within the language.  You clearly couldn't eliminate this kind of
type from ordinary use soon, because it's well-embedded in practice
and skills.

The issue then becomes whether it would be beneficial to also have a
Real-implementing type in the pattern I've mentioned.  The differences
would be small.  Since a calculation that results in an exceptional
value raises an exception, such a value that would otherwise be
assigned is simply not assigned (or even made visible).  I think that
takes care of all the modification that would be needed.

> The set of values of a derived type is neither subset or superset. It is a
> different set.

If you insist, but this is not derivation.

> > -- The set of operators on an implemented type
> >       _satisfy_ the axioms of the universal type.
>
> This cannot work because any implementation is necessarily a DFA.

???

Eric

Re: Ada.Strings.Bounded

[Dmitry A. Kazakov]

On Mon, 14 Apr 2008 08:50:21 -0700 (PDT), Eric Hughes wrote:

> On Apr 14, 3:07 am, "Dmitry A. Kazakov" <mail...@dmitry-kazakov.de>
> wrote:
>> If you are aiming at Liskov substitutability
>> principle,
> 
> But I'm not aiming for that.  It's related, to be sure, but it's not
> the same.  If you don't acknowledge that a universal type is a
> different creature than an ordinary type, then you would have to see
> only preexisting relationships.

I think it is wrong to consider N and universal_integer equivalent.

>>> So I can now outline what the relationship ought to be:
>>> -- The set of values of an implemented type is
>>>       a _subset_ of the terms of the universal type.
>>
>> Counterexample: NaN of Float.
> 
> I take from what you're saying that the ordinary way of bringing
> floating point arithmetic into a language is not an implementation of
> universal Real numbers.  That's true.

It is not a subset of R. Subseting is not a sufficient condition for a
successful modeling. Actually it is the opposite, a perfect subset cannot
be a good model. The best models of R aren't even close to subsets. For
example intervals with rational bounds.

>> The set of values of a derived type is neither subset or superset. It is a
>> different set.
> 
> If you insist, but this is not derivation.

It makes life a lot easier. Otherwise you will need to introduce encodings,
have to define the underlying bit patterns, and will never be able to
abstract implementations.
 
>>> -- The set of operators on an implemented type
>>>       _satisfy_ the axioms of the universal type.
>>
>> This cannot work because any implementation is necessarily a DFA.
> 
> ???

Programs are DFA (except hardware interrupts etc).

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

Re: Ada.Strings.Bounded

[Eric Hughes]

On Apr 14, 12:52 pm, "Dmitry A. Kazakov" <mail...@dmitry-kazakov.de>
wrote:
> I think it is wrong to consider N and universal_integer equivalent.

Sure.  It's {\bb Z} and universal_integer that are equivalent.

Seriously, we just disagree about this.  I can't take
universal_integer seriously as a root class, because it's impossible
to write down any representation of it.  I believe the approach I've
been thinking about could provide some reasonably solid grounding for
what universal integer is.

> Subseting is not a sufficient condition for a
> successful modeling.

In a discussion that's got a lot of formal logic in it, the word
"model" already means something pretty specific, usually involving a
Tarski structure.  On the other hand, the informal use of the word
"model", in this context, is basically beside the point, which is to
get a precise definition of a hypothetical universal real type,
amongst others.  There are plenty of useful things that are not-quite-
real numbers, such as the one- and two-point compactifications of the
real line, but these are the same thing as real numbers.  If you want
them, fine; just don't try to claim that they are same thing and use a
confusing name for them.

> Actually it is the opposite, a perfect subset cannot
> be a good model.

There was paper from the fifties (sorry, no reference handy), which
used Turing machines to compute a Dedekind cut.  On input a rational
number, it returned one of the two symbols "<=x" or ">=x".  (You
cannot compute exact trichotomy without solving the halting problem.)
In any language describing these machines, there's a least one (Kleene
minimization), so there's a unique representative of such a machine
for every computable real number, which means there's a subset
bijection.  Addition, multiplication, and their inverses are defined
in terms of the underlying operand-machine (it's pretty easy coding,
actually).  So there's pretty close to a perfect model of the real
numbers, whose only real limitation is that run times are horrendously
slow.  But it's also completely exact, with no compromises but
execution speed and representation size of a machine.

The subset is every real number that's computable.  About as good as
you can do with computers, I'd say.

> The best models of R aren't even close to subsets. For
> example intervals with rational bounds.

In the precise meaning of model, it's just not a model, because
there's no total ordering on such intervals, so the ordering axioms
are not satisfied.  In an imprecise meaning, it's real numbers plus
some other concept, which is more than {\bb R}.

Eric

Re: Ada.Strings.Bounded

[Dmitry A. Kazakov]

On Mon, 14 Apr 2008 19:07:25 -0700 (PDT), Eric Hughes wrote:

> On Apr 14, 12:52 pm, "Dmitry A. Kazakov" <mail...@dmitry-kazakov.de>
> wrote:
>> I think it is wrong to consider N and universal_integer equivalent.
> 
> Sure.  It's {\bb Z} and universal_integer that are equivalent.
> 
> Seriously, we just disagree about this.  I can't take
> universal_integer seriously as a root class, because it's impossible
> to write down any representation of it.

Yes, because it is not what you wanted it be.

>> Subseting is not a sufficient condition for a
>> successful modeling.
> 
> In a discussion that's got a lot of formal logic in it, the word
> "model" already means something pretty specific, usually involving a
> Tarski structure.

That is beside the point. A subset of values is not yet a type. The
requirement to be a subset (of values) alone does not enforce anything
useful.

>> Actually it is the opposite, a perfect subset cannot
>> be a good model.
> 
> There was paper from the fifties (sorry, no reference handy), which
> used Turing machines to compute a Dedekind cut.  On input a rational
> number, it returned one of the two symbols "<=x" or ">=x".  (You
> cannot compute exact trichotomy without solving the halting problem.)
> In any language describing these machines, there's a least one (Kleene
> minimization), so there's a unique representative of such a machine
> for every computable real number, which means there's a subset
> bijection.  Addition, multiplication, and their inverses are defined
> in terms of the underlying operand-machine (it's pretty easy coding,
> actually).  So there's pretty close to a perfect model of the real
> numbers, whose only real limitation is that run times are horrendously
> slow.  But it's also completely exact, with no compromises but
> execution speed and representation size of a machine.
> 
> The subset is every real number that's computable.  About as good as
> you can do with computers, I'd say.

No. It cannot represent pi and e. Now consider the following:

   type A_Subset_Of_R is (pi, e);  -- Ready!

The above is a perfect subset of R containing both pi and e. Isn't it good?

>> The best models of R aren't even close to subsets. For
>> example intervals with rational bounds.
> 
> In the precise meaning of model, it's just not a model, because
> there's no total ordering on such intervals, so the ordering axioms
> are not satisfied.  In an imprecise meaning, it's real numbers plus
> some other concept, which is more than {\bb R}.

For any model there are properties which are not satisfied. Intervals are
good because they preserve *interesting* properties and provide fair
approximations for properties lost. Total ordering is mere a property,
which has a minor importance to numeric computations. In fact, each second
handbook on numeric methods starts with something like "never ever compare
reals."

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

Re: Ada.Strings.Bounded

[Eric Hughes]

On Mon, 14 Apr 2008 19:07:25 -0700 (PDT), Eric Hughes wrote:
> Seriously, we just disagree about this.  I can't take
> universal_integer seriously as a root class, because it's impossible
> to write down any representation of it.

On Apr 15, 2:02 am, "Dmitry A. Kazakov" <mail...@dmitry-kazakov.de>
wrote:
> Yes, because it is not what you wanted it be.

My belief about universal_integer is rooted in the language
definition.  I assert that that Ada as currently defined has no bound
on the size of numbers within universal_integer.  Here is my argument.

The best definition is in ARM 3.4.1(6/2-7).  (Defect report: this
doesn't appear in the index entry for universal_integer.)  Wherein:

> The set of values of a universal type is the undiscriminated
> union of the set of values possible for any definable type
> in the associated class.

The associated class to universal_integer is the signed integer type
(3.5.4), delineated by ranges given by static simple_expression.
There's no length limitation on an expression in the language, so
arbitrarily large ranges are possible.  Thus I can define the
following series of types:
    type I1 is range -2^10 .. 2^10 ;
    type I2 is range -2^100 .. 2^100 ;
    type I3 is range -2^1000 .. 2^1000 ;
    -- ...
The exponent in I(n) is an integer within the range of I(n-1).  The
type of an integer literal is universal_integer (2.4), which means
that if I(n-1) is well-defined, then so is I(n).  (Hence the
requirement for bignum arithmetic in the compiler.)  If you want to
exhibit a bound on universal_integer as a counterexample, I will take
its logarithm, round up, and add 1, and use that index to exhibit a
type definition that exceeds this bound.  Every integer is thus a
member of universal_integer.

If you can show me a Ada definition that can store a
universal_integer, only then will I believe you that it's the kind of
type that's just like an ordinary Ada type.

Perhaps you could explain what you want universal_integer to be.

Eric

Re: Ada.Strings.Bounded

[Dmitry A. Kazakov]

On Tue, 15 Apr 2008 07:20:15 -0700 (PDT), Eric Hughes wrote:

> Perhaps you could explain what you want universal_integer to be.

Merely the type of a static numeric expression. Well, it isn't, a
counterexample is:

   A'Length  (ARM 3.6.2)

Universal_Integer is not necessarily Root_Integer, but somewhere close to
the root of Root_Integer'Class.

> If you can show me a Ada definition that can store a
> universal_integer, only then will I believe you that it's the kind of
> type that's just like an ordinary Ada type.

   type T is abstract private;

Can you store T?

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

Re: Ada.Strings.Bounded

[Eric Hughes]

On Tue, 15 Apr 2008 07:20:15 -0700 (PDT), Eric Hughes wrote:
> Perhaps you could explain what you want universal_integer to be.

On Apr 15, 9:23 am, "Dmitry A. Kazakov" <mail...@dmitry-kazakov.de>
wrote:
> Merely the type of a static numeric expression. Well, it isn't, a
> counterexample is:
>
>    A'Length  (ARM 3.6.2)

The fact that lengths are limited does not mean that their values
cannot sit within a type whose values are not.  The set of possible
values of lengths for a certain compiler are a subset of the values of
universal_integer.

> Universal_Integer is not necessarily Root_Integer, but somewhere close to
> the root of Root_Integer'Class.

"Somewhere close" is not a definition.  Please be more specific.

> > If you can show me a Ada definition that can store a
> > universal_integer, only then will I believe you that it's the kind of
> > type that's just like an ordinary Ada type.
>
>    type T is abstract private;
>
> Can you store T?

By ordinary type, I mean the kind that's assignable, not abstract, not
an interface, something you can declare a variable of.

Eric

Re: Ada.Strings.Bounded

[Dmitry A. Kazakov]

On Tue, 15 Apr 2008 19:51:17 -0700 (PDT), Eric Hughes wrote:

> On Tue, 15 Apr 2008 07:20:15 -0700 (PDT), Eric Hughes wrote:
>> Perhaps you could explain what you want universal_integer to be.
> 
> On Apr 15, 9:23 am, "Dmitry A. Kazakov" <mail...@dmitry-kazakov.de>
> wrote:
>> Merely the type of a static numeric expression. Well, it isn't, a
>> counterexample is:
>>
>>    A'Length  (ARM 3.6.2)
> 
> The fact that lengths are limited does not mean that their values
> cannot sit within a type whose values are not.  The set of possible
> values of lengths for a certain compiler are a subset of the values of
> universal_integer.

A'Length is of Universal_Integer.

>> Universal_Integer is not necessarily Root_Integer, but somewhere close to
>> the root of Root_Integer'Class.
> 
> "Somewhere close" is not a definition.  Please be more specific.

It is specific. "Close" means: a small tree distance to Root_Integer. (Tree
is the type inheritance tree.)

>>> If you can show me a Ada definition that can store a
>>> universal_integer, only then will I believe you that it's the kind of
>>> type that's just like an ordinary Ada type.
>>
>>    type T is abstract private;
>>
>> Can you store T?
> 
> By ordinary type, I mean the kind that's assignable, not abstract, not
> an interface, something you can declare a variable of.

So, actually, the whole point is that we could not have a variable of
Universal_Integer?

It is not uncommon. I cannot have a variable of a constant Boolean.

   X : constant Boolean := False;
begin
   X := True; -- Illegal, "constant" disallows ":="

Maybe it is indefinite types which worry you? Yes, I cannot have a variable
of String:

   X : String; -- Illegal, no constraint given

There is nothing special in Universal_Integer except that it lacks some
"primitive" operations, an Integer possess.

The only really interesting property of Universal_Integer is that its
constants are required to be static. I would allow such constraints for any
types, in order to introduce static compilation units (functions, packages,
maybe, procedures).

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

Re: Ada.Strings.Bounded

[Dmitry A. Kazakov]

On Tue, 15 Apr 2008 06:56:57 -0700 (PDT), Eric Hughes wrote:

> On Mon, 14 Apr 2008 19:07:25 -0700 (PDT), Eric Hughes wrote:
>> Seriously, we just disagree about this.  I can't take
>> universal_integer seriously as a root class, because it's impossible
>> to write down any representation of it.
> 
> On Apr 15, 2:02 am, "Dmitry A. Kazakov" <mail...@dmitry-kazakov.de>
> wrote:
>> Yes, because it is not what you wanted it be.
> 
> I assert that that Ada as currently defined has no bound on the size
> of numbers within universal_integer.

It specifies the lower bound and leaves the upper bound up to the vendor.
Which by no means imply that there were no upper bound. In any given
instance of Ada compiler universal_integer has an upper bound. Moreover,
because the number of all instances of all existed, existing and future Ada
compilers is obviously finite, there also exists the upper bound of
universal_integer as a whole.

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

Re: Ada.Strings.Bounded

[Eric Hughes]

On Tue, 15 Apr 2008 06:56:57 -0700 (PDT), Eric Hughes wrote:
> I assert that that Ada as currently defined has no bound on the size
> of numbers within universal_integer.

On Apr 15, 8:58 am, "Dmitry A. Kazakov" <mail...@dmitry-kazakov.de>
wrote:
> It specifies the lower bound and leaves the upper bound up to the vendor.
> Which by no means imply that there were no upper bound.

That's an upper bound for a compiler, not for "Ada as currently
defined".  Please check my language carefully.

> Moreover,
> because the number of all instances of all existed, existing and future Ada
> compilers is obviously finite, there also exists the upper bound of
> universal_integer as a whole.

"All compilers that were, all that are, and all that will ever be"--
these are not part of the Ada language definition.  My assertion
stands.

I would still like to know what you think universal_integer actually
is.

Eric

Re: Ada.Strings.Bounded

[Dmitry A. Kazakov]

On Tue, 15 Apr 2008 19:46:12 -0700 (PDT), Eric Hughes wrote:

> On Tue, 15 Apr 2008 06:56:57 -0700 (PDT), Eric Hughes wrote:
>> I assert that that Ada as currently defined has no bound on the size
>> of numbers within universal_integer.
> 
> On Apr 15, 8:58 am, "Dmitry A. Kazakov" <mail...@dmitry-kazakov.de>
> wrote:
>> It specifies the lower bound and leaves the upper bound up to the vendor.
>> Which by no means imply that there were no upper bound.
> 
> That's an upper bound for a compiler, not for "Ada as currently
> defined".  Please check my language carefully.
> 
>> Moreover,
>> because the number of all instances of all existed, existing and future Ada
>> compilers is obviously finite, there also exists the upper bound of
>> universal_integer as a whole.
> 
> "All compilers that were, all that are, and all that will ever be"--
> these are not part of the Ada language definition.  My assertion
> stands.

Neither a bound nor its absence is required. The former does not imply the
latter. Try a certified Ada compiler on:

   X : constant := 2**(2**(2**(2**(2**1000))));

> I would still like to know what you think universal_integer actually is.

Universal_Integer is merely an integer type.

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

Re: Ada.Strings.Bounded

[Eric Hughes]

On Apr 16, 2:16 am, "Dmitry A. Kazakov" <mail...@dmitry-kazakov.de>
wrote:
> Universal_Integer is merely an integer type.

OK, now you're just wrong.  Wrong, that is, assuming that by "integer
type" you mean an "integer type as defined by Ada" and not some other
notion of "integer type".  I've never seen you to acknowledge any
other kind of type here, so I believe I'm making that assumption in
good faith.

Suppose there existed some single and specific Ada integer type M
which is the same type as universal_integer.  All non-modular integer
types are defined by ranges (see 3.5.4 "Integer Types").  Since M is a
scalar type, the lower bound is M'First and the upper bound is M'Last
(see 3.5).  Since M is an integer type, it is declarable.  Let 'm' be
an integer literal by which the upper bound of M can be declared.  By
the premise, 'm' is an expression of universal_integer.  By my
previous proof about universal_integer, the expression 'm+1' is also a
universal_integer.  But 'm+1' is not a member of M.  Thus M cannot be
a type for universal_integer.

Now you'll come right back and cite things that aren't in the language
specification: specific compilers and specific programs.  Were you to
insist upon citing these, it would be tantamount to saying the
standard isn't actually normative, that instead practice is
normative.  But then I'd believe that you don't know the meaning of
the word "normative".

But I'll address them anyway, to forestall confusion.

Let's start with programs.  Take a the entire source code of any
program.  It's finite.  For that body of code, there's a
universal_integer expression of greatest absolute value.  Call it
'n'.  Declare the type
    type Large_Enough_Integer is range -n .. n ;
By assumption, every universal_integer that appears in that program is
a member of Large_Enough_Integer.  Furthermore, every integer type has
bounds that are members of Large_Enough_Integer.  Thus every integer
value that could ever be in that program has a value that's a member
of Large_Enough_Integer.  But Large_Enough_Integer is not the same as
universal_integer, because the value of 'n+1' is not in
Large_Enough_Integer and it is in universal_integer.  Thus, what's
true is the following predicate:
   For every program P,
   there exists an integer type N,
   for all executions E of P,
   for all times T within E,
   for all variables X within P,
   the value of X at time T within E is a value of N.

This predicate does not make N into universal_integer.  What it says
is that there's a relativized version of universal_integer which is
just barely adequate for every program.  But universal_integer is NOT
defined on a program-by-program basis.  It's defined for the language
as a whole.  For each program, there's a large-enough type, but that
type is not universal_integer.  It's supremum_integer_for_program_P.

The case for compilers is rather more subtle.  Let's dispose of the
easy case first.  Suppose there's some internal limit on the size of
integer types that a compiler accepts; call the type at that limit
'supremum_compilable_integer'.  Then that compiler does not accept
programs P where supremum_integer_for_program_P won't fit into
supremum_compilable_integer.  Now 'supremum_compilable_integer+1' is
also a universal_integer, but one that this compiler does not accept.
Now there's no requirement that a compiler be able to handle every
universal_integer in order to be a conformant compiler.  Such a
requirement would be impossible to satisfy, because it would require
an execution size that was unbounded, even though the compiler itself
could be bounded.  Hence for this case too, there's a relativized
version of universal_integer that applies to the compiler, but that
type isn't universal_integer either.

For a compiled program with an internally limited compiler, then, we
have the following sketch of potential type relationships:
    supremum_compilable_integer --> supremum_integer_for_program_P -->
root_integer
I didn't put universal_integer in there, though, because it's not a
type in the same sense that these others are.

A compiler, in theory (though certainly not in present practice), is
capable of generating expressions for arbitrarily large integers.
I'll be willing to discuss this case later, after the simpler cases
are properly disposed of.

Eric

Re: Ada.Strings.Bounded

[Dmitry A. Kazakov]

On Wed, 16 Apr 2008 07:40:32 -0700 (PDT), Eric Hughes wrote:

> By my
> previous proof about universal_integer, the expression 'm+1' is also a
> universal_integer.

How so? Clearly "+" is not closed in Universal_Integer. For any compiler,
there always exists an Ada program such that:

   M : constant := <some-literal>; -- Compiles
   N : constant := M + 1;  -- Does not compile

[...]
> By assumption, every universal_integer that appears in that program is
> a member of Large_Enough_Integer.

No. It does not include Universal_Integer, Root_Integer and BigNum if the
latter two will ever come. Certainly any of these types (should they become
named) would have either no attribute S'Range defined, or else one raising
Constraint_Error.

> For a compiled program with an internally limited compiler, then, we
> have the following sketch of potential type relationships:
>     supremum_compilable_integer --> supremum_integer_for_program_P -->
> root_integer
> I didn't put universal_integer in there, though, because it's not a
> type in the same sense that these others are.

Universal_Integer is a type, merely because ARM tells so. As I said before
it is not what you hold it for. Further, you cannot have what you want,
because that would be incomputable.

> A compiler, in theory (though certainly not in present practice), is
> capable of generating expressions for arbitrarily large integers.

Any compiler is a program with a finite number of states. Let each state of
it compiles a legal Ada program (in reality the ratio is much lower than
that). Now consider the following set of programs Foo_n:

procedure Foo_n is
   N : constant := <decimal-literal-of-n>;
begin
   null;
end Foo_n;

Clearly, this set is larger that the set of all states. Therefore, there
exists m, such that Foo_m is not compilable. q.e.d.

[Surely, you could design an Ada compiler which would compile one given
legal Ada program. But you cannot have a compiler which would compile any
legal program.]

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

Re: Ada.Strings.Bounded

[Eric Hughes]

On Wed, 16 Apr 2008 07:40:32 -0700 (PDT), Eric Hughes wrote:
> By my
> previous proof about universal_integer, the expression 'm+1' is also a
> universal_integer.

As a reference, that message was
<b7c7de31-2e96-4f5b-882e-5e991d52ae93@a9g2000prl.googlegroups.com>.

On Apr 16, 12:28 pm, "Dmitry A. Kazakov" <mail...@dmitry-kazakov.de>
wrote:
> How so? Clearly "+" is not closed in Universal_Integer.

No, addition is closed in universal integer.  It's an implication of
its definition. From 3.5.4/14
> Integer literals are all of the type universal_integer, the
> universal type (see 3.4.1) for the class rooted at root_integer,
> allowing their use with the operations of any integer type.

Every universal_integer has a literal expression 'm'. The expression 'm
+1' is also a literal.  All literals have type universal_integer (see
2.4/3).  Therefore 'm+1' is also a universal_integer.

The same kind argument works to argue to prove closure, although that
requires recursion on the structure of 'm'.  Writing up that proof
would be beside the point right now.

> Universal_Integer is a type, merely because ARM tells so.

I should have realized that this was the point of the agreement long
before.  The ARM is wrong on this point, or at the very least
inconsistent.  Either they'll have to just say it's not a type (that
is, an implementable Ada type) or they'll have to change the rules
about integer literals.  The above proof about 'm+1' can be taken as a
proof of inconsistency, if you like.

My attitude is that you can't declare a variable of universal_integer,
so it's no great harm if it's not an ordinary Ada type.  There's
another point I might have made earlier: universal_integer is a type
that could well appear in other programming languages, because it's a
completely abstract type, and I do not mean "abstract" in any of the
ways that's used as a reserved word in any programming language.  By
"completely abstract", I mean it's a pure concept of thought, a
mathematical abstraction.

It's the connection of such mathematically abstract types to
programming language types that was the point of contact with the
original posting.

Eric

Re: Ada.Strings.Bounded

[Robert A Duff]

Eric Hughes <eric.eh9@gmail.com> writes:

> On Wed, 16 Apr 2008 07:40:32 -0700 (PDT), Eric Hughes wrote:
>> By my
>> previous proof about universal_integer, the expression 'm+1' is also a
>> universal_integer.
>
> As a reference, that message was
> <b7c7de31-2e96-4f5b-882e-5e991d52ae93@a9g2000prl.googlegroups.com>.
>
> On Apr 16, 12:28 pm, "Dmitry A. Kazakov" <mail...@dmitry-kazakov.de>
> wrote:
>> How so? Clearly "+" is not closed in Universal_Integer.
>
> No, addition is closed in universal integer.  It's an implication of
> its definition. From 3.5.4/14
>> Integer literals are all of the type universal_integer, the
>> universal type (see 3.4.1) for the class rooted at root_integer,
>> allowing their use with the operations of any integer type.
>
> Every universal_integer has a literal expression 'm'. The expression 'm
> +1' is also a literal.  All literals have type universal_integer (see
> 2.4/3).  Therefore 'm+1' is also a universal_integer.

No, that's not quite right.  There's no such thing as a "literal
expression" in Ada, so I don't know what you mean by that.  Static
expression?  Expression of type universal_integer?  No idea...
The expression 'm+1' is certainly NOT a literal -- it's a function
call, passing an identifier and a literal as the actual parameters.

An integer literal has type universal_integer, as you said, but
universal_integer has no "+" operator.  There is a "+" for root_integer,
and also for user-defined integer types.  Universal_integers can be
implicitly converted to various integer types.

The type of an expression like m+1 depends in part on the context.

M : constant := 123; -- M is of type universal_integer.
X : constant := M + 1; -- The "+" for root_integer is called.
                       -- X is of type universal_integer.

type My_Int is range 1..100;
Y : constant My_Int := 1 + 1; -- The "+" of My_Int is called.
                              -- Y is of type My_Int.

In both of the above "+" calls, the universal_integer operands are
implicitly converted -- to root_integer in the first case, and to My_Int
in the second case.

Static expressions are calculated exactly (arbitrary range).
Dynamic expressions are limited to some implementation
defined ranges -- this includes run-time values of type
root_integer and universal_integer.

> I should have realized that this was the point of the agreement long
> before.  The ARM is wrong on this point, or at the very least
> inconsistent.  Either they'll have to just say it's not a type (that
> is, an implementable Ada type) or they'll have to change the rules
> about integer literals.  The above proof about 'm+1' can be taken as a
> proof of inconsistency, if you like.

I don't see any inconsistency here.  An inconsistency would be a case
where the RM contradicts itself about whether a certain program is
legal, or what the run-time semantics of the program is.  You have
proven nothing of the kind, as far as I can see.

Anyway, it might make your point clearer if you explain it again,
but using proper Ada terminology this time.  I'd be interesting
in understanding your point...

- Bob

Re: Ada.Strings.Bounded

[Eric Hughes]

On Apr 21, 8:08 am, Robert A Duff <bobd...@shell01.TheWorld.com>
wrote:
> Anyway, it might make your point clearer if you explain it again,
> but using proper Ada terminology this time.

I will endeavor to use Ada terminology when I can, but there is not
Ada terminology for some of the things I'm talking about.  I'll start
back at the beginning of the argument I made just previously.  I'm
stripping this argument down to its basics.  I've removed any piece of
the argument that includes anything that might be mistaken for an Ada
arithmetic operation.

Eric Hughes <eric....@gmail.com> writes:
> Every universal_integer has a literal expression 'm'.

Let N0 be the value in {\bb N} for this universal integer.  This N0 is
not an Ada natural, it's a mathematical one.  I will presume that
there is an injective map from universal_integer into {\bb Z} that
preserves value.  I would find it absurd to disagree with this
premise, but I'd rather make it explicit than not.

What I mean by what I said is that there a sequence of characters 'm'
that, when used as a static_expression in a number_declaration
(3.3.2/2), creates an Ada constant whose value is equal to N0.  'm' is
not an Ada construct, it's a sequence of characters valid for
substitution into an Ada program.  Furthermore, we can find such an
'm' that is valid as a 'numeral' (2.4.1/3), consisting only of
digits.  Since I was only discussing positive upper bounds and
'numeral' has no minus sign in its syntax, this sequence of characters
is unique and always exists.

Eric Hughes <eric....@gmail.com> writes:
> The expression 'm+1' is also a literal.

Let N1 = N0 + 1.  N1 is also in {\bb N}. There's another sequence of
characters, which I called 'm+1', again also valid as an Ada
'numeral', that has the value N1.  We compute this using outside-of-
Ada ordinary mathematical operations.  ARM 2.4.1 "Decimal Literals"
has no length limitation on 'numeral'.

Eric Hughes <eric....@gmail.com> writes:
> All literals have type universal_integer (see 2.4/3).
> Therefore 'm+1' is also a universal_integer.

Admittedly I was only talking about integer literals; other literals
have different types.  The term "integer literal" is defined in ARM
2.4/1:
> an integer literal is a numeric_literal without a point
Both sequences of characters 'm' and 'm+1' consist only of digits, so
each is also valid as an "integer literal".

So far I've only dealt with syntactic issues.  I need to now make an
assertion about type.  From ARM 2.4/3:
> The type of an integer literal is universal_integer.

I see two arguably-correct ways of interpreting this statement, one
absolute and one contingent:
-- Every integer literal has a type and that type is
universal_integer.
-- If an integer literal has a type, that type is universal_integer.
I believe the contingent version is not the meaning.  The ARM
statement is written in unconditional language.  "The type of an
integer literal" identifies the unique type associated with that
integer literal and implies that there is always such a type.  The
contingent version of this sentence would be "The type of an integer
literal, if any, is universal_integer."  But that's not what it says.

Hence both 'm' and 'm+1' have a type, and that that type is
universal_integer.  By induction, universal_integer has no upper
bound.


On Apr 21, 8:08 am, Robert A Duff <bobd...@shell01.TheWorld.com>
wrote:
> The expression 'm+1' is certainly NOT a literal -- it's a function
> call, passing an identifier and a literal as the actual parameters.

I redid the argument to get rid of this ambiguity.  Admittedly I had
not distinguished addition on {\bb N} and addition on Ada types.  My
argument doesn't rely upon addition on any Ada type.

> Universal_integers can be
> implicitly converted to various integer types.

This was the whole point of the discussion--why such implicit
conversions do not break the type system.  It's not like integers are
a tagged type.

> type My_Int is range 1..100;
> Y : constant My_Int := 1 + 1; -- The "+" of My_Int is called.
>                               -- Y is of type My_Int.

Are there other places in Ada when the context of an operation
determines the type of the operands of the function and thus also the
function signature?

Context-dependent function selection need not break correctness of a
program, even when there's ambiguity in what function might be
selected (non-deterministic execution).  The conditions for this to
work are implicitly present with integer types.  I believe it's
possible to make them explicit for arbitrary types.

Eric

Re: Ada.Strings.Bounded

[Robert A Duff]

Eric Hughes <eric.eh9@gmail.com> writes:

> On Apr 21, 8:08 am, Robert A Duff <bobd...@shell01.TheWorld.com>
> wrote:
>> Anyway, it might make your point clearer if you explain it again,
>> but using proper Ada terminology this time.
>
> I will endeavor to use Ada terminology when I can, but there is not
> Ada terminology for some of the things I'm talking about.  I'll start
> back at the beginning of the argument I made just previously.  I'm
> stripping this argument down to its basics.  I've removed any piece of
> the argument that includes anything that might be mistaken for an Ada
> arithmetic operation.

OK, thanks.  I think I get it now.

> Eric Hughes <eric....@gmail.com> writes:
>> Every universal_integer has a literal expression 'm'.
>
> Let N0 be the value in {\bb N} for this universal integer.  This N0 is
> not an Ada natural, it's a mathematical one.  I will presume that
> there is an injective map from universal_integer into {\bb Z} that
> preserves value.  I would find it absurd to disagree with this
> premise, but I'd rather make it explicit than not.
>
> What I mean by what I said is that there a sequence of characters 'm'
> that, when used as a static_expression in a number_declaration
> (3.3.2/2), creates an Ada constant whose value is equal to N0.  'm' is
> not an Ada construct, it's a sequence of characters valid for
> substitution into an Ada program.  Furthermore, we can find such an
> 'm' that is valid as a 'numeral' (2.4.1/3), consisting only of
> digits.  Since I was only discussing positive upper bounds and
> 'numeral' has no minus sign in its syntax, this sequence of characters
> is unique and always exists.
>
> Eric Hughes <eric....@gmail.com> writes:
>> The expression 'm+1' is also a literal.
>
> Let N1 = N0 + 1.  N1 is also in {\bb N}. There's another sequence of
> characters, which I called 'm+1', again also valid as an Ada
> 'numeral', that has the value N1.  We compute this using outside-of-
> Ada ordinary mathematical operations.  ARM 2.4.1 "Decimal Literals"
> has no length limitation on 'numeral'.

OK, so m is some sequence of characters -- an integer literal.
That's what I was confused about before.

(Nit: an implementation is allowed to restrict integer literals
to 200 characters.  See RM-2.2(14).  It is not required to do
so, and anyway, it doesn't change the fact that there are an
infinite number of integers.)

> Eric Hughes <eric....@gmail.com> writes:
>> All literals have type universal_integer (see 2.4/3).
>> Therefore 'm+1' is also a universal_integer.
>
> Admittedly I was only talking about integer literals; other literals
> have different types.  The term "integer literal" is defined in ARM
> 2.4/1:
>> an integer literal is a numeric_literal without a point
> Both sequences of characters 'm' and 'm+1' consist only of digits, so
> each is also valid as an "integer literal".
>
> So far I've only dealt with syntactic issues.  I need to now make an
> assertion about type.  From ARM 2.4/3:
>> The type of an integer literal is universal_integer.
>
> I see two arguably-correct ways of interpreting this statement, one
> absolute and one contingent:
> -- Every integer literal has a type and that type is
> universal_integer.
> -- If an integer literal has a type, that type is universal_integer.
> I believe the contingent version is not the meaning.

Yes.  Every integer literal has type univ_int.

>...The ARM
> statement is written in unconditional language.  "The type of an
> integer literal" identifies the unique type associated with that
> integer literal and implies that there is always such a type.  The
> contingent version of this sentence would be "The type of an integer
> literal, if any, is universal_integer."  But that's not what it says.
>
> Hence both 'm' and 'm+1' have a type, and that that type is
> universal_integer.  By induction, universal_integer has no upper
> bound.

Sure.  But I don't see the need for all this song and dance,
since AARM-3.5.4 says:

8     The set of values for a signed integer type is the (infinite) set of
mathematical integers[, though only values of the base range of the type are
fully supported for run-time operations]. The set of values for a modular
integer type are the values from 0 to one less than the modulus, inclusive.

We all know there are an infinite number of integers, so why did
you want to prove it?  Universal_integer is not special in this
regard.  And for compile time (static) calculations, Ada places
no limit on the size of integers.

> On Apr 21, 8:08 am, Robert A Duff <bobd...@shell01.TheWorld.com>
> wrote:
>> The expression 'm+1' is certainly NOT a literal -- it's a function
>> call, passing an identifier and a literal as the actual parameters.
>
> I redid the argument to get rid of this ambiguity.  Admittedly I had
> not distinguished addition on {\bb N} and addition on Ada types.  My
> argument doesn't rely upon addition on any Ada type.

OK, I see.

But you could rely on integer addition (for static values of type
root_integer, for example).

>> Universal_integers can be
>> implicitly converted to various integer types.
>
> This was the whole point of the discussion--why such implicit
> conversions do not break the type system.  It's not like integers are
> a tagged type.
>
>> type My_Int is range 1..100;
>> Y : constant My_Int := 1 + 1; -- The "+" of My_Int is called.
>>                               -- Y is of type My_Int.
>
> Are there other places in Ada when the context of an operation
> determines the type of the operands of the function and thus also the
> function signature?

Overload resolution always takes the context into account,
for function calls.  Nothing special about "+" in that regard.
If you say:

    P(Param => F(X));

Then the type of Param helps determine which F is called (if there are
many functions called F that are directly visible).  The type of X also
helps determine which F is called -- and there might be several
overloaded X's.  There might also be several P's, some of which have
a Param.

> Context-dependent function selection need not break correctness of a
> program, even when there's ambiguity in what function might be
> selected (non-deterministic execution). The conditions for this to
> work are implicitly present with integer types.

Seems like "need not break" isn't good enough -- I want to prove that it
"does not break".  There could be a user-defined "+".

>...I believe it's
> possible to make them explicit for arbitrary types.

Hmm.  I guess I need an example to see what you're getting at.
Choosing which function to call nondeterministically seems
like an Obviously Bad Idea, to me, so perhaps I don't understand
what you mean.

- Bob

Re: Ada.Strings.Bounded

[Eric Hughes]

On Apr 21, 12:04 pm, Robert A Duff <bobd...@shell01.TheWorld.com>
wrote:
> We all know there are an infinite number of integers, so why did
> you want to prove it?

The question was not about {\bb N}, but about universal_integer, which
two things are not _a priori_ the same thing.

> Sure.  But I don't see the need for all this song and dance,
> since AARM-3.5.4 says:
>
> 8     The set of values for a signed integer type is the (infinite) set of
> mathematical integers[, though only values of the base range of the type are
> fully supported for run-time operations]. The set of values for a modular
> integer type are the values from 0 to one less than the modulus, inclusive.

The argument was being made against the counter-assertion that
universal_integer is an ordinary integer type and thus has a finite
range.  And I wanted to make that argument from normative sources, not
from commentary.

> But you could rely on integer addition (for static values of type
> root_integer, for example).

Could I?  I'm not so sure.  If root_integer is a range, as ordinary
defined integer types are, then "+" is a partial function and not a
total one, breaking the argument.

Bob's example:
> type My_Int is range 1..100;
> Y : constant My_Int := 1 + 1; -- The "+" of My_Int is called.
>                               -- Y is of type My_Int.

Me:
> > Are there other places in Ada when the context of an operation
> > determines the type of the operands of the function and thus also the
> > function signature?

> Overload resolution always takes the context into account,
> for function calls.  Nothing special about "+" in that regard.
> If you say:
>
>     P(Param => F(X));
>
> Then the type of Param helps determine which F is called

OK.  Somehow I had missed the fact that Ada does overload resolution
based on assignment context.  So I read up on it in more detail.
Pardon me if I've missed something in the foregoing.

The overload resolution in the present example, though, doesn't seem
unique.  Could not "+" resolve to the "+" of root_integer?  It seems
to pass all of the requirements.  To test this, I wrote the following
three lines of code and ran them through GNAT:
    -- (Example A)
    Z0 : constant := Integer'Last - 1 ;
    type Z is range 0 .. Z0 ;
    B : constant Z := ( Z0 + 1 ) - 1 ;
GNAT compiled it without a problem and it ran without error.  The
following program, however, did neither:
    -- (Example B)
    Z0 : constant := Integer'Last - 1 ;
    type Z is range 0 .. Z0 ;
    C : constant Z := Z0 + 1 ;
GNAT gave a warning that a constraint error would be raised and indeed
running it raised one.  Now I raise the upper bound by one:
    -- (Example C)
    Z0 : constant := Integer'Last ;
    type Z is range 0 .. Z0 ;
    B : constant Z := ( Z0 + 1 ) - 1 ;
GNAT compiles this one fine and runs fine, just like Example A.
    -- (Example D)
    Z0 : constant := Integer'Last ;
    type Z is range 0 .. Z0 ;
    C : constant Z := Z0 + 1 ;
GNAT says "static expression fails Constraint_Check" and does not
compile.  Let's raise the upper bound one last time:
    -- (Example E)
    Z0 : constant := Integer'Last + 1 ;
    type Z is range 0 .. Z0 ;
    B : constant Z := ( Z0 + 1 ) - 1 ;
Just fine, as usual.
    -- (Example F)
    Z0 : constant := Integer'Last + 1 ;
    type Z is range 0 .. Z0 ;
    C : constant Z := Z0 + 1 ;
GNAT gives the same warning as example B.

As an aside, GNAT is clearly doing something odd.  Of the three
declarations of "C", you have two warnings and one error, not the
same.  I'm not even sure that's a defect.

The real point, though, is that it just can't be true that the
addition and subtraction in examples A and C are those of type Z.  If
this were true, the expression
    ( Z0 + 1 ) - 1
should translate to something like this:
    Z_subtract( Z_add( Z0, 1 ), 1 )
If that were the case, then the Z_add expression should raise a
constraint error.  It doesn't.  Maybe this is a GNAT defect.  It seems
just as likely that overload resolution is taking the addition and
subtraction of root_integer.

And then I had an inspiration:
    -- (Example G)
    Z0 : constant := Long_Long_Integer'Last ;
    type Z is range 0 .. Z0 ;
    B : constant Z := ( Z0 + 1 ) - 1 ;
    -- (Example H)
    Z0 : constant := Long_Long_Integer'Last + 1 ;
    type Z is range 0 .. Z0 ;
    B : constant Z := ( Z0 + 1 ) - 1 ;
Now we've hit the GNAT implementation limit.  Example H, finally,
fails to compile because "integer type definition bounds out of
range".  (I don't like this message because it's not clear that an
internal limit has been exceeded.)  Example G, however, compiles and
runs just fine.  Example G shows that, at least in this example, it's
doing arithmetic on universal_integer, because there's no other type
internally that it could be using.

> Choosing which function to call nondeterministically seems
> like an Obviously Bad Idea, to me, so perhaps I don't understand
> what you mean.

All the above examples seem to indicate that GNAT, at least, is
resolving overloaded addition operators.  The overload is between the
declared type, root_integer (or something like it), and possibly even
universal_integer.  With other types, ones where there is no universal
type, this would be an illegal ambiguity.  So it seems that GNAT is
nondeterministically resolving them.

It works here because all these types are compatible for such
resolution.  It doesn't cause any problems.  This is what I believe
could be declared explicitly.

Eric

Re: Ada.Strings.Bounded

[Adam Beneschan]

On Apr 21, 5:19 pm, Eric Hughes <eric....@gmail.com> wrote:

> OK.  Somehow I had missed the fact that Ada does overload resolution
> based on assignment context.  So I read up on it in more detail.
> Pardon me if I've missed something in the foregoing.
>
> The overload resolution in the present example, though, doesn't seem
> unique.  Could not "+" resolve to the "+" of root_integer?  It seems
> to pass all of the requirements.  To test this, I wrote the following
> three lines of code and ran them through GNAT:
>     -- (Example A)
>     Z0 : constant := Integer'Last - 1 ;
>     type Z is range 0 .. Z0 ;
>     B : constant Z := ( Z0 + 1 ) - 1 ;
> GNAT compiled it without a problem and it ran without error.  The
> following program, however, did neither:
>     -- (Example B)
>     Z0 : constant := Integer'Last - 1 ;
>     type Z is range 0 .. Z0 ;
>     C : constant Z := Z0 + 1 ;
> GNAT gave a warning that a constraint error would be raised and indeed
> running it raised one.  Now I raise the upper bound by one:
>     -- (Example C)
>     Z0 : constant := Integer'Last ;
>     type Z is range 0 .. Z0 ;
>     B : constant Z := ( Z0 + 1 ) - 1 ;
> GNAT compiles this one fine and runs fine, just like Example A.
>     -- (Example D)
>     Z0 : constant := Integer'Last ;
>     type Z is range 0 .. Z0 ;
>     C : constant Z := Z0 + 1 ;
> GNAT says "static expression fails Constraint_Check" and does not
> compile.  Let's raise the upper bound one last time:
>     -- (Example E)
>     Z0 : constant := Integer'Last + 1 ;
>     type Z is range 0 .. Z0 ;
>     B : constant Z := ( Z0 + 1 ) - 1 ;
> Just fine, as usual.
>     -- (Example F)
>     Z0 : constant := Integer'Last + 1 ;
>     type Z is range 0 .. Z0 ;
>     C : constant Z := Z0 + 1 ;
> GNAT gives the same warning as example B.
>
> As an aside, GNAT is clearly doing something odd.  Of the three
> declarations of "C", you have two warnings and one error, not the
> same.  I'm not even sure that's a defect.
>
> The real point, though, is that it just can't be true that the
> addition and subtraction in examples A and C are those of type Z.  If
> this were true, the expression
>     ( Z0 + 1 ) - 1
> should translate to something like this:
>     Z_subtract( Z_add( Z0, 1 ), 1 )
> If that were the case, then the Z_add expression should raise a
> constraint error.  It doesn't.  Maybe this is a GNAT defect.  It seems
> just as likely that overload resolution is taking the addition and
> subtraction of root_integer.

See 4.9(33).  I'm not sure it applies in this case, though, since the
root_integer operations will be preferred (see below).  But note that
this compiles and will not cause Constraint_Error to be raised:

   A1 : constant Integer := Integer'Last;
   A2 : constant Integer := (A1 + 1) - 1;


> And then I had an inspiration:
>     -- (Example G)
>     Z0 : constant := Long_Long_Integer'Last ;
>     type Z is range 0 .. Z0 ;
>     B : constant Z := ( Z0 + 1 ) - 1 ;
>     -- (Example H)
>     Z0 : constant := Long_Long_Integer'Last + 1 ;
>     type Z is range 0 .. Z0 ;
>     B : constant Z := ( Z0 + 1 ) - 1 ;
> Now we've hit the GNAT implementation limit.  Example H, finally,
> fails to compile because "integer type definition bounds out of
> range".  (I don't like this message because it's not clear that an
> internal limit has been exceeded.)  Example G, however, compiles and
> runs just fine.  Example G shows that, at least in this example, it's
> doing arithmetic on universal_integer, because there's no other type
> internally that it could be using.
>
> > Choosing which function to call nondeterministically seems
> > like an Obviously Bad Idea, to me, so perhaps I don't understand
> > what you mean.
>
> All the above examples seem to indicate that GNAT, at least, is
> resolving overloaded addition operators.  The overload is between the
> declared type, root_integer (or something like it), and possibly even
> universal_integer.  With other types, ones where there is no universal
> type, this would be an illegal ambiguity.  So it seems that GNAT is
> nondeterministically resolving them.

There's nothing nondeterministic about this.  See 8.6(29).

I can't follow your argument so I have no idea whether these points
affect it or not.  But you do seem to have made at least a couple
mistakes about the language.

                                 -- Adam

Re: Ada.Strings.Bounded

[Adam Beneschan]

On Apr 21, 5:49 pm, Adam Beneschan <a...@irvine.com> wrote:

> >     -- (Example C)
> >     Z0 : constant := Integer'Last ;
> >     type Z is range 0 .. Z0 ;
> >     B : constant Z := ( Z0 + 1 ) - 1 ;

> > All the above examples seem to indicate that GNAT, at least, is
> > resolving overloaded addition operators.  The overload is between the
> > declared type, root_integer (or something like it), and possibly even
> > universal_integer.  With other types, ones where there is no universal
> > type, this would be an illegal ambiguity.  So it seems that GNAT is
> > nondeterministically resolving them.
>
> There's nothing nondeterministic about this.  See 8.6(29).

I goofed.  This rule doesn't actually apply in this case, since the
expected type of the expression is a user-defined integer type, which
isn't compatible with root_integer.  (If the expected type of an
expression is a specific integer type that isn't root_integer, the
expression can be of that type or it can be universal_integer, but it
can't be root_integer.)  I've sometimes made the mistake of confusing
root_ and universal_integer, and I got sloppy here.

But I think that actually makes the point even moreso that there's no
nondeterminism involved.  The expected type is Z; therefore, in
example C, the only possible meaning for "-" is the function that
takes two arguments of type Z and returns Z.  That, in turn, applies
to "+".  So it's 100% clear from the language rules what functions are
called by this expression.  The reason it doesn't raise
Constraint_Error is 4.9(33), as I mentioned earlier.

                                 -- Adam

Re: Ada.Strings.Bounded

[Eric Hughes]

On Apr 21, 7:02 pm, Adam Beneschan <a...@irvine.com> wrote:
> The expected type is Z; therefore, in
> example C, the only possible meaning for "-" is the function that
> takes two arguments of type Z and returns Z.  That, in turn, applies
> to "+". So it's 100% clear from the language rules what functions are
> called by this expression.  The reason it doesn't raise
> Constraint_Error is 4.9(33), as I mentioned earlier.

OK.  But then what's the type of the subexpression "( Z0 + 1 )" within
the static expression "( Z0 + 1 ) - 1"?  It can't be of type Z, since
it's outside the bounds of type Z.  And the addition chosen can't be
the same addition as the declared one, which returns Z, and that
subexpression returns something that's not in Z.  The addition used
here has a different signature.

It seems that the overload resolution rules don't apply when
universal_integer is involved.  This seems a pretty obvious
consequence of 4.9(33).

Eric

Re: Ada.Strings.Bounded

[Robert A Duff]

Eric Hughes <eric.eh9@gmail.com> writes:

> On Apr 21, 7:02 pm, Adam Beneschan <a...@irvine.com> wrote:
>> The expected type is Z; therefore, in
>> example C, the only possible meaning for "-" is the function that
>> takes two arguments of type Z and returns Z.  That, in turn, applies
>> to "+". So it's 100% clear from the language rules what functions are
>> called by this expression.  The reason it doesn't raise
>> Constraint_Error is 4.9(33), as I mentioned earlier.
>
> OK.  But then what's the type of the subexpression "( Z0 + 1 )" within
> the static expression "( Z0 + 1 ) - 1"?  It can't be of type Z, since
> it's outside the bounds of type Z.  And the addition chosen can't be
> the same addition as the declared one, which returns Z, and that
> subexpression returns something that's not in Z.

Ah, I see what might be confusing you.  You need to understand the
difference between types and subtypes.  When you say:

    type Z is range ...;

you are declaring a type and a subtype (the "first subtype").  The name
Z refers to the firts subtype, and has the specified range.  There is no
way to refer to the type by name.  Strange, but true!  When I say "the
type Z", I really mean "the type whose first subtype is Z".
The RM sometimes uses the term "the type of subtype Z".

The operators of the type Z can return results outside the range of Z.
                     ^^^^^^
                     note sloppy/informal wording!

Consider:

    type T is range 1..10;
    A : T := Read_From_Keyboard;
    B : T := Read_From_Keyboard;
    C : T := (A - 1) + B;

Imagine Read_From_Keyboard reads a number between 1 and 10,
and suppose we happen to get A = 1, and B = 5.  C must equal
5, even though the intermediate result A-1 is out of range
for T.

The "base subtype", called T'Base, has an implementation-defined range,
which covers at least -10..10, but might well be something like
-2**31..2**31-1.  At run time, operators will get the right
answer if it's in the base range.  If it's outside the base
range, the compiler is ALLOWED to get the right answer, but
is also allowed to overflow.

>...  The addition used
> here has a different signature.
>
> It seems that the overload resolution rules don't apply when
> universal_integer is involved.  This seems a pretty obvious
> consequence of 4.9(33).

No, it's false, and is therefore obviously NOT a consequence of
4.9(33)!  ;-)

There are some special rules for univ_int (mainly, the implicit
conversions), but the rules apply.

- Bob

Re: Ada.Strings.Bounded

[Eric Hughes]

On Apr 21, 6:49 pm, Adam Beneschan <a...@irvine.com> wrote:
> See 4.9(33).

Oh.  OK.  For those insufficiently motivated to look at this section,
it says that static expressions are evaluated exactly, without
performing overflow checks.  To me, that word "exactly" means that
static expressions are evaluated as universal_integer, since that's
the only way to get them defined exactly.

Previously, Bob Duff had said:
> An integer literal has type universal_integer, as you said, but
> universal_integer has no "+" operator.  There is a "+" for root_integer,
> and also for user-defined integer types.  Universal_integers can be
> implicitly converted to various integer types.

Something's got to give here.  I see the following possibilities:
1) universal_integer actually does have a "+" operator.  It would only
be available at compile time, since there's no way to declare a
variable of type universal_integer.
2) The addition chosen is the context-dependent one, as for dynamic
expressions, but when overflow happens, the result is magically
converted to universal_integer.
3) The addition of the ordinary type is tried with the base type.  If
it overflows, a bigger type is tried, and so on up to
universal_integer, which will always succeed.
4) The evaluation happens purely mathematically, without regard for
the Ada type system.
5) There are different versions of the type and its addition operation
for static and run-time use.  The static ones have arbitrarily large
capacity and exact arithmetic.

I'm sure my imagination is not large enough to guess at all the
possibilities.  What's going on here, really?

Eric

Re: Ada.Strings.Bounded

[Robert A Duff]

Eric Hughes <eric.eh9@gmail.com> writes:

> On Apr 21, 6:49 pm, Adam Beneschan <a...@irvine.com> wrote:
>> See 4.9(33).
>
> Oh.  OK.  For those insufficiently motivated to look at this section,
> it says that static expressions are evaluated exactly, without
> performing overflow checks.

Right.

>...To me, that word "exactly" means that
> static expressions are evaluated as universal_integer, since that's
> the only way to get them defined exactly.

No, that does not follow.  It says they are evaluated exactly,
which means the compiler must get the right answer, according
to the normal rules of integer math.  That has nothing to do
with univ_int.

> Previously, Bob Duff had said:
>> An integer literal has type universal_integer, as you said, but
>> universal_integer has no "+" operator.  There is a "+" for root_integer,
>> and also for user-defined integer types.  Universal_integers can be
>> implicitly converted to various integer types.
>
> Something's got to give here.  I see the following possibilities:
> 1) universal_integer actually does have a "+" operator.

It does not.  It doesn't need them, since univ_int can be implicitly
converted to any other integer type.  And if univ_int had operators,
lots of useful expressions would be ambiguous, and therefore illegal!

>...It would only
> be available at compile time, since there's no way to declare a
> variable of type universal_integer.

However, there are some fairly obscure ways to write nonstatic
expressions of type universal_integer, and pass those to
the operators of type root_integer, at run time.  These will
get overflows -- Constraint_Error if the value doesn't fit in
the base range of root_int (the 64-bit range, for GNAT).

> 2) The addition chosen is the context-dependent one, as for dynamic
> expressions, but when overflow happens, the result is magically
> converted to universal_integer.

No.

> 3) The addition of the ordinary type is tried with the base type.  If
> it overflows, a bigger type is tried, and so on up to
> universal_integer, which will always succeed.

No.

> 4) The evaluation happens purely mathematically, without regard for
> the Ada type system.

Yes.  That is, the "+" operator of all types behaves that way in static
expressions.

> 5) There are different versions of the type and its addition operation
> for static and run-time use.  The static ones have arbitrarily large
> capacity and exact arithmetic.

Sort of.  I wouldn't call it "different versions of the type", though.
The operators behave differently in static expressions than at run
time.  There's nothing special about the root_int ops in this regard
(and there are no univ_int ops).

> I'm sure my imagination is not large enough to guess at all the
> possibilities.  What's going on here, really?

I hope my comments above answer that question!  ;-)

- Bob

Re: Ada.Strings.Bounded

[Robert A Duff]

Eric Hughes <eric.eh9@gmail.com> writes:

> On Apr 21, 12:04 pm, Robert A Duff <bobd...@shell01.TheWorld.com>
> wrote:
>> We all know there are an infinite number of integers, so why did
>> you want to prove it?
>
> The question was not about {\bb N}, but about universal_integer, which
> two things are not _a priori_ the same thing.
>
>> Sure.  But I don't see the need for all this song and dance,
>> since AARM-3.5.4 says:
>>
>> 8     The set of values for a signed integer type is the (infinite) set of
>> mathematical integers[, though only values of the base range of the type are
>> fully supported for run-time operations]. The set of values for a modular
>> integer type are the values from 0 to one less than the modulus, inclusive.
>
> The argument was being made against the counter-assertion that
> universal_integer is an ordinary integer type and thus has a finite
> range.  And I wanted to make that argument from normative sources, not
> from commentary.

The above-quoted paragraph 3.5.4(8) is normative.  It comes right out
and says in plain language exactly what you were trying to prove in a
circuitous manner -- that the the set of values is infinite.

Note that it does not say anything special about root_int or univ_int.
It applies to ALL signed integer types, including user-defined ones.

You should read about static expressions, which will clear up some of
your confusings below.  You should also make sure you understand the
difference between overflow checks and range checks.

Also, there's a rule (which I'm too lazy to look up right now),
which says that at run time, the compiler is always allowed to get the
right answer.

So for a static expression that is outside the base range of its type,
the compiler must calculate the right answer.  For a non-static
expression, the compiler may raise Constraint_Error if the value is
outside the base range, or it may choose to get the right mathematical
answer.  It can even roll dice to decide whether to get the right
answer.

>> But you could rely on integer addition (for static values of type
>> root_integer, for example).
>
> Could I?  I'm not so sure.  If root_integer is a range, as ordinary
> defined integer types are, then "+" is a partial function and not a
> total one, breaking the argument.

No, the semantics of "+" are different depending on whether the
expression is static.  NOT depending on whether the type is root_int.
For static expressions, "+" is not a partial function.

> Bob's example:
>> type My_Int is range 1..100;
>> Y : constant My_Int := 1 + 1; -- The "+" of My_Int is called.
>>                               -- Y is of type My_Int.
>
> Me:
>> > Are there other places in Ada when the context of an operation
>> > determines the type of the operands of the function and thus also the
>> > function signature?
>
>> Overload resolution always takes the context into account,
>> for function calls.  Nothing special about "+" in that regard.
>> If you say:
>>
>>     P(Param => F(X));
>>
>> Then the type of Param helps determine which F is called
>
> OK.  Somehow I had missed the fact that Ada does overload resolution
> based on assignment context.  So I read up on it in more detail.
> Pardon me if I've missed something in the foregoing.
>
> The overload resolution in the present example, though, doesn't seem
> unique.  Could not "+" resolve to the "+" of root_integer?

No.  The "+" of root_integer returns root_integer, and there is no
implicit conversion from root_integer to My_Int, so the "+" of
root_integer can't be used in the above example.

>...It seems
> to pass all of the requirements.  To test this, I wrote the following
> three lines of code and ran them through GNAT:
>     -- (Example A)
>     Z0 : constant := Integer'Last - 1 ;
>     type Z is range 0 .. Z0 ;
>     B : constant Z := ( Z0 + 1 ) - 1 ;
> GNAT compiled it without a problem and it ran without error.  The
> following program, however, did neither:
>     -- (Example B)
>     Z0 : constant := Integer'Last - 1 ;
>     type Z is range 0 .. Z0 ;
>     C : constant Z := Z0 + 1 ;
> GNAT gave a warning that a constraint error would be raised and indeed
> running it raised one.  Now I raise the upper bound by one:
>     -- (Example C)
>     Z0 : constant := Integer'Last ;
>     type Z is range 0 .. Z0 ;
>     B : constant Z := ( Z0 + 1 ) - 1 ;
> GNAT compiles this one fine and runs fine, just like Example A.
>     -- (Example D)
>     Z0 : constant := Integer'Last ;
>     type Z is range 0 .. Z0 ;
>     C : constant Z := Z0 + 1 ;
> GNAT says "static expression fails Constraint_Check" and does not
> compile.  Let's raise the upper bound one last time:
>     -- (Example E)
>     Z0 : constant := Integer'Last + 1 ;
>     type Z is range 0 .. Z0 ;
>     B : constant Z := ( Z0 + 1 ) - 1 ;
> Just fine, as usual.
>     -- (Example F)
>     Z0 : constant := Integer'Last + 1 ;
>     type Z is range 0 .. Z0 ;
>     C : constant Z := Z0 + 1 ;
> GNAT gives the same warning as example B.
>
> As an aside, GNAT is clearly doing something odd.

It is obeying the language rules.  You might say the language rules are
odd, and I would agree.  I don't much like the fact that static
expressions have subtly different evaluation rules from normal
run-time calculations.

>...Of the three
> declarations of "C", you have two warnings and one error, not the
> same.  I'm not even sure that's a defect.

It's not a defect in GNAT -- read the section on static expressions.

> The real point, though, is that it just can't be true that the
> addition and subtraction in examples A and C are those of type Z.  If
> this were true, the expression
>     ( Z0 + 1 ) - 1
> should translate to something like this:
>     Z_subtract( Z_add( Z0, 1 ), 1 )
> If that were the case, then the Z_add expression should raise a
> constraint error.

No.  Static expressions cannot overflow.  The "+" used in those two
examples is that of type Z.

Note that the "-" that occurs in some of your declarations of Z0 is the
"-" on root_integer.  Look at the special rules for named numbers in
3.3.2, and the special preference rule in 8.6(29).  But 8.6(29) has
nothing to do with the B and C constants in your examples.

>...It doesn't.  Maybe this is a GNAT defect.

No.

>...It seems
> just as likely that overload resolution is taking the addition and
> subtraction of root_integer.

No, as I explained, that "+" and "-" return the wrong type!

> And then I had an inspiration:
>     -- (Example G)
>     Z0 : constant := Long_Long_Integer'Last ;
>     type Z is range 0 .. Z0 ;
>     B : constant Z := ( Z0 + 1 ) - 1 ;
>     -- (Example H)
>     Z0 : constant := Long_Long_Integer'Last + 1 ;
>     type Z is range 0 .. Z0 ;
>     B : constant Z := ( Z0 + 1 ) - 1 ;
> Now we've hit the GNAT implementation limit.

Right.  Note that it complains about type Z, not about the named number
Z0.  GNAT is not allowed to complain about Z0 in Example H.

>...Example H, finally,
> fails to compile because "integer type definition bounds out of
> range".  (I don't like this message because it's not clear that an
> internal limit has been exceeded.)

A fair complaint.

>...Example G, however, compiles and
> runs just fine.  Example G shows that, at least in this example, it's
> doing arithmetic on universal_integer, because there's no other type
> internally that it could be using.

No.  It is using the "+" on Z.  There is no "+" on universal_integer,
and the one on root_integer has the wrong result type.

>> Choosing which function to call nondeterministically seems
>> like an Obviously Bad Idea, to me, so perhaps I don't understand
>> what you mean.
>
> All the above examples seem to indicate that GNAT, at least, is
> resolving overloaded addition operators.  The overload is between the
> declared type, root_integer (or something like it), and possibly even
> universal_integer.  With other types, ones where there is no universal
> type, this would be an illegal ambiguity.  So it seems that GNAT is
> nondeterministically resolving them.

No.  There is no nondeterministic overload resolution in Ada.

> It works here because all these types are compatible for such
> resolution.  It doesn't cause any problems.  This is what I believe
> could be declared explicitly.

Well, in the last sentence, "This" refers to some incorrect
interpretations of some (annoyingly complicated) Ada language rules,
so I still don't know what you mean (sorry).

- Bob

Re: Ada.Strings.Bounded

[Dmitry A. Kazakov]

On Tue, 22 Apr 2008 11:41:29 -0400, Robert A Duff wrote:

> For static expressions, "+" is not a partial function.

If compilable. The following should break GNAT GPL 2007:

with Ada.Text_IO;  use Ada.Text_IO;

procedure Test_Int is
   L : constant Integer := Integer'Last;
   M : constant Integer :=
(L + 
   L*L*L*L ... *L  -- 40 times per line
 *L*L*L*L ... *L 
 ...                    -- 200 lines should be enough
 *L*L*L*L ... *L 
)
-  L*L*L*L ... *L  -- Same as above
 *L*L*L*L ... *L 
 ...
 *L*L*L*L ... *L 
;
begin
   Put_Line (Integer'Image (M));
end Test_Int;

Here we have approximately L + 2**(32*8000) - 2**(32*8000).
-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

Re: Ada.Strings.Bounded

[Samuel Tardieu]

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

Dmitry> If compilable. The following should break GNAT GPL 2007:

It doesn't break GCC 4.4.0:

% gnatmake -g -O2 t
gcc -c -g -O2 t.adb
gnatbind -x t.ali
gnatlink t.ali -g

% ./t
 2147483647

The file I used is on http://www.rfc1149.net/tmp/t.adb if you want to
try it yourself :)

  Sam
-- 
Samuel Tardieu -- sam@rfc1149.net -- http://www.rfc1149.net/

Re: Ada.Strings.Bounded

[Dmitry A. Kazakov]

On Tue, 22 Apr 2008 20:26:31 +0200, Samuel Tardieu wrote:

>>>>>> "Dmitry" == Dmitry A Kazakov <mailbox@dmitry-kazakov.de> writes:
> 
> Dmitry> If compilable. The following should break GNAT GPL 2007:
> 
> It doesn't break GCC 4.4.0:
> 
> % gnatmake -g -O2 t
> gcc -c -g -O2 t.adb
> gnatbind -x t.ali
> gnatlink t.ali -g
> 
> % ./t
>  2147483647
> 
> The file I used is on http://www.rfc1149.net/tmp/t.adb if you want to
> try it yourself :)

Well, it seems I miscalculated the number of lines. But actually not too
much, I have added 30 lines to each summand and got the infamous: GNAT BUG
DETECTED ... GPL 2007 (20070405-41) (i586-pc-mingw32msv) Storage_Error heap
exhausted [*]... However it is not a bug of course. In simpler cases like:

   M : constant := 2**1_000_000;

GNAT gives reasonable: "static value too large, capacity exceeded"

---------------
*  In case that would not help (I don't know how many terabytes of memory
you have (:-)), double the number of lines in each summand. Continue so
until the Easter egg reveal itself...

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

Re: Ada.Strings.Bounded

[Eric Hughes]

On Apr 22, 9:41 am, Robert A Duff <bobd...@shell01.TheWorld.com>
wrote:
> The above-quoted paragraph 3.5.4(8) is normative.  It comes right out
> and says in plain language exactly what you were trying to prove in a
> circuitous manner -- that the the set of values is infinite.

Here's the relevant sentence in 3.5.4(8) again:
> The set of values for a signed integer type is the (infinite) set
> of mathematical integers, though only values of the base range of
> the type are fully supported for run-time operations.

So now wait.  When I declare
    type X is range 0 .. 99 ;
does that mean that the value 100 is a value of type X?  Because how
that definition reads in any sort of facially-reasonable way is that
100 is not a value of type X.

> Note that it does not say anything special about root_int or univ_int.
> It applies to ALL signed integer types, including user-defined ones.

Apparently so.

And so now I have developed a Strong Opinion.  This is a travesty.  A
probably-irredeemable travesty. This is so completely counter-
intuitive that I have a hard time believing that competent people came
up with this way of writing the definition.  It's unnecessary.  There
are far better ways of defining this, and they don't break any
existing syntax.

I'm out.  Completely out.  Everything I've said has been predicated on
the assumption that the set of values of a type is what the
declaration says it is, rather than having values that cannot be
assigned to a variable of that type.  In my opinion this means that
assignment and variable definition are broken.  I don't even care what
the details are at this point.

Eric

Re: Ada.Strings.Bounded

[Dmitry A. Kazakov]

On Tue, 22 Apr 2008 11:47:05 -0700 (PDT), Eric Hughes wrote:

> And so now I have developed a Strong Opinion.  This is a travesty.  A
> probably-irredeemable travesty. This is so completely counter-
> intuitive that I have a hard time believing that competent people came
> up with this way of writing the definition.  It's unnecessary.  There
> are far better ways of defining this, and they don't break any
> existing syntax.
> 
> I'm out.  Completely out.  Everything I've said has been predicated on
> the assumption that the set of values of a type is what the
> declaration says it is, rather than having values that cannot be
> assigned to a variable of that type.  In my opinion this means that
> assignment and variable definition are broken.  I don't even care what
> the details are at this point.

Well, there are reasons why:

1. Integer types are thought as models for mathematical numbers. The range
is a constraint put on the set value.

2. This allows to skip a lot of checks when the implementation type is
larger than the range. Otherwise, the compiler would be forced to check
each intermediate result in order to raise Constraint_Error.

3. It is rather intuitive, normally one expects to get the right result,
independently on the intermediate results. Moreover, the compiler might
optimize the code choosing a different computation path, so long the result
is mathematically correct.

4. It makes programming less tedious, when values close to the range ends
are involved.

The only real disadvantage I see, is that the program might get
non-portable if programmers actively exploit 4.

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

Re: Ada.Strings.Bounded

[Robert A Duff]

Eric Hughes <eric.eh9@gmail.com> writes:

> On Apr 22, 9:41 am, Robert A Duff <bobd...@shell01.TheWorld.com>
> wrote:
>> The above-quoted paragraph 3.5.4(8) is normative.  It comes right out
>> and says in plain language exactly what you were trying to prove in a
>> circuitous manner -- that the the set of values is infinite.
>
> Here's the relevant sentence in 3.5.4(8) again:
>> The set of values for a signed integer type is the (infinite) set
>> of mathematical integers, though only values of the base range of
>> the type are fully supported for run-time operations.
>
> So now wait.  When I declare
>     type X is range 0 .. 99 ;
> does that mean that the value 100 is a value of type X?

Yes, if you're using "type X" as I explained in my other message to mean
"the type whose first subtype is X".

Subtype X has the range you expect (0..99).  But it has an underlying
type that has all the integer values, including 100.

Note that you could say:

    subtype S is X'Base range 0..100;

>...Because how
> that definition reads in any sort of facially-reasonable way is that
> 100 is not a value of type X.

100 is not a value of SUBtype X.

>> Note that it does not say anything special about root_int or univ_int.
>> It applies to ALL signed integer types, including user-defined ones.
>
> Apparently so.
>
> And so now I have developed a Strong Opinion.  This is a travesty.

I agree it's confusing.  But "travesty" is too strong.  In practise,
none of this matters much.

Don't you want to be able to say "(Blah + 1) mod 99" without overflow
(where Blah is of subtype X)?

- Bob

Re: Ada.Strings.Bounded

[Eric Hughes]

On Apr 22, 1:41 pm, Robert A Duff <bobd...@shell01.TheWorld.com>
wrote:
> I agree it's confusing.  But "travesty" is too strong.  In practise,
> none of this matters much.

Definitions matters if you wish to extend them.  These definitions are
not extensible.  I still think it's a travesty.

> Don't you want to be able to say "(Blah + 1) mod 99" without overflow
> (where Blah is of subtype X)?

I can do it without those definitions.

Eric

Re: Ada.Strings.Bounded

[christoph.grein]

When you declare a type

  type T is range 1 .. 10;

the name T denotes the first subtype of the anonymous type of T (the
RM uses T in italics to denote this type, e.g. in 4.5.3, and this type
has the infinite set of mathematical integers).
Thus 11 *is* a value of the type of T (in sloppy language, the type
T).

The static named number

  S: constant := Integer’Last + Integer’Last;

uses the "+" of Integer without overflow and converts the result to
Universal_Integer. Therefore

  S: constant := Integer’Last + Long_Integer’Last;

is not allowed because it mixes two different types, but

  T: constant := Long_Integer’Last;
  U: constant := S + T;

is allowed, the "+" in the last expression being the one of
root_integer.

Re: Ada.Strings.Bounded

[christoph.grein]

  S: constant := Integer’Last + Integer’Last; -- "+" of Integer
  T: constant := Long_Integer’Last + 1;       -- "+" of Long_Integer
  U: constant := S + T;                       -- "+" of root_integer
  V: constant := S + Long_Integer’Last;       -- "+" of Long_Integer

All of S, T, U, V are of type Universal_Integer.

Re: Ada.Strings.Bounded

[Georg Bauhaus]

Robert A Duff schrieb:

>> And so now I have developed a Strong Opinion.  This is a travesty.
> 
> I agree it's confusing.  But "travesty" is too strong.  In practise,
> none of this matters much.
> 
> Don't you want to be able to say "(Blah + 1) mod 99" without overflow
> (where Blah is of subtype X)?

Hmm, less explicit and more lazy programming is
attractive to many programmers, so just write expressions
of a type that cannot be named, just in case of integers.
But how about this:

procedure Ex is
    type E is (A, B, C);
    X: E;
begin
    X := E'pred(E'succ(C));
end Ex;

In this case there is a static constraint error. Is this
consistent with anything but the Ada LRM's exception for
"integer convenience"?

Without of course knowing why the choices were made the
way they were made for the LRM, my conclusion is that
many programmers still prefer high school ideas about
numbers over the theory of computer numbers.

Is it really inacceptable to write

   Larger_Type'(Blah + 1) mod 99;

The expression doesn't hide a secret about its
value range.

Re: Ada.Strings.Bounded

[Dmitry A. Kazakov]

On Wed, 23 Apr 2008 12:42:32 +0200, Georg Bauhaus wrote:

> But how about this:
> 
> procedure Ex is
>     type E is (A, B, C);
>     X: E;
> begin
>     X := E'pred(E'succ(C));
> end Ex;
> 
> In this case there is a static constraint error. Is this
> consistent with anything but the Ada LRM's exception for
> "integer convenience"?

But enumeration is finite. If we had extensible enumerations then it would
be reasonable to consider the set of enumeration values infinite, similarly
to signed integers.

Probably it could be possible to formalize such things by allowing the user
to describe certain properties of primitive operations. The case (A + B)
mod C relies on the group property of "+" and "mod":

   forall n   (A + nC) mod C = A mod C

There exists properties Ada compiler knows. For example:

  forall private T, (not X=Y) = (X/=Y)

But it does not know that  X - Y = X + (-Y), etc.

Also, supertyping should help. The anonymous types before the first named
subtype is nothing but a supertype, if you wanted to expose it. In the
cases when the user defines a primitive operation, the stuff like above
could to be defined in terms of the supertype or the class of
(contravariant).

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

Re: Ada.Strings.Bounded

[christoph.grein]

> procedure Ex is
>     type E is (A, B, C);
>     X: E;
> begin
>     X := E'pred(E'succ(C));
> end Ex;

You can have this:

  type Enum is (A, B, C, D);
  type Sub is new Enum range A .. C;

  Sub'Succ (Sub'Last) = D
  Sub'Pred (Sub'Succ (Sub'Last)) = C

Sub'Base has range A .. D.

Re: Ada.Strings.Bounded

[Georg Bauhaus]

christoph.grein@eurocopter.com schrieb:
>> procedure Ex is
>>     type E is (A, B, C);
>>     X: E;
>> begin
>>     X := E'pred(E'succ(C));
>> end Ex;
> 
> You can have this:
> 
>   type Enum is (A, B, C, D);
>   type Sub is new Enum range A .. C;
> 
>   Sub'Succ (Sub'Last) = D
>   Sub'Pred (Sub'Succ (Sub'Last)) = C
> 
> Sub'Base has range A .. D.

Yes, but extending the set of values only shifts the
(theoretical) problem of 'Succ by one inductive step.
Once we forget about the type of unrepresentable numbers
the problem ceases to exist, I think.

Re: Ada.Strings.Bounded

[Adam Beneschan]

On Apr 23, 3:42 am, Georg Bauhaus <rm.dash-bauh...@futureapps.de>
wrote:

> Without of course knowing why the choices were made the
> way they were made for the LRM, my conclusion is that
> many programmers still prefer high school ideas about
> numbers over the theory of computer numbers.

Nahhh, we just want to write programs that work, and have a language
that helps prevent us from making stupid errors, but without forcing
us to waste time writing needless junk in order to have things fit
more consistently into some "theory".  Remember, "theory" is our
servant, not our master.

                                -- Adam

Re: Ada.Strings.Bounded

[(see below)]

On 23/04/2008 16:12, in article
62dde2ab-d6ad-454b-aa87-8dbc23855903@v23g2000pro.googlegroups.com, "Adam
Beneschan" <adam@irvine.com> wrote:

> On Apr 23, 3:42 am, Georg Bauhaus <rm.dash-bauh...@futureapps.de>
> wrote:
> 
>> Without of course knowing why the choices were made the
>> way they were made for the LRM, my conclusion is that
>> many programmers still prefer high school ideas about
>> numbers over the theory of computer numbers.
> 
> Nahhh, we just want to write programs that work, and have a language
> that helps prevent us from making stupid errors, but without forcing
> us to waste time writing needless junk in order to have things fit
> more consistently into some "theory".  Remember, "theory" is our
> servant, not our master.

Bravo!
-- 
Bill Findlay
<surname><forename> chez blueyonder.co.uk

Re: Ada.Strings.Bounded

[Ray Blaak]

Adam Beneschan <adam@irvine.com> writes:
> Nahhh, we just want to write programs that work, and have a language
> that helps prevent us from making stupid errors, but without forcing
> us to waste time writing needless junk in order to have things fit
> more consistently into some "theory".  Remember, "theory" is our
> servant, not our master.

Careful. That way lies the path to the dark side: dynamic typing, garbage
collection, interpreted scripts.

-- 
Cheers,                                        The Rhythm is around me,
                                               The Rhythm has control.
Ray Blaak                                      The Rhythm is inside me,
rAYblaaK@STRIPCAPStelus.net                    The Rhythm has my soul.

Re: Ada.Strings.Bounded

[Randy Brukardt]

"Georg Bauhaus" <rm.dash-bauhaus@futureapps.de> wrote in message
news:480f1298$0$6782$9b4e6d93@newsspool2.arcor-online.net...
...
> Without of course knowing why the choices were made the
> way they were made for the LRM, my conclusion is that
> many programmers still prefer high school ideas about
> numbers over the theory of computer numbers.

The reason is that the "theory" doesn't match the capabilities of actual
computer hardware.

If you required intermediate results to be checked, integer expressions
would generate 5 times as much code and run only half as fast as they do.
(I'm basing that on the code generated by Janus/Ada, and only considering
operators beyond the first in an expression. It might be possible to do a
bit better, but I've looked at the code generated by other compilers and I
don't think it is wildly different) That wouldn't be competive with other
computer languages.

You could complain that
    X := E'pred(E'succ(C));
isn't different. And indeed I'd agree: it *is* twice as big and
substantially slower than the equivalent
   X := (C + 1) - 1;
would be. It just doesn't matter much because it is rare to use more than
one attribute in an expression, while using multiple integer operators in an
expression is very common.

> Is it really inacceptable to write
>
>    Larger_Type'(Blah + 1) mod 99;
>
> The expression doesn't hide a secret about its
> value range.

There may be no such type, and optimizers transform expressions all of the
time based on the "the correct answer is always OK" rule. It may not be
necessary to evaluate the expression with a larger type. You're essentially
saying that you *don't* want the correct answer in that case, which seems
way too pedantic. I don't think that much code improvement could be done at
all with a strict rule (it's hard to do any as it as, given that overflow
checking prevents a lot of reordering that would be OK in C).

The net effect is that if you want efficient code, you have to relax the
strict rules somewhere. And Ada does that without sacrificing any safety.
(Another similar place is the "invalid" object rules, which allow compilers
to eliminate range checks so long as the value is checked before doing
anything dangerous [like array indexing].)

                                Randy.

Re: Ada.Strings.Bounded

[Adam Beneschan]

On Apr 22, 11:47 am, Eric Hughes <eric....@gmail.com> wrote:

> So now wait.  When I declare
>     type X is range 0 .. 99 ;
> does that mean that the value 100 is a value of type X?

Yes.  See 3.2.1(6).  This declaration defines both a *type* X and its
*first subtype* X.  The type X includes all integers.  The subtype X
imposes a constraint of 0..99 on that type.  When you declare

    Var : X;

and then assign something into Var, the expression's value will be
checked against the subrange 0..99, just as if you had said

    type Y is range 0..1_000_000_000;
    subtype YY is Y range 0..99;

    Var : YY;

> And so now I have developed a Strong Opinion.  This is a travesty.  A
> probably-irredeemable travesty. This is so completely counter-
> intuitive that I have a hard time believing that competent people came
> up with this way of writing the definition.  It's unnecessary.  There
> are far better ways of defining this, and they don't break any
> existing syntax.

Back on April 15, in a different thread, you said "Make the formal
standard normative, the human language expository", arguing that it
would be OK for the formal standard to be inaccessible to human
programmers.  Now, in a case where the formal standard has been made a
little bit complex in order to get the language to work they way they
wanted it to work, then you complain about it not being intuitive.  I
don't think you can have it both ways.

But I am going to complain bitterly about one thing: you are way out
of line to insinuate that the people who came up with the standard are
incompetent.  WAY out of line.  I know how much work the people who
work on the standard put into it, and how much thought they put into
making sure everything fits together and all the bases are covered
while at the same time trying to make it reasonably readable.  So even
if you don't understand why the standard's authors defined something
the way they did, you can assume there's a 99.9999% chance that there
was a darn good reason why they did it that way.  In this particular
case, I think they saw a need to support static expressions with
intermediate results that were larger than a machine integer, and the
type/subtype definitions they came up with allowed them to accomplish
this.

                                 -- Adam

Re: Ada.Strings.Bounded

[Peter Hermann]

Adam Beneschan <adam@irvine.com> wrote:
> was a darn good reason why they did it that way.  In this particular
> case, I think they saw a need to support static expressions with
> intermediate results that were larger than a machine integer, and the

which is one of the many advantages of Ada.

BTW (changing topic):
I am still hoping that the next Ada 2015 will contain

subtype Number_Base is Integer range 2 .. 36; -- old:16;

in Ada.Text_IO for practical reasons, see

www.ada-auth.org/cgi-bin/cvsweb.cgi/ACs/AC-00070.TXT?rev=1.1

Re: Ada.Strings.Bounded

[Dmitry A. Kazakov]

On Wed, 23 Apr 2008 13:14:24 +0000 (UTC), Peter Hermann wrote:

> BTW (changing topic):
> I am still hoping that the next Ada 2015 will contain
> 
> subtype Number_Base is Integer range 2 .. 36; -- old:16;

You should have asked for more, much MORE! I mean, characters from
identifier_start + number_decimal - '0' (see Ada 2005 RM 2.3). If anybody
needed that thing, of course... (:-))

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

Re: Ada.Strings.Bounded

[Adam Beneschan]

On Apr 23, 7:40 am, "Dmitry A. Kazakov" <mail...@dmitry-kazakov.de>
wrote:
> On Wed, 23 Apr 2008 13:14:24 +0000 (UTC), Peter Hermann wrote:
> > BTW (changing topic):
> > I am still hoping that the next Ada 2015 will contain
>
> > subtype Number_Base is Integer range 2 .. 36; -- old:16;
>
> You should have asked for more, much MORE!

Right!  Base 36 allows us to use letters from A to Z, instead of just
A to F.  But with Unicode, we now have many, many, many more letters,
so why limit it to 36?  I think it would be great to have a numeric
base that would allow us to encode a numeric literal that includes C
with a hacek, a Tamil letter, some 5th-century Ogham runes, and a
couple Chinese ideographs all in the same literal.  It's obvious that
this would be a very useful feature.

                                -- Adam

Re: Ada.Strings.Bounded

[Adam Beneschan]

On Apr 22, 8:41 am, Robert A Duff <bobd...@shell01.TheWorld.com>
wrote:

> Also, there's a rule (which I'm too lazy to look up right now),
> which says that at run time, the compiler is always allowed to get the
> right answer.

You may be thinking of 4.5(13), which allows the compiler to reorder
operators at the same precedence level, so that in:

   X : Integer := Some_Function_Call (...);
   Y : Integer := (X + 1) - 1;

assuming "+" and "-" haven't been overridden, it's permissible for the
compiler to change the last expression to X + (1 - 1) which becomes
simply X, and thus not raise Constraint_Error even if
Some_Function_Call returns Integer'Last.  However, I don't know that
this *always* allows the compiler to get the right answer:

    X : Positive := Some_Function_Call (...);
    Y : Positive := X**2 / X;

The implementation permission wouldn't apply since the two operators
involved in Y's initialization aren't at the same precedence level,
and I don't know that there's anything else in the RM that would allow
the compiler to avoid raising Constraint_Error if X**2 is too large.
Also, I don't see how that rule would let the compiler avoid doing the
multiplication in something like

    Y : Integer := (X * X) - (X * X);

4.5(13) is pretty limited in its application, and I don't think
there's a general principle that the compiler is always allowed to
figure out the mathematically correct result in *all* cases without
regard to internal overflows.  Maybe there's such a rule somewhere
else, but I don't know where.  Neither of the permissions in 11.6 are
relevant here, I think.

                               -- Adam

Re: Ada.Strings.Bounded

[Dmitry A. Kazakov]

On Mon, 21 Apr 2008 09:35:36 -0700 (PDT), Eric Hughes wrote:

> ARM 2.4.1 "Decimal Literals"
> has no length limitation on 'numeral'.

Hmm, I don't see it saying this. Do you mean that the syntax rule specifies
not limit?

If so, we have visited this before, that would not prove your point.
Putting no explicit limit does not require its absence. Consider German
highways, there is no speed limit, alas only at certain places. Should it
mean existence of cars moving faster that light?

It is legal not to compile [some] legal programs.

> On Apr 21, 8:08 am, Robert A Duff <bobd...@shell01.TheWorld.com>

>> Universal_integers can be
>> implicitly converted to various integer types.
> 
> This was the whole point of the discussion--why such implicit
> conversions do not break the type system.  It's not like integers are
> a tagged type.

I don't see any difference, except that the type tag is not stored in (more
precisely, cannot be obtained from) the values.

>> type My_Int is range 1..100;
>> Y : constant My_Int := 1 + 1; -- The "+" of My_Int is called.
>>                               -- Y is of type My_Int.
> 
> Are there other places in Ada when the context of an operation
> determines the type of the operands of the function and thus also the
> function signature?

The context does not define the types. It resolves overloaded symbols.

> Context-dependent function selection need not break correctness of a
> program, even when there's ambiguity in what function might be
> selected (non-deterministic execution).  The conditions for this to
> work are implicitly present with integer types.  I believe it's
> possible to make them explicit for arbitrary types.

The following program:

with Ada.Text_IO;  use Ada.Text_IO;

procedure Test_Int is
   type My_Int is range 1..100;
   function "+" (L, R : My_Int) return My_Int is
   begin
      return 10;
   end "+";
   Y : constant My_Int := 1 + 1;
begin
   Put_Line (My_Int'Image (Y));
end Test_Int;

illustrates Robert's point. It shall print 10.

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

Re: Ada.Strings.Bounded

[Eric Hughes]

> On Mon, 21 Apr 2008 09:35:36 -0700 (PDT), Eric Hughes wrote:
> > ARM 2.4.1 "Decimal Literals"
> > has no length limitation on 'numeral'.

On Apr 21, 12:50 pm, "Dmitry A. Kazakov" <mail...@dmitry-kazakov.de>
wrote:
> Hmm, I don't see it saying this. Do you mean that the syntax rule specifies
> not limit?

That's right.  The language places no limit on the length of
numerals.  See Bob Duff's "nit" for a qualification.  Every compiler
will have some limit, but that doesn't affect the language definition.

Eric

Re: Ada.Strings.Bounded

[Adam Beneschan]

On Apr 12, 11:50 am, Eric Hughes <eric....@gmail.com> wrote:
> On Apr 5, 3:43 am, Pascal Obry <pas...@obry.net> wrote:
>
> >     What to do if we have Put_Line defined for String and
> >     Unbounded_String? Which version gets called?
>
> I know this answer is a bit heretical, but the answer I'd pick is
> "either one".  Non-deterministic execution, if you'd like the
> technical term.

Ooops, I must have stumbled into some other newsgroup---I thought I
was in comp.lang.ada.

                               -- Adam

Re: Ada.Strings.Bounded

[Eric Hughes]

On Apr 14, 9:11 am, Adam Beneschan <a...@irvine.com> wrote:
> Ooops, I must have stumbled into some other newsgroup---I thought I
> was in comp.lang.ada.

I did say "heresy".  But the whole point of that discussion was to
characterize when non-determinism would not break correctness.

Eric

Re: Ada.Strings.Bounded

[Georg Bauhaus]

Eric Hughes wrote:
> On Apr 14, 9:11 am, Adam Beneschan <a...@irvine.com> wrote:
>> Ooops, I must have stumbled into some other newsgroup---I thought I
>> was in comp.lang.ada.
> 
> I did say "heresy".  But the whole point of that discussion was to
> characterize when non-determinism would not break correctness.

It might be worth noting that this kind of "correctness"
specifically precludes factors that are essential to typical
Ada programming: for a program to solve a problem correctly,
use of time and storage must stay within specified bounds, too.

Is there a definition of "correctness" that includes more than
the necessary, static, computer agnostic precondition
of "left side of equation equals right side of equation" no
matter when and how?

Re: Ada.Strings.Bounded

[Eric Hughes]

On Apr 14, 12:13 pm, Georg Bauhaus <rm.tsoh.plus-
bug.bauh...@maps.futureapps.de> wrote:
> It might be worth noting that this kind of "correctness"
> specifically precludes factors that are essential to typical
> Ada programming: for a program to solve a problem correctly,
> use of time and storage must stay within specified bounds, too.
>
> Is there a definition of "correctness" that includes more than
> the necessary, static, computer agnostic precondition
> of "left side of equation equals right side of equation" no
> matter when and how?

Yes.

To me, the quickest way of getting at the essence of such conditions
is to start trying to write them down.  You need symbols for that.
You need a function symbol for, say, the time something takes and
another for the space something takes.  You need units of time and
units of space for the results.  You need literal expressions for
durations of time and amounts of space to write down bounds.  All
these are analytical symbols that need not be part of the language
they are analyzing.

The traditional method of correctness uses only the symbols of a
programming language combined with those of predicate calculus.
Simply from lack of expressibility, this traditional method cannot
directly address issues of time and space.  You need to obtain those
symbols from somewhere, and this pretty much means constructing an
execution model that provides a place to root those symbols.
Execution models, however, are properties of the target processor and
execution environment, and thus outside of and, really, independent of
the abstractions of high-level languages.  So, to ground this in Ada,
should there be a Ada-wide execution model?  Probably not.  Might
there be someday a way of expressing an execution model in Ada?  I
would hope so.

One of the consequences of this is that, in general, you can't prove
performance predicates about a program by itself, but only together
with an execution model.  Admittedly most execution models are
similar, but it would be a error of categories to assert a universal
one. (I don't mean to say that a canonical one might not be useful.)
There's a whole area of practical experience to gather about the
similarities of such proof prior to standardization, and I wouldn't
rush in quickly.

Finally, in order for this to work, you have to be able to connect
execution of the high-level program with execution of a program of
equivalent effect in the execution model.  This is where that Hoare
paper that I mentioned a while back, "Proof of correctness of data
representations" comes in.  It describes exactly how this works.

Eric

Re: Ada.Strings.Bounded

[Georg Bauhaus]

Eric Hughes wrote:

> Finally, in order for this to work, you have to be able to connect
> execution of the high-level program with execution of a program of
> equivalent effect in the execution model.  This is where that Hoare
> paper that I mentioned a while back, "Proof of correctness of data
> representations" comes in.  It describes exactly how this works.

Thanks for the title. I see that some methods are actually
heading in this direction. Hopefully, the basic idea that
data and timing must be formally correct, too, finds its way
into education.

Re: Ada.Strings.Bounded

[Eric Hughes]

Eric Hughes wrote:
> This is where that Hoare
> paper that I mentioned a while back, "Proof of correctness of data
> representations" comes in.  It describes exactly how this works.

On Apr 15, 2:33 pm, Georg Bauhaus <rm.tsoh.plus-
bug.bauh...@maps.futureapps.de> wrote:
> Thanks for the title. I see that some methods are actually
> heading in this direction. Hopefully, the basic idea that
> data and timing must be formally correct, too, finds its way
> into education.

You're welcome.  That essay is collected in the book _Essays in
Computing Science_.

The title of that essay might well have been titled "Proof of
correctness of compiler output", but Hoare doesn't go into compilation
issues as such in enough depth to justify such a title.  You'd have a
program annotated with some properties and their proof, a compiler
that converted the proof to one in its execution model, and proof-
carrying object code as its output.  Even if the proof annotations of
the program were empty (as today), you can still infer some basic
semantics from expressions and statements by themselves and generate
checkable proof.  I suspect that discipline would get rid of a lot of
code generation defects.

Eric

Re: Ada.Bounded_Strings

[Robert A Duff]

Adam Beneschan <adam@irvine.com> writes:

> The disadvantage of this approach was given as this: "[P]redefined
> assignment and equality for discriminated Bounded_String do not have
> the desired behavior.  Assignment makes sense when the maximum lengths
> of source and target are different, as long as the source's current
> length is no greater than the target's maximum length, yet predefined
> ":=" would raise Constraint_Error on the discriminant mismatch".
>
> The reason this doesn't make sense to me is, how does the generic
> definition solve the problem?

It doesn't, but it does cause the problem to be prevented statically,
rather than via an exception at run time.

As far as I know, there is no way to actually solve the problem in Ada
-- that is, allow all the assignments that make sense, and no others.

I must admit, that generic seems awfully heavy.  Part of the rationale
(rationalization?) was that you can just pick some reasonable max
length, and instantiate the thing once, and use it all over your
program.

- Bob

Re: Ada.Bounded_Strings

[Adam Beneschan]

On Apr 4, 4:35 pm, Robert A Duff <bobd...@shell01.TheWorld.com> wrote:
> Adam Beneschan <a...@irvine.com> writes:
> > The disadvantage of this approach was given as this: "[P]redefined
> > assignment and equality for discriminated Bounded_String do not have
> > the desired behavior.  Assignment makes sense when the maximum lengths
> > of source and target are different, as long as the source's current
> > length is no greater than the target's maximum length, yet predefined
> > ":=" would raise Constraint_Error on the discriminant mismatch".
>
> > The reason this doesn't make sense to me is, how does the generic
> > definition solve the problem?
>
> It doesn't, but it does cause the problem to be prevented statically,
> rather than via an exception at run time.

Right.  But even in the discriminant case, the compiler would usually
know statically that the assignment would necessarily raise an
exception.  (I'm assuming the discriminant would be constant in the
vast majority of cases.)  The compilers I'm familiar with would
display that fact at compile time.  Our compiler also has an option to
reject programs that will necessarily fail a predefined check such as
this.


> As far as I know, there is no way to actually solve the problem in Ada
> -- that is, allow all the assignments that make sense, and no others.

Not in a way that allows you to put the two characters := in the
statement.  But  in the discriminant case, you can still define your
own assignment *procedure*, which is almost as good.  I know, it
doesn't help with initializers.


> I must admit, that generic seems awfully heavy.  Part of the rationale
> (rationalization?) was that you can just pick some reasonable max
> length, and instantiate the thing once, and use it all over your
> program.

Again, this doesn't sound reasonable in the context of the sort of
"business applications" that I used to work on in COBOL.  For other
types of applications, it's probably OK, or Ada.Strings.Unbounded may
be best.  The reason I'm even thinking about all this is that I had
been hoping for a number of years now that Ada would be able to make
inroads into "business" applications and maybe be seen as an
alternative to COBOL, and I'm a bit disappointed that, AFAIK, nothing
or very little has happened in that arena.  Not that I think
Ada.Strings.Bounded is a major reason for this, or that providing a
better string-handling facility would help at all.  (shrug)

                                -- Adam

Re: Ada.Bounded_Strings

[Randy Brukardt]

"Adam Beneschan" <adam@irvine.com> wrote in message
news:444c0bf9-a2ad-4280-8d69-58d59938f69e@d2g2000pra.googlegroups.com...
...
> Again, this doesn't sound reasonable in the context of the sort of
> "business applications" that I used to work on in COBOL.  For other
> types of applications, it's probably OK, or Ada.Strings.Unbounded may
> be best.  The reason I'm even thinking about all this is that I had
> been hoping for a number of years now that Ada would be able to make
> inroads into "business" applications and maybe be seen as an
> alternative to COBOL, and I'm a bit disappointed that, AFAIK, nothing
> or very little has happened in that arena.  Not that I think
> Ada.Strings.Bounded is a major reason for this, or that providing a
> better string-handling facility would help at all.  (shrug)

I think that the inability to write a package that "naturally" uses literals
(and possibly indexing and slicing) for a private type are also large
impediments. (Worse, the current string packages cannot be retrofitted to
use such a capability even if it was added to Ada, lessening the possibility
of doing that.)

Net-net, I think the string packages are a disaster: just good enough to
prevent them from being properly replaced, but not good enough to use in a
natural way. (And Ada doesn't do anything useful to support UTF-8, which
doesn't help matters any.)

                          Randy.

Re: Ada.Bounded_Strings

[Dmitry A. Kazakov]

On Fri, 4 Apr 2008 23:55:56 -0500, Randy Brukardt wrote:

> "Adam Beneschan" <adam@irvine.com> wrote in message
> news:444c0bf9-a2ad-4280-8d69-58d59938f69e@d2g2000pra.googlegroups.com...
> ...
>> Again, this doesn't sound reasonable in the context of the sort of
>> "business applications" that I used to work on in COBOL.  For other
>> types of applications, it's probably OK, or Ada.Strings.Unbounded may
>> be best.  The reason I'm even thinking about all this is that I had
>> been hoping for a number of years now that Ada would be able to make
>> inroads into "business" applications and maybe be seen as an
>> alternative to COBOL, and I'm a bit disappointed that, AFAIK, nothing
>> or very little has happened in that arena.  Not that I think
>> Ada.Strings.Bounded is a major reason for this, or that providing a
>> better string-handling facility would help at all.  (shrug)
> 
> I think that the inability to write a package that "naturally" uses literals
> (and possibly indexing and slicing) for a private type are also large
> impediments.

+ classes of all types. All string types shall become members of one class.

> (Worse, the current string packages cannot be retrofitted to
> use such a capability even if it was added to Ada, lessening the possibility
> of doing that.)

Why is this a problem? Old packages could be re-implemented using new
features with the specifications left as-is for backward compatibility.

> Net-net, I think the string packages are a disaster: just good enough to
> prevent them from being properly replaced, but not good enough to use in a
> natural way. (And Ada doesn't do anything useful to support UTF-8, which
> doesn't help matters any.)

I see encodings as a different and more difficult problem. All strings are
implementations of an abstract array interface. With different encoding not
only the arrays, but also their elements will have a class: ASCII, Latin-1,
UCS-2, full Unicode. I have no idea how to handle that keeping all strings
in one class. Further, there is the presentation layer (when, say, UTF-8 is
seen as a sequence of octets). I am not sure if that need to be exposed.
Probably it has to be in order to interface other languages.

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

Re: Ada.Bounded_Strings

[Randy Brukardt]

"Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message
news:1tgn4av0s35bj.1xdkgm7hg8psa.dlg@40tude.net...
...
> > (Worse, the current string packages cannot be retrofitted to
> > use such a capability even if it was added to Ada, lessening the
possibility
> > of doing that.)
>
> Why is this a problem? Old packages could be re-implemented using new
> features with the specifications left as-is for backward compatibility.

Because there are plenty of people who will oppose adding better predefined
packages to the language, because the current ones are "good enough" and
more packages means more clutter and confusion for new Ada users.

I already ran into this once when we were discussing how to fix the problems
of the Unbounded_Strings package (it's not possible to do all operations
using only values of Unbounded_Strings - patterns, for instance have to be
regular strings. That means they have to be converted from Unbounded_String
to String in order to use them to search in an Unbounded_String -- that's
very ugly.) We only were able to make minor incremental changes, and there
was opposition to even those changes. And there was no support whatsoever
for a an improved version.

I'd expect the situation to change somewhat if we have lots of new features
to integrate, but we have a classic chicken-and-egg problem here: we're
probably not going to get those new features unless they can be used with
the string packages, but the string packages can't use those new features,
and there isn't interest in changing the packages in the absence of
significant new functionality.

                                         Randy.

Re: Untyped Ada?

[Adam Beneschan]

On Apr 4, 8:16 am, Graham <graham.st...@virtual-worlds.biz> wrote:
> On Apr 1, 11:00 pm, "Phaedrus" <phaedrus...@hotmail.com> wrote:
>
> > Certainly it is an important part of Ada, but I wasn't suggesting that it be
> > deleted entirely.  However, it might be handy to have a less-strongly typed
> > version of Ada, for instance to create prototypes faster and easier.  Then,
> > aspects of the prototype could be migrated into a "fully typed" arena once
> > the "quick and dirty" prototype was completed.
>
> > Just thinking a little bit outside the ol' box, here...
>
> > Brian
>
> I haven't been using Ada for all that long, but I have been thinking
> that a kinder, gentler version would be nice in some circumstances.
> Not necessarily *no* type-checking, but the ability to mix, say,
> integers, fixed-point types and floats in an equation without
> cluttering up the code with conversions.

The danger, of course, is that if the language allowed this, it
wouldn't catch some errors that a programmer could make, e.g. adding a
number of days to an amount of money (since you work on financial
applications).  But if there are certain operations that make sense on
certain specific types, you can define them yourself in a package, and
then another package could USE the package with the operations to be
able to use the operations that make sense, without type conversions.
That might even be better than using type conversions.  If you have
too many type conversions, a programmer could get into the habit of
just converting everything and may accidentally convert "money" to
"days" without thinking about it.  But explicitly defining the
operators that make sense will force you to think about which
operators make sense and which don't.

Ada programmers dealing with physical units have been doing this sort
of thing for a long time, with functions like:

   function "*" (X : Feet; Y : Pounds) returns Foot_Pounds;

                                 -- Adam

Re: Untyped Ada?

[DScott]

Graham wrote:
...
> I haven't been using Ada for all that long, but I have been thinking
> that a kinder, gentler version would be nice in some circumstances.
> Not necessarily *no* type-checking, but the ability to mix, say,
> integers, fixed-point types and floats in an equation without
> cluttering up the code with conversions.
> 
> I dare say that you wouldn't want to program a missile in such a loose
> way, but for the kinds of things I'm involved in - financial apps and
> simulations - the level of strictness of Ada would be a turn-off for
> many developers. And, from what I can see, the main problem with Ada
> is its lack of take-up outside its core areas of avionics and real-
> time systems.
> 
> Sorting out string handling out would be nice, too.
> 
> Graham
As one half of a team that has just started (2 months) using Ada in a business environment 
(Call Center/ Rent-A-Secretary), I have invented a few new curse words, but I wouldn't 
give it up for anything.
The strong typing is one of its best features. It makes us think very carefully about our 
data and how stuff gets passed around. The discipline is quite refreshing after all the 
slovenly code I have seen in the last 20 years.

-- 
Fui et vidi experiri.
=DSM=
A.S., B.A., M.A., M.S., Ph.D.
Ni Dan
Multi-lingual Programmer since 1960
Distinguished Rifleman
and a whole barrow-load of other stuff :)

Re: Untyped Ada?

[Dmitry A. Kazakov]

On Fri, 4 Apr 2008 08:16:04 -0700 (PDT), Graham wrote:

> I haven't been using Ada for all that long, but I have been thinking
> that a kinder, gentler version would be nice in some circumstances.
> Not necessarily *no* type-checking, but the ability to mix, say,
> integers, fixed-point types and floats in an equation without
> cluttering up the code with conversions.

But you can do that. Provided you knew the semantics of Integer + Float
your hands are free. Define

   function "+" (Left : Integer; Right : Float) return Float;

Here you  are.

The compiler does not define it for you for just one reason. The semantics
of this operation cannot be universally defined. Integers and Floats have
contradicting algebraic properties. + is exact for the former and inexact
for the latter. Therefore if adding them makes sense, that is specific for
the application which gives an interpretation to Integer and Float in some
way. In other words it is your business.

> I dare say that you wouldn't want to program a missile in such a loose
> way, but for the kinds of things I'm involved in - financial apps and
> simulations - the level of strictness of Ada would be a turn-off for
> many developers.

This puzzles me. Do not financial applications have quite strict
requirements imposed numeric behavior? Or are you writing for Bear Stearns?
(:-))

> Sorting out string handling out would be nice, too.

What do you mean? In fact Ada's fixed strings handling is the best I know.
You should never need Unbounded_String except for rare cases, when you
wanted to return two strings out of one function.

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

Re: Untyped Ada?

[Georg Bauhaus]

On Fri, 2008-04-04 at 19:38 +0200, Dmitry A. Kazakov wrote:
> On Fri, 4 Apr 2008 08:16:04 -0700 (PDT), Graham wrote:

> > I dare say that you wouldn't want to program a missile in such a loose
> > way, but for the kinds of things I'm involved in - financial apps and
> > simulations - the level of strictness of Ada would be a turn-off for
> > many developers.
> 
> This puzzles me. Do not financial applications have quite strict
> requirements imposed numeric behavior? Or are you writing for Bear Stearns?
> (:-))

I suppose it depends on 
(a) type of finance and
(b) on whose side you're on.


Say money is passed to/from a private customer. (Or, to the
state.) There are strict rules for how to add two money values
when these are the results of division, say. Thus they may need a
smaller fractional unit than the smallest currency unit permits:
"Here is $ 1. We are three. We'll divide the dollar evenly.
Each of us gets ..."
Ada's fixed point numbers are practical here.

There are really no rules when it comes to market analysis,
portfolio optimizing, and so on, as long as operation of the
software generates money, or is o.K. for the scientific
community. There should not be any obvious signs of
negligence in the software, though.
Obvious negligence in number handling might potentially be
used to provide evidence of fraud.  Market participants
may want fraud, or the friendlier forms of financial
advantage, but you want to avoid evidence. Avoid precise
evidence for sure. So the rules for computing with numbers
can be different from what you'd expect from a SPARK type 
machine control programming style, I suppose.

Likely some variables and functions will be controlling
the algorithms, reflecting what is important.
They'll read something like

   Xyz_At_Stake : Some_Type;

   function Noticeable_Change
     (Now, Then: Money; Interval: Time_Span)
     return Boolean;


Anything that works is acceptable. Not everywhere, but some
companies can operate with just the necessary level of
precision in their products. The dominant question is rather
whether or not the software works profitably. Also, whether
the software can be used as a subsidiary instrument to
generate profit, e.g. as a showcase. It does then not matter
much what the software is computing, *exactly*. More important
than  producing correct results WRT some econometric formulas,
it should compute something reasonable, i.e. results that can be
defended and that are useful in persuading someone to sign a
contract. Let's call it computer age scientific sales promotion.
(I mean in the sense of positive science, said without bias.)

If you read about the current money crisis, one cause is
attributed to (the lack of) trust among traders.
The theory of trust as a function value is not yet fully
established, let alone established with precision. How could
it? Scientific, even computable, rationalization of the
trading business? Would you want to pay for being replaced
with a computer program? So the financial market has a
more extensive set of rules about number handling than machine
control I suppose.



> What do you mean? In fact Ada's fixed strings handling is the best I know.
> You should never need Unbounded_String except for rare cases, when you
> wanted to return two strings out of one function.

Replacements of varying length are ssllllloooooooowww.

Re: Untyped Ada?

[Dmitry A. Kazakov]

On Fri, 04 Apr 2008 20:52:38 +0200, Georg Bauhaus wrote:

> On Fri, 2008-04-04 at 19:38 +0200, Dmitry A. Kazakov wrote:
> 
> [...]
> The dominant question is rather whether or not the software works profitably. 

Yes, but that is not a technical problem.

> The theory of trust as a function value is not yet fully
> established, let alone established with precision. How could
> it? 

You need a model of uncertainty for that, plus a notion of process in order
to capture temporal aspect. And an elaborated types system of Ada shines
here. Observe that otherwise, the whole argument could be reduced to the
following:

Our model is wrong. Numbers have no defined meaning. What to do? Be cool,
we will still use them with an additional advantage not to care about
accuracy of +,-,*,/ because the input data is rubbish anyway...

> Scientific, even computable, rationalization of the
> trading business? Would you want to pay for being replaced
> with a computer program? So the financial market has a
> more extensive set of rules about number handling than machine
> control I suppose.

It is an interesting issue. One of the reasons of collapse of so-called
"planned economy" was an inability to balance it, just technically,
computers were too slow that time. If somebody tried it now (without an
ideological agenda, of course), could it be possible?

>> What do you mean? In fact Ada's fixed strings handling is the best I know.
>> You should never need Unbounded_String except for rare cases, when you
>> wanted to return two strings out of one function.
> 
> Replacements of varying length are ssllllloooooooowww.

I don't remember single case where I used such replacement. For that matter
"&" has exactly same complexity. I think that the problem is how people
think about strings processing. There is a whole culture of "tokenizing"
style, which is just a wrong paradigm.

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

Re: Untyped Ada?

[Graham]

On Apr 4, 6:38 pm, "Dmitry A. Kazakov" <mail...@dmitry-kazakov.de>
wrote:
> On Fri, 4 Apr 2008 08:16:04 -0700 (PDT), Graham wrote:
> > I haven't been using Ada for all that long, but I have been thinking
> > that a kinder, gentler version would be nice in some circumstances.
> > Not necessarily *no* type-checking, but the ability to mix, say,
> > integers, fixed-point types and floats in an equation without
> > cluttering up the code with conversions.
>
> But you can do that. Provided you knew the semantics of Integer + Float
> your hands are free. Define
>
>    function "+" (Left : Integer; Right : Float) return Float;
>
> Here you  are.
>

The 'Ada way' is to define lots of types, right? So you could end up
having to maintain hundreds of these functions, couldn't you? Do
people do that? Just curious.

> The compiler does not define it for you for just one reason. The semantics
> of this operation cannot be universally defined. Integers and Floats have
> contradicting algebraic properties. + is exact for the former and inexact
> for the latter. Therefore if adding them makes sense, that is specific for
> the application which gives an interpretation to Integer and Float in some
> way. In other words it is your business.
>

That's the kind of almost philosophical argument I find baffling.
People write programs every day that mix integers and floats in
calculations, without any special handling, and the results usually
make sense.

> > I dare say that you wouldn't want to program a missile in such a loose
> > way, but for the kinds of things I'm involved in - financial apps and
> > simulations - the level of strictness of Ada would be a turn-off for
> > many developers.
>
> This puzzles me. Do not financial applications have quite strict
> requirements imposed numeric behavior? Or are you writing for Bear Stearns?
> (:-))
>

Above all, they have requirements for clarity. Suppose I have
something like:

tax : Money; -- some kind of fixed-point or decimal
tax_rate : Rate; -- some kind of float
quantity : Integer; -- or some such

I want to be able to write:

tax = tax_rate * price * quantity;

Because that way everyone can concentrate on the logic of what's going
on, rather the mechanics of it.

If instead I have to write:

tax = Money(tax_rate * Rate( price ) * Rate( quantity ));

then that's much harder to follow.

I'm open to writing functions like the suggested one:

function "*" (X : Feet; Y : Pounds) returns Foot_Pounds;

I like that idea. But I'd want persuading that it's a practical idea
for a moderately large project.

> > Sorting out string handling out would be nice, too.
>
> What do you mean? In fact Ada's fixed strings handling is the best I know.
> You should never need Unbounded_String except for rare cases, when you
> wanted to return two strings out of one function.
>

I don't understand that at all. For any web based application (at
least) you need unicode and you can't rely on strings being any
particular length.

Graham

Re: Untyped Ada?

[tmoran]

> > But you can do that. Provided you knew the semantics of Integer + Float
> > your hands are free. Define
> >
> >    function "+" (Left : Integer; Right : Float) return Float;
>
> The 'Ada way' is to define lots of types, right? So you could end up
> having to maintain hundreds of these functions, couldn't you?
  What's to "maintain"?  Not erasing the source file?  Correcting
errors that are discovered in function "+"?  Or modifying the
definition of "+" because of new requirements?  I would hope
"maintain" means the first, which shouldn't be a big burden.

Re: Untyped Ada?

[Dmitry A. Kazakov]

On Fri, 4 Apr 2008 12:14:38 -0700 (PDT), Graham wrote:

> On Apr 4, 6:38 pm, "Dmitry A. Kazakov" <mail...@dmitry-kazakov.de>
> wrote:
>> On Fri, 4 Apr 2008 08:16:04 -0700 (PDT), Graham wrote:
>>> I haven't been using Ada for all that long, but I have been thinking
>>> that a kinder, gentler version would be nice in some circumstances.
>>> Not necessarily *no* type-checking, but the ability to mix, say,
>>> integers, fixed-point types and floats in an equation without
>>> cluttering up the code with conversions.
>>
>> But you can do that. Provided you knew the semantics of Integer + Float
>> your hands are free. Define
>>
>>    function "+" (Left : Integer; Right : Float) return Float;
>>
>> Here you  are.
>>
> The 'Ada way' is to define lots of types, right? So you could end up
> having to maintain hundreds of these functions, couldn't you? Do
> people do that? Just curious.

Yes they do, because it is not hundreds in Ada. It has inheritance and
generics in order to support reuse.

>> The compiler does not define it for you for just one reason. The semantics
>> of this operation cannot be universally defined. Integers and Floats have
>> contradicting algebraic properties. + is exact for the former and inexact
>> for the latter. Therefore if adding them makes sense, that is specific for
>> the application which gives an interpretation to Integer and Float in some
>> way. In other words it is your business.
> 
> That's the kind of almost philosophical argument I find baffling.
> People write programs every day that mix integers and floats in
> calculations, without any special handling, and the results usually
> make sense.

...and the programs usually work, you mean. Granted. Now let us return to
your argument about maintaining hundreds of functions. Considering that
"usual" means 99% of cases, that gives us 1% x 100 = 100% fault rate. Thus
it does *not* work "usually". Further when it does not, how would you find
and fix the problem?

The idea of Ada is that catching inconsistencies earlier is less expensive,
though admittedly more uncomfortable for programmers) than sending bags to
Milan later.

>>> I dare say that you wouldn't want to program a missile in such a loose
>>> way, but for the kinds of things I'm involved in - financial apps and
>>> simulations - the level of strictness of Ada would be a turn-off for
>>> many developers.
>>
>> This puzzles me. Do not financial applications have quite strict
>> requirements imposed numeric behavior? Or are you writing for Bear Stearns?
>> (:-))
>>
> 
> Above all, they have requirements for clarity. Suppose I have
> something like:
> 
> tax : Money; -- some kind of fixed-point or decimal
> tax_rate : Rate; -- some kind of float
> quantity : Integer; -- or some such
> 
> I want to be able to write:
> 
> tax = tax_rate * price * quantity;
> 
> Because that way everyone can concentrate on the logic of what's going
> on, rather the mechanics of it.
> 
> If instead I have to write:
> 
> tax = Money(tax_rate * Rate( price ) * Rate( quantity ));
> 
> then that's much harder to follow.

Thank you for making my argument! The above immediately indicates a
problem. Granted, I am not a financial expert, but I guess it is
semantically wrong. What do you multiply first:

1. (tax_rate * price) * quantity

2. tax_rate * (price * quantity)

I bet only second is correct. So I would insist to define:

function "*" (Left : Money; Right : Natural) return Money;
function "*" (Left : Natural; Right : Money) return Money;
function "*" (Left : Tax_Rate; Right : Money) return Money;
function "*" (Left : Money; Right : Tax_Rate) return Money;

(I wished some syntax to instruct the compiler to derive commutative
operations and complements, as it does for "/=". But this is another story)

>>> Sorting out string handling out would be nice, too.
>>
>> What do you mean? In fact Ada's fixed strings handling is the best I know.
>> You should never need Unbounded_String except for rare cases, when you
>> wanted to return two strings out of one function.
> 
> I don't understand that at all. For any web based application (at
> least) you need unicode and you can't rely on strings being any
> particular length.

Yet I use exclusively fixed length strings! The trick is that you never
need truly varying strings. If you feel you need it, then try to reconsider
the design, because in most cases varying strings is a wrong design. The
reason is that a string is either the user/GUI/protocol input, which
determines its length, or, when you compose strings, then that is either
primitive catenation or else filling a buffer of a fixed length. 

If you need UTF-8 string handling in Ada, you might have a look at my take
of how it should be:

http://www.dmitry-kazakov.de/ada/strings_edit.htm

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

Re: Untyped Ada?

[Eric Hughes]

On Apr 4, 9:16 am, Graham <graham.st...@virtual-worlds.biz> wrote:
> I haven't been using Ada for all that long, but I have been thinking
> that a kinder, gentler version would be nice in some circumstances.
> Not necessarily *no* type-checking, but the ability to mix, say,
> integers, fixed-point types and floats in an equation without
> cluttering up the code with conversions.

If you'd like one, write one using a record with a variant part.

   type Number_Type is ( Integer_Type, Fixed1_Type, Float1_Type ) ;
-- etc.
   type Number is record
      T : Number_Type ;
      case T is
         when Integer_Type =>
            Integer_Value : Integer ;
         when Fixed1_Type =>
            Fixed1_Value : Fixed1 ;
         when Float1_Type =>
            Float1_Value : Float1 ;
      end case ;
   end record ;

Now, when you choose your floating and fixed point types and then also
write your arithmetic operations and conversions, you may realize why
there's no universal one of these that's appropriate for everybody.
I'm sure you can make one that's appropriate for you.

As for syntax, you'll have to use explicit constructor functions for
constants.  Perhaps you'd like to declare it as "type N is ...".

Eric

Re: Untyped Ada?

[adaworks]

"Phaedrus" <phaedrusalt@hotmail.com> wrote in message 
news:oYSdnZzY7_T8P2_anZ2dnUVZ_uGknZ2d@earthlink.com...
> Certainly it is an important part of Ada, but I wasn't suggesting that it be 
> deleted entirely.  However, it might be handy to have a less-strongly typed 
> version of Ada, for instance to create prototypes faster and easier.  Then, 
> aspects of the prototype could be migrated into a "fully typed" arena once the 
> "quick and dirty" prototype was completed.

Kinda sorta like having an reserved word, "unsafe" as part of the language.  :-)

Richard Riehle