Re: Ada 2012 Constraints (WRT an Ada IR)

[Shark8 <onewingedshark@gmail.com>]

On Wednesday, November 30, 2016 at 1:45:04 PM UTC-7, Dmitry A. Kazakov wrote:
> 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).

In the sense that a program *IS* data, it certainly is a DDL.

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

This is true, but I don't think that ought to be the concern of the IR. -- Insofar as a CPAN-like tool is concerned w/ the IR the major operations are merely STORE and RETRIEVE; other functionality such as, say, tracking licenses or searching/indexing stored data don't involve the IR... in fact, the only operations that would are listing the dependencies and the aforementioned version-control.

Maybe a tool [or language for] operating on the IR would be appropriate, perhaps using generic/template functionality to enable the expression of a "compressed" form so that (e.g.) [[Wide_[Wide_]]String could all share common portions and so that you could have something operating across the interfaces of packages, generic or not, meta-programming stuff... but that seems pretty far outside the scope of creating an IR.

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

This is true, a full "bullet-proof system" would require extensive unit-tests tightly coupled with the particular program/library... perhaps more than are comfortable/practical for the hobbyist and small-business types.

Requiring that level of support would be nice, from an end-user point-of-view, and certainly has appeal to me given my admiration of provability and desires for "the industry" to embrace better practices... but that would require *MUCH* more work, and hamper ease-of-use [to the point of hampering usability itself, I suspect] on the program/library uploader.

As much as I like "completely correct", versioning at the CPAN-like-repository level should probably be restricted to the public interface. (Essentially the analog of "can it compile?" asked of a prolog program with the sets of modules involved, starting with the most-recent versions and backtracking until the solution is found.)

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

Of course it is, it's in the set of operations available to the subtype... imagine extending the ability to add constraints to values, but with operations. It is, in a very general sense, the same thing -- the values a type has are a set, the operations a type has are a set: if we can exclude items from the value-set, why can't we exclude operations from the operation-set?

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

Then wouldn't a way to represent both be applicable to representing an Ada-83 type?

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

Are the semantics needed when semantic validity has been ensured by the semantic-analysis phase? 

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

Or we could simply assume Ada's model w/ subtypes. (i.e. that "+"(Left, Right : Integer) Return Integer can be used for subtypes like Natural.)

The IR is to model Ada programs, not behaviors.

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

No, you misunderstand -- my thought is that the Ada type-system (insofar as defining types) can be modeled in a DDL. DIANA was just such a system, an instance of IDL, and could represent Ada's type-declarations. QED.

What I'm looking for is a more unified, universal way to do so that encompass constraints generally.