Re: Ada 2012 Constraints (WRT an Ada IR)

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

On 29/11/2016 23:59, Shark8 wrote:
> On Tuesday, November 29, 2016 at 2:06:21 PM UTC-7, Dmitry A. Kazakov wrote:
>> On 2016-11-29 21:51, Shark8 wrote:
>>> On Tuesday, November 29, 2016 at 1:44:43 PM UTC-7, Dmitry A. Kazakov wrote:
>>>> On 2016-11-29 21:32, Shark8 wrote:
>>>>
>>>>> The above has a constraint -- that of only holding digits -- but
>>>>> still  is unconstrained. If we were doing a formal CS class we'd say something
>>>>> like "The type Serial_Number contains all strings that have only the
>>>>> decimal digits therein."
>>>>
>>>> You want convariance, that is a completely different beast.
>>>
>>> No, I really don't.
>>> I'm not talking about Ada-syntax,
>>
>> Yes you do, covariance vs. contravariance is semantics, not syntax.
>
> Maybe I'm misunderstanding.
> I simply don't see how covariance vs. contravariance is at all
> germane  to representing the definition of a type.

It is relevant to the difference between Ada 83 style constrained types 
and constrained types introduced by predicates. Ada 83 constraints are 
more consistent because they took into account operations that must be 
covariant. E.g. adding to the list of examples:

    subtype Text is String (1..80);

That overrides 'First, 'Last, 'Range, 'Length and propagates the 
constraint to other types by promoting Text definite. None of this 
happens if you add a predicate because all operations are inherited 
as-is = contravariant.

>>>> It is a new
>>>> type with some operations overridden, e.g. the operation that yields a
>>>> value of a discrete type for case statement. It is an implicit operation
>>>> in Ada, yet it is an operation. It must be covariant, i.e. returning the
>>>> new type rather than the old one for the case be satisfied with the new
>>>> set of values. Same with already mentioned 'First, 'Last, 'Range. Or,
>>>> for that matter, 'Succ and 'Pred if the new type has a non-contiguous
>>>> values set, e.g. Odd_Number. You cannot get there by merely putting some
>>>> predicate on the assignment operation (which Ada's predicates do). That
>>>> model is too weak to express such things.
>>>
>>> This is not about defining a type in Ada, it's about abstracting the
>>> making of a type [in Ada] and how best to represent _that_.
>>
>> What is abstracting making the type?
>
> Perhaps I should have used the word "defining" or "representing" instead of "making".

So it *is* about "defining" now?

[I still do not understand what you meant.]

BTW, "representing" is certainly irrelevant because Ada is a statically 
typed language, hence, no types are ever represented in an Ada program 
[they are in the compiler and then the representations are thrown away].

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