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: Subtypes and type invariants in Ada2012 Date: Mon, 21 Aug 2017 21:55:33 +0200 Organization: Aioe.org NNTP Server Message-ID: References: NNTP-Posting-Host: MajGvm9MbNtGBKE7r8NgYA.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 10.0; WOW64; rv:52.0) Gecko/20100101 Thunderbird/52.3.0 X-Notice: Filtered by postfilter v. 0.8.2 Content-Language: en-US Xref: news.eternal-september.org comp.lang.ada:47774 Date: 2017-08-21T21:55:33+02:00 List-Id: On 2017-08-21 19:41, Victor Porton wrote: > Maybe it makes sense to allow subtype predicates, but make the subtype with > a predicate no more a scalar (even if its base is a scalar)? What should that change? > We could define "prescalars". Prime numbers would be an example of > prescalars. Prime numbers are scalar, at least in mathematics. > Prescalars would have some but not all properties of scalars. For example > prescalars would have base range but no range. Prime numbers have range, it is just so that the range with prime bounds is not always a subset of Prime. While any integer interval contains all intervals with bounds from it. That in turn is related to whether the set is closed upon numeric operations. Prime numbers lose these operations, so the set of prime numbers is not an abelian group. Nevertheless you still can enumerate primes: for I in Prime range 1..13 loop -- Runs through 1,2,3,5,7,11,13 > The hardest part here seems to define such operations as > > Prime + Prime return Natural > > Let us discuss it. I think, something can be invented. OK, but you should explain the goal. In particular why it should be a subtype? > For example, the operations returning the base type of a prescalar could be > automatically defined. It must be a type in order to distinguish between co- and contra-variance. So subtype in Ada sense looks like a non-starter. I think that finesses like arbitrary constraints cannot be expressed at the types level. A much easier way IMO is to deal with individual values and use SPARK in order to prove properties of concrete variables formulated as a post-condition. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de