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!.POSTED!not-for-mail From: "G.B." Newsgroups: comp.lang.ada Subject: Re: A function that cannot be called? Date: Fri, 19 Oct 2018 15:55:09 +0200 Organization: A noiseless patient Spider Message-ID: References: Reply-To: nonlegitur@notmyhomepage.de Mime-Version: 1.0 Content-Type: text/plain; charset=utf-8; format=flowed Content-Transfer-Encoding: 8bit Injection-Date: Fri, 19 Oct 2018 13:55:09 -0000 (UTC) Injection-Info: reader02.eternal-september.org; posting-host="189888e645ecebbf26e597f043adf425"; logging-data="645"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX1+23FF3JD40qUuDtnzPWuXb9kP6VJLMFY8=" User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.13; rv:52.0) Gecko/20100101 Thunderbird/52.9.1 Cancel-Lock: sha1:2vyM9yY7brko8xIazoixZVHqKr4= In-Reply-To: Content-Language: de-DE Xref: reader02.eternal-september.org comp.lang.ada:54652 Date: 2018-10-19T15:55:09+02:00 List-Id: On 19.10.18 09:15, Dmitry A. Kazakov wrote: > On 2018-10-18 22:21, G.B. wrote: >> On 18.10.18 17:33, Stefan.Lucks@uni-weimar.de wrote: >>> On Thu, 18 Oct 2018, G.B. wrote: >>> >>>> There is a type declaration, I rememberd, in Ada, that >>>> does not allow any object of the type to be declared. >>> >>> What, exactly, is the point of your question? >> >> Philip Wadler asked, on occasion[*], whether there was any programming >> language other than Haskell that had a (concrete, usable in the normal >> way I guess) type like ("unihabited") Void in Data.Void.  (The point is >> getting my feet wet at the shores of correspondences of logic, typed lambdas, > > You should probably start expressing what you want using clearer terms. A type has a set of values and a set of operations. A type can be a member of several classes of types. First, correction: Bartosz Milewski was talking about all this, on the same occasion, referring to functions like (in Haskell) absurd :: Void -> T for some "initial object" (in a category) or (maybe Ada-ized): type Double_Negation is access -- (T -> Void) -> Void function (F : access function (X : T) return Void) return Void; with reference to intuitionist logic embedded in classical logic. (Wadler had talked about proofs and evaluating programs written using simple typed lambdas, terminating). Void is not C's void, Milewski says, so maybe Ada can never have that kind of Void either. > 1. What values the type in question must have? A concrete type "that does not allow any object of the type to be declared." > 2. What operations it must have? "a function that nominally returns objects of this type", but "should be impossible to call". Maybe callable, but fore sure the above "absurd" function cannot be called, there not being any object/value of type Void. More generally, it should be possible to designate functions whose signature includes the type Void. > 3. Of which classes it must be a member? On the outside, are there different types Void whose functions compute results of types that differ by class? I see that the original Void is an instance of Eq type. More ideas below, not really up to anything precise yet. > E.g. the type proposed by Niklas: > >    type Zilch is range 1 .. 0; > > has an empty set of values, non empty set of operations. It is a member of the non-tagged classes Zilch'Base, universal integer etc. This scalar type has no values, but declarations are possible, unless I use type Void(<>) is private; private type Void is range 1 .. 0; and make sure that there is no way of producing an object of the subtype. (As shown, in a package inside a private part.) However, not doing that and making type Void is range 1 .. 0; only private to package body and children, thus allowing objects, an interesting set of functions around type Void comes to mind, for use in expression evaluation. I'd switch to handler functions taking functions returning Void. So, an access value designating function Impossible (X : Exception_Id) return Void is begin return Result : Void; exception when Constraint_Error => Raise_Exception (X); end Impossible; and passed as an argument, will signal, for example, by raising exception X, that "This, i.e., X, shouldn't happen!" Meaning that if Impossible gets evaluated, something is wrong! Since this is all about learning, I shouldn't be talking any more now.