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=-0.3 required=5.0 tests=BAYES_00,
	REPLYTO_WITHOUT_TO_CC autolearn=no 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!mx05.eternal-september.org!feeder.eternal-september.org!aioe.org!.POSTED!not-for-mail
From: "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de>
Newsgroups: comp.lang.ada
Subject: Re: Seeking for papers about tagged types vs access to subprograms
Date: Sun, 12 May 2013 12:07:33 +0200
Organization: cbb software GmbH
Message-ID: <5z6ykdvv3ku2$.trxjt4vkzdg9$.dlg@40tude.net>
References: <op.wv8jh1c1ule2fv@cardamome>
 <1bfhq7jo34xpi.p8n2vq6yjsea.dlg@40tude.net> <op.wwrefx1pule2fv@cardamome>
 <cps71yzogw24$.7ol98fxcaurj$.dlg@40tude.net> <op.wwriky0dule2fv@cardamome>
 <nd22gfeezrwf$.tlj4yyygrwq3$.dlg@40tude.net> <kmecg6$et4$1@loke.gir.dk>
 <12gn9wvv1gwfk.10ikfju4rzmnj.dlg@40tude.net> <kmh7d4$up3$1@loke.gir.dk>
 <1oy5rmprgawqs.1jz36okze0xju$.dlg@40tude.net> <kmk45u$v45$1@loke.gir.dk>
 <1q2ql1e4rcgko.diszzq1mhaq8$.dlg@40tude.net> <op.wwwtznpsule2fv@cardamome>
 <1msoad3apbkf.1optea1ujjydv.dlg@40tude.net>
 <wcc61ypi100.fsf@shell01.TheWorld.com>
 <otnq8fecgbel.1itrfodtky6d0.dlg@40tude.net> <op.wwyj4vovule2fv@cardamome>
 <xrlivgfvo6vp.1w3qblmw5gfzr.dlg@40tude.net> <op.wwypinhaule2fv@cardamome>
 <18iybsmtjt4ay.efhc3ordxiua$.dlg@40tude.net> <op.wwysrzk1ule2fv@cardamome>
Reply-To: mailbox@dmitry-kazakov.de
NNTP-Posting-Host: 15waz9CoS+eMakbyhTPyFQ.user.speranza.aioe.org
Mime-Version: 1.0
Content-Type: text/plain; charset="iso-8859-1"
Content-Transfer-Encoding: 8bit
X-Complaints-To: abuse@aioe.org
User-Agent: 40tude_Dialog/2.0.15.1
X-Notice: Filtered by postfilter v. 0.8.2
Xref: news.eternal-september.org comp.lang.ada:15526
Date: 2013-05-12T12:07:33+02:00
List-Id: <comp.lang.ada>

On Sun, 12 May 2013 11:32:13 +0200, Yannick Duchêne (Hibou57) wrote:

> Le Sun, 12 May 2013 11:25:51 +0200, Dmitry A. Kazakov  
> <mailbox@dmitry-kazakov.de> a écrit:
> 
>>> Seems the invariably `True`
>>> precondition wants to give the illusion of universal reuse without
>>> conditions.
>>
>> No, "true" means what that the contract was not a lie. If you say that  the
>> argument of sqrt is Float and another person say that it is not negative,
>> then somebody is lying here.
> 
> This is the same person who says both as this is the one who wrote the  
> signature and the precondition. And this is not a contradiction to have  
> conjunction of conditions, that's common.

Except that it is not a conjunction. If it were a conjunction then either
specified as proper type or else, if there were no types, as solely a
dynamic precondition. That is the choice between being untyped or strong
types. Your case is neither. Furthermore it cannot be made the second in
realistic cases because such constraints cannot be statically enforced. So
if you want it a conjunction it must be the first:

# pre X in Float and then X >= 0.0
   function sqrt (X : Any) return Float;

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