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.1 required=5.0 tests=BAYES_00,
	PP_MIME_FAKE_ASCII_TEXT autolearn=no autolearn_force=no version=3.4.4
Path: 
 eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!feeder.eternal-september.org!nntp-feed.chiark.greenend.org.uk!ewrotcd!newsfeed.xs3.de!io.xs3.de!news.jacob-sparre.dk!franka.jacob-sparre.dk!pnx.dk!.POSTED.rrsoftware.com!not-for-mail
From: "Randy Brukardt" <randy@rrsoftware.com>
Newsgroups: comp.lang.ada
Subject: Re: Record operations (Algebraic Data Types and printing)
Date: Tue, 9 Oct 2018 17:25:26 -0500
Organization: JSA Research & Innovation
Message-ID: <ppj9sm$vq2$1@franka.jacob-sparre.dk>
References: 
 <0f5608ef-0038-491c-b15f-f67bcc76fae8@googlegroups.com><00285ebf-6ede-44da-848f-456930dc7475@googlegroups.com><ppgnnu$v90$1@franka.jacob-sparre.dk><0028bb67-9b19-46a5-a126-3415e0281add@googlegroups.com>
 <87d0sj379h.fsf@nightsong.com>
Injection-Date: Tue, 9 Oct 2018 22:25:27 -0000 (UTC)
Injection-Info: franka.jacob-sparre.dk;
 posting-host="rrsoftware.com:24.196.82.226";
	logging-data="32578"; mail-complaints-to="news@jacob-sparre.dk"
X-Priority: 3
X-MSMail-Priority: Normal
X-Newsreader: Microsoft Outlook Express 6.00.2900.5931
X-RFC2646: Format=Flowed; Original
X-MimeOLE: Produced By Microsoft MimeOLE V6.00.2900.7246
Xref: reader02.eternal-september.org comp.lang.ada:54530
Date: 2018-10-09T17:25:26-05:00
List-Id: <comp.lang.ada>

"Paul Rubin" <no.email@nospam.invalid> wrote in message 
news:87d0sj379h.fsf@nightsong.com...
> Henrik Härkönen <heharkon@gmail.com> writes:
>> And interestingly, what got me initially checking more about Ada, was
>> this Wikipedia page about Dependent Types, where "Ada 202x" was listed
>> to be supporting those:
>>
>> https://en.wikipedia.org/wiki/Dependent_type
>
> I don't think that can be right, in the sense in which that term is
> normally used.  But, I think C++ uses it to mean something different, so
> maybe Ada 202x does as well.

The Wikipedia article references "Subtype predicates" (and I would add "Type 
invariants" to that) to provide this capability. Which means the reference 
really should be to Ada 2012, since that is where those were introduced. It 
also references SPARK to get static proofs.

                                         Randy.