From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me X-Spam-Level: X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00 autolearn=unavailable autolearn_force=no version=3.4.4 Path: eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!news.eternal-september.org!news.eternal-september.org!feeder.eternal-september.org!aioe.org!.POSTED!not-for-mail From: "Dmitry A. Kazakov" Newsgroups: comp.lang.ada Subject: Re: Ada 2012 Constraints (WRT an Ada IR) Date: Thu, 1 Dec 2016 09:55:10 +0100 Organization: Aioe.org NNTP Server Message-ID: References: <92ed75e9-baae-455c-9e34-53348dc6eaef@googlegroups.com> <03847fd7-5699-48de-bb3c-ef5512398f26@googlegroups.com> <3ef819e8-55f7-4ef7-9f37-77e6abc33f98@googlegroups.com> NNTP-Posting-Host: vZYCW951TbFitc4GdEwQJg.user.gioia.aioe.org Mime-Version: 1.0 Content-Type: text/plain; charset=utf-8; format=flowed Content-Transfer-Encoding: 7bit X-Complaints-To: abuse@aioe.org User-Agent: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:45.0) Gecko/20100101 Thunderbird/45.5.0 X-Notice: Filtered by postfilter v. 0.8.2 Xref: news.eternal-september.org comp.lang.ada:32543 Date: 2016-12-01T09:55:10+01:00 List-Id: On 01/12/2016 01:58, Shark8 wrote: > 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. No, that thing is called "code", not program. A program would include semantics of what the program is supposed to do in the problem space. >> 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... You need no other language to run tests, as if they were of any use in this case. > As much as I like "completely correct", versioning at the > CPAN-like-repository level should probably be restricted to the public > interface. Surely so. The problem is that it is undecidable right now unless interfaces were limited to an assorted set of subprograms. Anything beyond complexity of C API stops working. >>> 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? Because that breaks other programs and operations. You cannot exclude "+" if there is "average" somewhere. The approach of putting arbitrary constraints does not work. It simply cannot work. In mathematics tasks involving constrained sets are way more difficult than unconstrained ones. E.g. looking for a maximum. Whole divisions are devoted to certain types of constraints. So it is beyond any how microscopic chance, you don't need even start. >> 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? Sure, but it is not a representation. The Ada type system certainly can be generalized and simplified. It was somehow discussed before, but there is no interest. >> 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? All sematic analysis merely resolving names. The language is designed to have nominal typing, for very good reason... >> 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. In your model of creating types (types algebra) you must answer the question what happens with the operations of the original types. The point was there is no answer to this without knowing of the problem space semantics. >> 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. Argument to Turing-completeness, huh? That applies to x86 assembly too. > What I'm looking for is a more unified, universal way to do so that > encompass constraints generally. I don't think there is any need in that from the programming POV. We cannot handle existing types of constraints in meaningful way already. The problem is not expressing some arbitrary constraint, but in propagating the constraint to dependent types and other language constructs. That usage determines the type of constraint. Ada 83 understood that very well. On the contrary, predicates is useless and dangerous mess. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de