Re: Ada 2012 Constraints (WRT an Ada IR)

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

On 2016-11-30 19:28, Shark8 wrote:

> So, with that in mind it makes sense to
> consider the usefulness of making Semantic_Analysis_Result its own
> formal language: the Intermediate Representation.

It would be difficult without making intermediate effectively target 
language, e.g. byte code. What you have in mind is some sort of data 
definition language [DDL] (operations' semantics stripped).

> These properties are ideal for many applications -- one of the most
> practical to addressing some of the complaints/difficulties leveled at
> Ada (like a poor ecosystem) would be implementation of a CPAN-style
> repository... but far better -- for if we can, say, make this IR amiable
> to storage in a DB (with attendant consistency-checks) we can eliminate
> the storage of invalid Ada in said repository; furthermore, because we
> have all the semantic-information already we could build-in tools to
> allow correct dependency-storage, like Gnoga using Simple Components,
> but with proper versioning so that a breaking change in a new version's
> API could be detected and the older one with the required properties
> could be retrieved.

Surely some level of introspection would be extremely helpful for 
distributed and persistency systems.

Versioning is a huge issue unresolved. I am afraid that type 
representation if not enough by far, because you need a lot of 
additional information to decide substitutablity, which is key to 
handling type versions.

>>>>> 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.
>
> And shouldn't that (eg Predicated_Subtype'Pred or 'Last, etc) be
> caught by the semantic-analysis phase? If so, then it's entirely a moot
> point, isn't it?

The compiler cannot read minds. The information that the semantics of 
'Pred must be changed (and thus the operation becomes covariant) is 
nowhere to get. In the model of tagged types covariance is the default. 
In the model of added predicates it is contravariance the default. 
Ada-83 subtypes mix contravariance and covariance by hardwired rules.

> But it certainly doesn't invalidate the concept of considering a
> type  [and subtype] as the collection of a set of values and a set of
> operations on those values; for example:
>
>     Type Nybble is range 0..15 with Size => 4;
>     Subtype Prime_Nybble is Nybble with
>       Static_Predicate => Prime_Nybble in 2|3|5|7|11|13;
>
> could be represented as something which visualized-as-text would be:
>
>    Nybble is
>     Size            : Bits(4)
>     Internal_Values : Set(0..15)
>     Offset          : 0          -- So we could represent 1..16 w/ 4-bits
>     Operations      : Arithmetic_ops & Scalar_Attributes
>
>
>    Prime_Nybble modifying Nybble is
>     Operations      : Operations without Scalar_Attributes
>
> or somesuch.

You describe here DDL and leave all semantics of the operations aside.

Prime numbers do not have arithmetic because arithmetic operations on 
primes do not yield a prime. A semantically correct choice for "+" is 
either leave it contravariant:

    function "+" (Left, Right : Prime) return Universal_Integer;

or drop it

    function "+" (Left, Right : Prime) return Prime is abstract;

For attributes the choices are different. It depends on the properties 
of the mathematical structure the [sub]type is to model. There is no way 
the language could decide that. It can for built-in types, because they 
are built-in.

[...]

 > Does that clear things up?

Yes, you are under the delusion that DDL is a type system. It is not, 
DDL is weakly/untyped and as such is fundamentally incapable to describe 
Ada type system, not even in first approximation.

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