Eric Hughes <eric.eh9@[EMAIL PROTECTED]
> writes:
> On Apr 21, 8:08 am, Robert A Duff <bobd...@[EMAIL PROTECTED]
>
> 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....@[EMAIL PROTECTED]
> 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....@[EMAIL PROTECTED]
> 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....@[EMAIL PROTECTED]
> 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 sup****ted 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...@[EMAIL PROTECTED]
>
> 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
|
