* A function that cannot be called? @ 2018-10-18 12:14 G.B. 2018-10-18 15:33 ` Stefan.Lucks ` (3 more replies) 0 siblings, 4 replies; 41+ messages in thread From: G.B. @ 2018-10-18 12:14 UTC (permalink / raw) There is a type declaration, I rememberd, in Ada, that does not allow any object of the type to be declared. I think the type should be along the lines below. Is this correct? Then, a function that nominally returns objects of this type should be impossible to call. Is this right, too? generic type T(<>) is limited private; -- gen. arg. type package What is type Void (<>) is private; function Impossible (X : T) return Void; private package Inner is type Void (<>) is private; private type Void is record null; end record; end Inner; type Void is new Inner.Void; end What; (If current Ada could still pass by reference in both call direction and return direction, then I'd have added *limited* to the Voids' declarations. Without it, a body of Impossible is closer to becoming possible by using Convention => Ada together with an 'Address clause on a Result object. I think.) ^ permalink raw reply [flat|nested] 41+ messages in thread
* Re: A function that cannot be called? 2018-10-18 12:14 A function that cannot be called? G.B. @ 2018-10-18 15:33 ` Stefan.Lucks 2018-10-18 20:21 ` G.B. 2018-10-18 17:03 ` AdaMagica ` (2 subsequent siblings) 3 siblings, 1 reply; 41+ messages in thread From: Stefan.Lucks @ 2018-10-18 15:33 UTC (permalink / raw) [-- Attachment #1: Type: text/plain, Size: 820 bytes --] 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? If you really want to define a type, which does not allow any object of that type to be declared, here is one such type: type Void is abstract tagged null record; Note that objects of type Void'class can exist, but never, ever, any objects of type Void. Thus, for good reason the Ada compiler refuses to compile function Impossible(X: T) return Void; -------- I love the taste of Cryptanalysis in the morning! -------- www.uni-weimar.de/de/medien/professuren/mediensicherheit/people/stefan-lucks ----Stefan.Lucks (at) uni-weimar.de, Bauhaus-Universität Weimar, Germany---- ^ permalink raw reply [flat|nested] 41+ messages in thread
* Re: A function that cannot be called? 2018-10-18 15:33 ` Stefan.Lucks @ 2018-10-18 20:21 ` G.B. 2018-10-18 20:57 ` Niklas Holsti 2018-10-19 7:15 ` Dmitry A. Kazakov 0 siblings, 2 replies; 41+ messages in thread From: G.B. @ 2018-10-18 20:21 UTC (permalink / raw) 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, and categories with resp. programming languages' features.) As a minimum, I imagine this means passing access-to-function values, each such value designating a function whose signature include type Void. Abstract functions cannot be designated, IINM, i.e., no 'Access. > [... abstract ...] > Note that objects of type Void'class can exist, but never, ever, any objects of type Void. Thus, for good reason the Ada compiler refuses to compile > > function Impossible(X: T) return Void; So, I do want the above function to exist. I'll put the following one on the shelf, then: function Impossible (X : T) return Void is abstract; Although, the idea is, presumably, that I can use an access-to-function in some ways, but not actually call (apply) it or one of its overriding substitutes. All of this, I think, an Ada compiler will prevent when type Void is part of the signature. __ [*] Propositions as Types, Talk at Lambda Days 2016 (according to youtube) ^ permalink raw reply [flat|nested] 41+ messages in thread
* Re: A function that cannot be called? 2018-10-18 20:21 ` G.B. @ 2018-10-18 20:57 ` Niklas Holsti 2018-10-19 7:15 ` Dmitry A. Kazakov 1 sibling, 0 replies; 41+ messages in thread From: Niklas Holsti @ 2018-10-18 20:57 UTC (permalink / raw) On 18-10-18 23: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, > and categories with resp. programming languages' features.) I'm not sure that I understand what you want, but here is a type for which no valid and initialized object can exist: type Zilch is range 1 .. 0; -- Niklas Holsti Tidorum Ltd niklas holsti tidorum fi . @ . ^ permalink raw reply [flat|nested] 41+ messages in thread
* Re: A function that cannot be called? 2018-10-18 20:21 ` G.B. 2018-10-18 20:57 ` Niklas Holsti @ 2018-10-19 7:15 ` Dmitry A. Kazakov 2018-10-19 13:55 ` G.B. 1 sibling, 1 reply; 41+ messages in thread From: Dmitry A. Kazakov @ 2018-10-19 7:15 UTC (permalink / raw) 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. 1. What values the type in question must have? 2. What operations it must have? 3. Of which classes it must be a member? 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. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de ^ permalink raw reply [flat|nested] 41+ messages in thread
* Re: A function that cannot be called? 2018-10-19 7:15 ` Dmitry A. Kazakov @ 2018-10-19 13:55 ` G.B. 2018-10-19 15:31 ` Dmitry A. Kazakov 0 siblings, 1 reply; 41+ messages in thread From: G.B. @ 2018-10-19 13:55 UTC (permalink / raw) 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. ^ permalink raw reply [flat|nested] 41+ messages in thread
* Re: A function that cannot be called? 2018-10-19 13:55 ` G.B. @ 2018-10-19 15:31 ` Dmitry A. Kazakov 0 siblings, 0 replies; 41+ messages in thread From: Dmitry A. Kazakov @ 2018-10-19 15:31 UTC (permalink / raw) On 2018-10-19 15:55, G.B. wrote: > 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. I don't see relation to intuitionistic logic. Double negation is not same as the law of excluded middle. Intuitionistic logic avoids the latter but is OK with the former. >> 1. What values the type in question must have? > > A concrete type "that does not allow any object of the type to be > declared." That is not same. An ability to declare instances is unrelated to the type. E.g. universal integer, it has values, operations, but no objects declared (no named instances, except for literals of course). >> 2. What operations it must have? > > "a function that nominally returns objects of this type", > but "should be impossible to call". Any function can be called, per definition of. > Maybe callable, but fore sure > the above "absurd" function cannot be called, there not being > any object/value of type Void. Which by no means implies that it cannot be called. Ada is a consistent language. You *can* declare a function returning a type without values in Ada, the one Niklas suggested, for example. But you could not implement such a function without weakening its contract to include exceptions. > More generally, it should be possible to designate functions > whose signature includes the type Void. You still did not define that type. >> 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, That depends on what you mean under "possible". It is not possible to have a valid object of Zilch, declared or not. Further you can have this: type Zilch_Ptr is not null access Zilch; Furthermore you can annotate a declaration of a Zilch using SPARK in order to convert validness into compile-time error. > 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! That does not make sense to me. It is an old discussion about the difference between faults and bugs. You cannot handle correctness of a program in the program itself. No way. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de ^ permalink raw reply [flat|nested] 41+ messages in thread
* Re: A function that cannot be called? 2018-10-18 12:14 A function that cannot be called? G.B. 2018-10-18 15:33 ` Stefan.Lucks @ 2018-10-18 17:03 ` AdaMagica 2018-10-18 19:36 ` G.B. 2018-10-19 8:48 ` AdaMagica 2018-10-19 18:19 ` marciant 3 siblings, 1 reply; 41+ messages in thread From: AdaMagica @ 2018-10-18 17:03 UTC (permalink / raw) Am Donnerstag, 18. Oktober 2018 14:14:32 UTC+2 schrieb G.B.: > package What is > > type Void (<>) is private; > > function Impossible (X : T) return Void; > > private ... > end What; Of course this is possible. Declarations of objects of type Void must have an initial value, which can be provided via the "constructor" Impossible: X: Void := Impossible (T0); This works even if Void is made limited - then the return value is constructed in place. In effect, it's not clear what you're about. ^ permalink raw reply [flat|nested] 41+ messages in thread
* Re: A function that cannot be called? 2018-10-18 17:03 ` AdaMagica @ 2018-10-18 19:36 ` G.B. 2018-10-18 21:30 ` Randy Brukardt 0 siblings, 1 reply; 41+ messages in thread From: G.B. @ 2018-10-18 19:36 UTC (permalink / raw) On 18.10.18 19:03, AdaMagica wrote: > Am Donnerstag, 18. Oktober 2018 14:14:32 UTC+2 schrieb G.B.: >> package What is >> >> type Void (<>) is private; >> >> function Impossible (X : T) return Void; >> >> private > ... >> end What; > > Of course this is possible. Declarations of objects of type Void must have an initial value, which can be provided via the "constructor" Impossible: > > X: Void := Impossible (T0); Impossible needs to return a value. But a returned object can neither be declared nor a value constructed, since type Void has an unknown discriminant so that no initial constraint can be given anywhere. ^ permalink raw reply [flat|nested] 41+ messages in thread
* Re: A function that cannot be called? 2018-10-18 19:36 ` G.B. @ 2018-10-18 21:30 ` Randy Brukardt 2018-10-19 14:00 ` G.B. 0 siblings, 1 reply; 41+ messages in thread From: Randy Brukardt @ 2018-10-18 21:30 UTC (permalink / raw) "G.B." <bauhaus@notmyhomepage.invalid> wrote in message news:pqanbb$hl5$1@dont-email.me... > On 18.10.18 19:03, AdaMagica wrote: >> Am Donnerstag, 18. Oktober 2018 14:14:32 UTC+2 schrieb G.B.: >>> package What is >>> >>> type Void (<>) is private; >>> >>> function Impossible (X : T) return Void; >>> >>> private >> ... >>> end What; >> >> Of course this is possible. Declarations of objects of type Void must >> have an initial value, which can be provided via the "constructor" >> Impossible: >> >> X: Void := Impossible (T0); > > Impossible needs to return a value. But a returned object can > neither be declared nor a value constructed, since type Void > has an unknown discriminant so that no initial constraint > can be given anywhere. It can always be given in the body of the package, since the full type for Void has to have some declaration with "known" discriminants. (Unknown discriminants aren't allowed on full types.) And that's the point: with this declaration, the only objects that can be created are those created by the package, which is fully within the control of the creator of the abstraction. If you don't want any objects at all (which would be weird, as types have no real use until some object is created of it or a descendant), then don't create any. Randy. ^ permalink raw reply [flat|nested] 41+ messages in thread
* Re: A function that cannot be called? 2018-10-18 21:30 ` Randy Brukardt @ 2018-10-19 14:00 ` G.B. 2018-10-19 15:39 ` Dmitry A. Kazakov 2018-10-20 1:34 ` Randy Brukardt 0 siblings, 2 replies; 41+ messages in thread From: G.B. @ 2018-10-19 14:00 UTC (permalink / raw) On 18.10.18 23:30, Randy Brukardt wrote: > If you don't want any objects at all (which would be weird, as > types have no real use until some object is created of it or a descendant), > then don't create any. Not having any objects at all needs to be a feature of the Ada language's type system, at least for this kind of competition. (Hence hiding the full type in a private nest with no body.) The members of the functionist faction will turn their eyes towards the cieling in dispair: it is these weird functions involving uninhabited types that have turned out to be essential for the interplay between logicians and computer scientists discovering practical solutions. For example, what about a type system that guarantees termination? ^ permalink raw reply [flat|nested] 41+ messages in thread
* Re: A function that cannot be called? 2018-10-19 14:00 ` G.B. @ 2018-10-19 15:39 ` Dmitry A. Kazakov 2018-10-20 1:34 ` Randy Brukardt 1 sibling, 0 replies; 41+ messages in thread From: Dmitry A. Kazakov @ 2018-10-19 15:39 UTC (permalink / raw) On 2018-10-19 16:00, G.B. wrote: > Not having any objects at all needs to be a feature of the > Ada language's type system, at least for this kind of competition. Why? The purpose of the (<>) hack is not to prevent object existence, it is for ensuring proper initialization of. What Ada language needs is proper constructors. Non-existent objects do not exist merely because they don't ... > (Hence hiding the full type in a private nest with no body.) > > The members of the functionist faction will turn their eyes > towards the cieling in dispair: > it is these weird functions involving uninhabited types that have > turned out to be essential for the interplay between logicians > and computer scientists discovering practical solutions. For > example, what about a type system that guarantees termination? Termination of what? It may come as a revelation for FP folks, but a simple power plug guaranties ultimate termination of whatever program ... (:-)) -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de ^ permalink raw reply [flat|nested] 41+ messages in thread
* Re: A function that cannot be called? 2018-10-19 14:00 ` G.B. 2018-10-19 15:39 ` Dmitry A. Kazakov @ 2018-10-20 1:34 ` Randy Brukardt 2018-10-20 9:14 ` G.B. 1 sibling, 1 reply; 41+ messages in thread From: Randy Brukardt @ 2018-10-20 1:34 UTC (permalink / raw) "G.B." <bauhaus@notmyhomepage.invalid> wrote in message news:pqco17$2vr$1@dont-email.me... ... > The members of the functionist faction will turn their eyes > towards the cieling in dispair: > it is these weird functions involving uninhabited types that have > turned out to be essential for the interplay between logicians > and computer scientists discovering practical solutions. For > example, what about a type system that guarantees termination? It's this sort of babble that makes me want to ignore formal models of anything and just get my freaking work done. :-) Randy. ^ permalink raw reply [flat|nested] 41+ messages in thread
* Re: A function that cannot be called? 2018-10-20 1:34 ` Randy Brukardt @ 2018-10-20 9:14 ` G.B. 2018-10-20 11:13 ` Simon Wright 0 siblings, 1 reply; 41+ messages in thread From: G.B. @ 2018-10-20 9:14 UTC (permalink / raw) On 20.10.18 03:34, Randy Brukardt wrote: > "G.B." <bauhaus@notmyhomepage.invalid> wrote in message > news:pqco17$2vr$1@dont-email.me... > ... >> The members of the functionist faction will turn their eyes >> towards the cieling in dispair: >> it is these weird functions involving uninhabited types that have >> turned out to be essential for the interplay between logicians >> and computer scientists discovering practical solutions. For >> example, what about a type system that guarantees termination? > > It's this sort of babble that makes me want to ignore formal models of > anything and just get my freaking work done. :-) The lucid clarity of the (A)ARM speaks for itself... It might wet your appetite to recall that without the formal model of classical logic, none of Ada or its RM would be used by us. The safe SPARK subset of Ada cannot exist without type based static program analysis. SPARK is largely based on the above babble. No less. Note also that "discovery" is meant as "result of working on properties and effects of programming language designs" in research. Results such as not being able to introduce certain bugs into a program text because compile time type analysis can then proove absence of termination bugs. Sounds familiar, doesn't it, almost like taken from a SPARK brochure. Granted, the ink spot habits of functionists' writing style is incompatible with Ada culture. But they are mathematicians in disguise and so will push their guild's symbolism. 8-> ^ permalink raw reply [flat|nested] 41+ messages in thread
* Re: A function that cannot be called? 2018-10-20 9:14 ` G.B. @ 2018-10-20 11:13 ` Simon Wright 2018-10-20 14:11 ` Dmitry A. Kazakov 2018-10-21 9:07 ` G.B. 0 siblings, 2 replies; 41+ messages in thread From: Simon Wright @ 2018-10-20 11:13 UTC (permalink / raw) "G.B." <bauhaus@notmyhomepage.invalid> writes: > It might wet your appetite to recall that without the formal model > of classical logic, none of Ada or its RM would be used by us. *whet Who is "us"? Certainly doesn't include me. ^ permalink raw reply [flat|nested] 41+ messages in thread
* Re: A function that cannot be called? 2018-10-20 11:13 ` Simon Wright @ 2018-10-20 14:11 ` Dmitry A. Kazakov 2018-10-21 9:25 ` G.B. 2018-10-21 9:07 ` G.B. 1 sibling, 1 reply; 41+ messages in thread From: Dmitry A. Kazakov @ 2018-10-20 14:11 UTC (permalink / raw) On 2018-10-20 13:13, Simon Wright wrote: > "G.B." <bauhaus@notmyhomepage.invalid> writes: > >> It might wet your appetite to recall that without the formal model >> of classical logic, none of Ada or its RM would be used by us. > > *whet > > Who is "us"? Certainly doesn't include me. Huh, RM does not look much illogical to me. P.S. I think Randy wrongly accused formal models. There was nothing formal in the "babble" that offended him, IMO, it was just a pseudo-scientific claptrap... -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de ^ permalink raw reply [flat|nested] 41+ messages in thread
* Re: A function that cannot be called? 2018-10-20 14:11 ` Dmitry A. Kazakov @ 2018-10-21 9:25 ` G.B. 0 siblings, 0 replies; 41+ messages in thread From: G.B. @ 2018-10-21 9:25 UTC (permalink / raw) On 20.10.18 16:11, Dmitry A. Kazakov wrote: > P.S. I think Randy wrongly accused formal models. There was nothing formal in the "babble" that offended him, IMO, it was just a pseudo-scientific claptrap... An interesting view of an isomorphism. (The one dubbed Curry-Howard correspondence...) Although, Wadler unveils a λ-man T-shirt warn under his casual shirt, near the end of his keynote. ^ permalink raw reply [flat|nested] 41+ messages in thread
* Re: A function that cannot be called? 2018-10-20 11:13 ` Simon Wright 2018-10-20 14:11 ` Dmitry A. Kazakov @ 2018-10-21 9:07 ` G.B. 2018-10-21 9:51 ` Dmitry A. Kazakov ` (2 more replies) 1 sibling, 3 replies; 41+ messages in thread From: G.B. @ 2018-10-21 9:07 UTC (permalink / raw) On 20.10.18 13:13, Simon Wright wrote: > "G.B." <bauhaus@notmyhomepage.invalid> writes: > >> It might wet your appetite to recall that without the formal model >> of classical logic, none of Ada or its RM would be used by us. > > *whet (Ah. Thank you.) > Who is "us"? Certainly doesn't include me. The idea is that classical logic caused, and continues to cause, (features of) programming languages like Ada, in some sense. The idea is not to suggest that programmers need to be concerned with formal models in order to write programs. So, I guess for writing an embedded program like loop Ouput (Compute (Input)); end loop; one doesn't need to be aware that classical logic, without some type system, incurs the possibility of the HALTing trouble. But, OTOH, pure functionists with "program terminating types" will need monads and things as a way to write a non-terminating program. ^ permalink raw reply [flat|nested] 41+ messages in thread
* Re: A function that cannot be called? 2018-10-21 9:07 ` G.B. @ 2018-10-21 9:51 ` Dmitry A. Kazakov 2018-10-21 10:57 ` Niklas Holsti 2018-10-21 18:00 ` Simon Wright 2 siblings, 0 replies; 41+ messages in thread From: Dmitry A. Kazakov @ 2018-10-21 9:51 UTC (permalink / raw) On 2018-10-21 11:07, G.B. wrote: > The idea is that classical logic caused, and continues to cause, > (features of) programming languages like Ada, in some sense. A bizarre idea. Logic does not cause anything, in the context of programming languages it is a tool. > The idea is not to suggest that programmers need to be concerned > with formal models in order to write programs. > > So, I guess for writing an embedded program like > > loop > Ouput (Compute (Input)); > end loop; > > one doesn't need to be aware that classical logic, without some > type system, incurs the possibility of the HALTing trouble. > But, OTOH, pure functionists with "program terminating types" > will need monads and things as a way to write a non-terminating > program. This confusion of program properties with program purpose probably irritates people like Randy most. Whatever property of a program is, that becomes interesting only and exclusively with connection to the purpose of the program. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de ^ permalink raw reply [flat|nested] 41+ messages in thread
* Re: A function that cannot be called? 2018-10-21 9:07 ` G.B. 2018-10-21 9:51 ` Dmitry A. Kazakov @ 2018-10-21 10:57 ` Niklas Holsti 2018-10-21 18:00 ` Simon Wright 2 siblings, 0 replies; 41+ messages in thread From: Niklas Holsti @ 2018-10-21 10:57 UTC (permalink / raw) On 18-10-21 12:07 , G.B. wrote: > On 20.10.18 13:13, Simon Wright wrote: >> "G.B." <bauhaus@notmyhomepage.invalid> writes: >> >>> It might wet your appetite to recall that without the formal model >>> of classical logic, none of Ada or its RM would be used by us. >> >> *whet > (Ah. Thank you.) >> Who is "us"? Certainly doesn't include me. > > The idea is that classical logic caused, and continues to cause, > (features of) programming languages like Ada, in some sense. > The idea is not to suggest that programmers need to be concerned > with formal models in order to write programs. > > So, I guess for writing an embedded program like > > loop > Ouput (Compute (Input)); > end loop; > > one doesn't need to be aware that classical logic, without some > type system, incurs the possibility of the HALTing trouble. IMO most of the logicians' worry about the non-termination of such "embedded" programs is a red herring and of no importance. The logical view of an embedded program with an outermost eternal loop, as above, should consider a single cycle, that is, a program like this: assume Cycle_Invariant (State); read Inputs; compute Outputs from Inputs and State; write Outputs; update State to New_State; assert Cycle_Invariant (New_State); which has no non-termination aspects related to the cyclic loop. If the logical model has to consider some coupling of the Outputs of one cycle to the Inputs of the next cycle (for control-loop stability analysis, say) the State can often be extended to cover that coupling. Things become more complicated when the program contains cyclic tasks with various periods and perhaps some sporadic tasks. But it seems to me that such a complex multi-task program should divide its state into concurrent parts, anyway, and the invariants describing the validity of those state parts, and perhaps their mutual validity too, should be robust against all the task interleavings that can occur during execution. The logical model of even the longest-cycle task needs to consider only a statically bounded number of executions of the higher-rate or sporadic tasks, so the logical models of all tasks can assume that the outermost "non-terminating" loop, in any task, repeats for a statically bounded number of times. That said, I certainly consider termination analysis to be an important subject. But I am more interested in _quantitative_ termination bounds (for WCET analysis) than in yes/no analysis. -- Niklas Holsti Tidorum Ltd niklas holsti tidorum fi . @ . ^ permalink raw reply [flat|nested] 41+ messages in thread
* Re: A function that cannot be called? 2018-10-21 9:07 ` G.B. 2018-10-21 9:51 ` Dmitry A. Kazakov 2018-10-21 10:57 ` Niklas Holsti @ 2018-10-21 18:00 ` Simon Wright 2 siblings, 0 replies; 41+ messages in thread From: Simon Wright @ 2018-10-21 18:00 UTC (permalink / raw) "G.B." <bauhaus@notmyhomepage.invalid> writes: > So, I guess for writing an embedded program like > > loop > Ouput (Compute (Input)); > end loop; > > one doesn't need to be aware that classical logic, without some type > system, incurs the possibility of the HALTing trouble. For (most) embedded programs, one would rather they didn't halt. ^ permalink raw reply [flat|nested] 41+ messages in thread
* Re: A function that cannot be called? 2018-10-18 12:14 A function that cannot be called? G.B. 2018-10-18 15:33 ` Stefan.Lucks 2018-10-18 17:03 ` AdaMagica @ 2018-10-19 8:48 ` AdaMagica 2018-10-19 11:15 ` G.B. 2018-10-19 18:19 ` marciant 3 siblings, 1 reply; 41+ messages in thread From: AdaMagica @ 2018-10-19 8:48 UTC (permalink / raw) > package What is > > type Void (<>) is private; > Obj1, Obj2: Void; procedure Process (X: in out Void; Params: Some_Type); > > private -- Full type and object declarations here > end What; Also this is possible. There are just two objects with which you can work. An example may be registering for a certain application in different levels. ^ permalink raw reply [flat|nested] 41+ messages in thread
* Re: A function that cannot be called? 2018-10-19 8:48 ` AdaMagica @ 2018-10-19 11:15 ` G.B. 2018-10-19 17:06 ` AdaMagica 0 siblings, 1 reply; 41+ messages in thread From: G.B. @ 2018-10-19 11:15 UTC (permalink / raw) On 19.10.18 10:48, AdaMagica wrote: >> package What is >> >> type Void (<>) is private; >> > Obj1, Obj2: Void; > > procedure Process (X: in out Void; Params: Some_Type); >> >> private > -- Full type and object declarations here >> end What; > > Also this is possible. There are just two objects with which you can work. For purposes of exploration, I want Void to have no values, but I want it to have functions. One function of lesser importance would be the empty function. ^ permalink raw reply [flat|nested] 41+ messages in thread
* Re: A function that cannot be called? 2018-10-19 11:15 ` G.B. @ 2018-10-19 17:06 ` AdaMagica 2018-10-19 19:57 ` G.B. 0 siblings, 1 reply; 41+ messages in thread From: AdaMagica @ 2018-10-19 17:06 UTC (permalink / raw) I do not really understand what all this is about, but: package What is type Void (<>) is private; function Create (Params: Some_Type) return Void is abstract; private type Void is null record; -- no values end What; Void has no values (hm, a null record is a value, but it's irrelevant, since no objects exist (there is none in the private part; a body is illegal); no objects can be created because Create is abstract, so in effect Create does not exist - so it cannot be called. With caveat - I didn't try to compile this. ^ permalink raw reply [flat|nested] 41+ messages in thread
* Re: A function that cannot be called? 2018-10-19 17:06 ` AdaMagica @ 2018-10-19 19:57 ` G.B. 2018-10-19 22:06 ` Jere 0 siblings, 1 reply; 41+ messages in thread From: G.B. @ 2018-10-19 19:57 UTC (permalink / raw) On 19.10.18 19:06, AdaMagica wrote: > I do not really understand what all this is about, but: > > package What is > type Void (<>) is private; > function Create (Params: Some_Type) return Void is abstract; > private > type Void is null record; -- no values > end What; > > Void has no values (hm, a null record is a value, but it's irrelevant, since no objects exist (there is none in the private part; a body is illegal); no objects can be created because Create is abstract, so in effect Create does not exist - so it cannot be called. 41. Consume (What.Create'Access); | >>> prefix of "Access" attribute cannot be abstract If the above package is placed in some private part, then, I think, the language will guarantee that there is no way of introducing objects anywhere. From the docs of Haskell's Data.Void: "A Haskell 98 logically uninhabited data type, used to indicate that a given term should not exist." One use of all this could be: any attempt at calling the access-value passed to Consume will trigger some kind of exceptional situation. This implement works when Void is range 1..0 such that objects can be declared, but is not available with either abstract functions, as seen, or with a Void(<>) that cannot be constrained. ^ permalink raw reply [flat|nested] 41+ messages in thread
* Re: A function that cannot be called? 2018-10-19 19:57 ` G.B. @ 2018-10-19 22:06 ` Jere 2018-10-21 10:14 ` G.B. 0 siblings, 1 reply; 41+ messages in thread From: Jere @ 2018-10-19 22:06 UTC (permalink / raw) On Friday, October 19, 2018 at 3:57:41 PM UTC-4, G.B. wrote: > On 19.10.18 19:06, AdaMagica wrote: > > I do not really understand what all this is about, but: > > > > package What is > > type Void (<>) is private; > > function Create (Params: Some_Type) return Void is abstract; > > private > > type Void is null record; -- no values > > end What; > > > > Void has no values (hm, a null record is a value, but it's irrelevant, since no objects exist (there is none in the private part; a body is illegal); no objects can be created because Create is abstract, so in effect Create does not exist - so it cannot be called. > > > 41. Consume (What.Create'Access); > | > >>> prefix of "Access" attribute cannot be abstract > > If the above package is placed in some private part, then, I think, > the language will guarantee that there is no way of introducing > objects anywhere. > > From the docs of Haskell's Data.Void: > > "A Haskell 98 logically uninhabited data type, > used to indicate that a given term should not exist." > > > One use of all this could be: any attempt at calling > the access-value passed to Consume will trigger some kind of > exceptional situation. > This implement works when Void is range 1..0 such that objects > can be declared, but is not available with either abstract > functions, as seen, or with a Void(<>) that cannot be constrained. Are you ok with runtime checks? If so, you can create a separate package for the void type: package Voids is type Void is limited private; private type Void is new Ada.Finalization.Limited_Controlled with null record; overriding procedure Initialize(Self : in out Void); end Voids; package body Voids is procedure Initialize(Self : in out Void) is begin raise Program_Error; end Initialize; end Voids; Here, if try to create a variable of type Void, it will raise Program_Error (or you can add a custom exception. Same for if you call a function that tries to return a Voids.Void variable. However, you can still create functions that return this type and take their 'Access or 'Address, you just cannot ever call them without also getting an exception. Example: procedure Hello is generic type T(<>) is limited private; package Client is function Impossible(V : T) return Voids.Void; end Client; package body Client is function Impossible(V : T) return Voids.Void is begin -- do something?? return Result : Voids.Void; end Impossible; end Client; procedure Save(p : access function (V : Integer) return Voids.Void) is null; package Test is new Client(Integer); begin begin declare a : Voids.Void; begin Put_Line("Variable Creation test failed"); end; exception when Program_Error => Put_Line("Variable Creation test passed"); when others => Put_Line("Variable Creation test still failed"); end; begin Save(Test.Impossible'Access); Put_Line("Access usage test passed"); exception when others => Put_Line("Access usage test failed"); end; end Hello; Output from my compiler: $gnatmake -o hello *.adb gcc -c hello.adb gnatbind -x hello.ali gnatlink hello.ali -o hello $hello Variable Creation test passed Access usage test passed If this doesn't give you what you want, would you consider generating some example usages you envision for the type? My understanding from what you have said so far is that you want: 1. Cannot create objects of the type 2. Can create functions that return the type 3. Cannot call those functions Side note: You can also simplify my Void type with a non controlled one if you use a private full declaration like: type Void is limited record Dummy : not null access Void; end record; Since Ada will default the access variable to null, it will raise a constraint_error. My initial way allows for a custom exception if you want it. ^ permalink raw reply [flat|nested] 41+ messages in thread
* Re: A function that cannot be called? 2018-10-19 22:06 ` Jere @ 2018-10-21 10:14 ` G.B. 2018-10-21 11:30 ` Egil H H 0 siblings, 1 reply; 41+ messages in thread From: G.B. @ 2018-10-21 10:14 UTC (permalink / raw) On 20.10.18 00:06, Jere wrote: > Are you ok with runtime checks? If so, you can create a separate package > for the void type: > > package Voids is > type Void is limited private; > private > type Void is new Ada.Finalization.Limited_Controlled > with null record; > overriding procedure Initialize(Self : in out Void); > end Voids; > package body Voids is > procedure Initialize(Self : in out Void) is > begin > raise Program_Error; > end Initialize; > end Voids; > > Here, if try to create a variable of type Void, it will raise > Program_Error (or you can add a custom exception. Same for if > you call a function that tries to return a Voids.Void variable. I like the idea because the compiler will probably not suppress raising the exception. This is unlike relying on Constraint_Error being raised for 1..0. The not null constraint on a component triggers C_E not matter what, it seems. However, Initialize states the intention directly. ^ permalink raw reply [flat|nested] 41+ messages in thread
* Re: A function that cannot be called? 2018-10-21 10:14 ` G.B. @ 2018-10-21 11:30 ` Egil H H 2018-10-23 11:45 ` G.B. 0 siblings, 1 reply; 41+ messages in thread From: Egil H H @ 2018-10-21 11:30 UTC (permalink / raw) On Sunday, October 21, 2018 at 12:14:05 PM UTC+2, G.B. wrote: > On 20.10.18 00:06, Jere wrote: > > > Are you ok with runtime checks? If that's the case, you can abuse contracts: package What is pragma Assertion_Policy(Check); type Void is private with Type_Invariant => False; function Impossible return Void with Pre => False; private type Void is null record; end What; -- ~egilhh ^ permalink raw reply [flat|nested] 41+ messages in thread
* Re: A function that cannot be called? 2018-10-21 11:30 ` Egil H H @ 2018-10-23 11:45 ` G.B. 2018-10-23 14:35 ` Jere 0 siblings, 1 reply; 41+ messages in thread From: G.B. @ 2018-10-23 11:45 UTC (permalink / raw) On 21.10.18 13:30, Egil H H wrote: > package What is > pragma Assertion_Policy(Check); > > type Void is private with Type_Invariant => False; > > function Impossible return Void with Pre => False; > > private > > type Void is null record; > > end What; This approach maybe illustrates a point best: in which way does Ada's type system support detecting errors in a program early? Or is is SPARK's type system? Compile time will be best. It is tricky to explore empirically, though, since by experiments I have got two different bug boxes so far. On this account, I'm not sure if I can take 'Access of a function because seemingly doing so triggers testing theprecondition... ^ permalink raw reply [flat|nested] 41+ messages in thread
* Re: A function that cannot be called? 2018-10-23 11:45 ` G.B. @ 2018-10-23 14:35 ` Jere 2018-10-23 14:57 ` Dmitry A. Kazakov 0 siblings, 1 reply; 41+ messages in thread From: Jere @ 2018-10-23 14:35 UTC (permalink / raw) On Tuesday, October 23, 2018 at 7:45:27 AM UTC-4, G.B. wrote: > On 21.10.18 13:30, Egil H H wrote: > > > package What is > > pragma Assertion_Policy(Check); > > > > type Void is private with Type_Invariant => False; > > > > function Impossible return Void with Pre => False; > > > > private > > > > type Void is null record; > > > > end What; > > This approach maybe illustrates a point best: in which way > does Ada's type system support detecting errors in a program > early? Or is is SPARK's type system? Compile time will be best. > The difficulty with compile time comes from your requirements I think. In order for the function to exist, the compiler needs to have it actually be callable. Since Ada was not designed with such a type in mind, it would be difficult for the compiler to meet both requirements at the same time. If it were built from scratch with such a type in mind, perhaps. ^ permalink raw reply [flat|nested] 41+ messages in thread
* Re: A function that cannot be called? 2018-10-23 14:35 ` Jere @ 2018-10-23 14:57 ` Dmitry A. Kazakov 2018-10-23 17:49 ` G.B. 0 siblings, 1 reply; 41+ messages in thread From: Dmitry A. Kazakov @ 2018-10-23 14:57 UTC (permalink / raw) On 2018-10-23 16:35, Jere wrote: > The difficulty with compile time comes from your requirements I think. > In order for the function to exist, the compiler needs to have it > actually be callable. In which sense a non-callable function may exist? What exactly is the meaning of "callable"? > Since Ada was not designed with such a type in > mind, it would be difficult for the compiler to meet both requirements > at the same time. Yep, Ada was designed with consistency in mind. Given *reasonable* definitions of "callable", every function is callable and conversely. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de ^ permalink raw reply [flat|nested] 41+ messages in thread
* Re: A function that cannot be called? 2018-10-23 14:57 ` Dmitry A. Kazakov @ 2018-10-23 17:49 ` G.B. 2018-10-23 19:25 ` Dmitry A. Kazakov 0 siblings, 1 reply; 41+ messages in thread From: G.B. @ 2018-10-23 17:49 UTC (permalink / raw) On 23.10.18 16:57, Dmitry A. Kazakov wrote: > On 2018-10-23 16:35, Jere wrote: > >> The difficulty with compile time comes from your requirements I think. >> In order for the function to exist, the compiler needs to have it >> actually be callable. > > In which sense a non-callable function may exist? What exactly is the meaning of "callable"? The function is supposed to exist just like the empty function in {} -> {} in mathematics, I think. "Callable" is probably meaningful in contexts involving types, such as argument type pattern matching in functionist languages. Can't say if lazyness is needed in addition. Maybe "used" is a better word than "called". functions in Ada that take no argument but that still return something seem weird in a different way. If one restricts one's views to the "D -> E" pattern as the only respectalbe way of describing a function, then what is the proper signature of "function of no argument, but returning T" ? (Which is nice in that it allows naming expressions: function Pi return Float is (355.0 / 113.0); ) There might be another good bit in Ada in this regard, namely pure functions, to be got from a pragma, thus package Nope is pragma Pure (Nope); function Source return Integer; end Nope; I can't say whether this particular one approximates Haskell's absurd :: Void -> a but providing an Ada body for function Source from the pure package above and one that is actually impure is a little tricky. ^ permalink raw reply [flat|nested] 41+ messages in thread
* Re: A function that cannot be called? 2018-10-23 17:49 ` G.B. @ 2018-10-23 19:25 ` Dmitry A. Kazakov 2018-10-24 7:35 ` G.B. 0 siblings, 1 reply; 41+ messages in thread From: Dmitry A. Kazakov @ 2018-10-23 19:25 UTC (permalink / raw) On 2018-10-23 19:49, G.B. wrote: > On 23.10.18 16:57, Dmitry A. Kazakov wrote: >> On 2018-10-23 16:35, Jere wrote: >> >>> The difficulty with compile time comes from your requirements I think. >>> In order for the function to exist, the compiler needs to have it >>> actually be callable. >> >> In which sense a non-callable function may exist? What exactly is the >> meaning of "callable"? > "Callable" is probably meaningful in contexts involving types, Again, hat is "callable"? -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de ^ permalink raw reply [flat|nested] 41+ messages in thread
* Re: A function that cannot be called? 2018-10-23 19:25 ` Dmitry A. Kazakov @ 2018-10-24 7:35 ` G.B. 2018-10-24 8:14 ` Dmitry A. Kazakov 0 siblings, 1 reply; 41+ messages in thread From: G.B. @ 2018-10-24 7:35 UTC (permalink / raw) On 23.10.18 21:25, Dmitry A. Kazakov wrote: > On 2018-10-23 19:49, G.B. wrote: >> On 23.10.18 16:57, Dmitry A. Kazakov wrote: >>> On 2018-10-23 16:35, Jere wrote: >>> >>>> The difficulty with compile time comes from your requirements I think. >>>> In order for the function to exist, the compiler needs to have it >>>> actually be callable. >>> >>> In which sense a non-callable function may exist? What exactly is the meaning of "callable"? > >> "Callable" is probably meaningful in contexts involving types, > > Again, hat is "callable"? The original statement was referrring to the past and current Ada notion of "callable", I think. ^ permalink raw reply [flat|nested] 41+ messages in thread
* Re: A function that cannot be called? 2018-10-24 7:35 ` G.B. @ 2018-10-24 8:14 ` Dmitry A. Kazakov 0 siblings, 0 replies; 41+ messages in thread From: Dmitry A. Kazakov @ 2018-10-24 8:14 UTC (permalink / raw) On 2018-10-24 09:35, G.B. wrote: > On 23.10.18 21:25, Dmitry A. Kazakov wrote: >> On 2018-10-23 19:49, G.B. wrote: >>> On 23.10.18 16:57, Dmitry A. Kazakov wrote: >>>> On 2018-10-23 16:35, Jere wrote: >>>> >>>>> The difficulty with compile time comes from your requirements I think. >>>>> In order for the function to exist, the compiler needs to have it >>>>> actually be callable. >>>> >>>> In which sense a non-callable function may exist? What exactly is >>>> the meaning of "callable"? >> >>> "Callable" is probably meaningful in contexts involving types, >> >> Again, hat is "callable"? > > The original statement was referrring to the past and current > Ada notion of "callable", I think. In Ada callable is either T'Callable is a task attribute of some murky meaning. RM 9.9 or Callable construct = a thing invoked by a call, e.g. subprogram or entry. RM 6(1) Obviously, each function is a callable construct. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de ^ permalink raw reply [flat|nested] 41+ messages in thread
* Re: A function that cannot be called? 2018-10-18 12:14 A function that cannot be called? G.B. ` (2 preceding siblings ...) 2018-10-19 8:48 ` AdaMagica @ 2018-10-19 18:19 ` marciant 2018-10-19 18:22 ` marciant 2018-10-19 20:25 ` Shark8 3 siblings, 2 replies; 41+ messages in thread From: marciant @ 2018-10-19 18:19 UTC (permalink / raw) On Thursday, October 18, 2018 at 8:14:32 AM UTC-4, G.B. wrote: > There is a type declaration, I rememberd, in Ada, that > does not allow any object of the type to be declared. > I think the type should be along the lines below. Is > this correct? > > Then, a function that nominally returns objects of > this type should be impossible to call. Is this right, > too? > > generic > type T(<>) is limited private; -- gen. arg. type > > package What is > > type Void (<>) is private; > > function Impossible (X : T) return Void; > > private > > package Inner is > type Void (<>) is private; > private > type Void is record > null; > end record; > end Inner; > > type Void is new Inner.Void; > > end What; > > (If current Ada could still pass by reference in both call > direction and return direction, then I'd have added *limited* > to the Voids' declarations. Without it, a body of Impossible > is closer to becoming possible by using Convention => Ada > together with an 'Address clause on a Result object. I think.) Before Ada 95 or Ada 2005 it would have been a package spec that had the following (with P1,P2,etc. being valid types): type Not_Objects_Just_for_Parameters is limited private; function Return_A_Corresponding_Value(p1:t1;p2:t2;etc...) return Not_Objects_Just_for_Parameters; procedrure Force_Call_Of_Function_1 (Function_Call:Not_Objects_Just_for_Parameters; Other_Param3:p3;etc...); procedrure Force_Call_Of_Function_2 (Function_Call:Not_Objects_Just_for_Parameters; Other_Param4:p4;etc...); I miss that way of forcing/ensuring new execution of some code as a prerequisite of use of a subprogram. ;-( Being able to hang on to the result of such a function by using renames wrecks this usage. ^ permalink raw reply [flat|nested] 41+ messages in thread
* Re: A function that cannot be called? 2018-10-19 18:19 ` marciant @ 2018-10-19 18:22 ` marciant 2018-10-20 1:36 ` Randy Brukardt 2018-10-19 20:25 ` Shark8 1 sibling, 1 reply; 41+ messages in thread From: marciant @ 2018-10-19 18:22 UTC (permalink / raw) On Friday, October 19, 2018 at 2:19:07 PM UTC-4, marc...@earthlink.net wrote: > On Thursday, October 18, 2018 at 8:14:32 AM UTC-4, G.B. wrote: > > There is a type declaration, I rememberd, in Ada, that > > does not allow any object of the type to be declared. > > I think the type should be along the lines below. Is > > this correct? > > > > Then, a function that nominally returns objects of > > this type should be impossible to call. Is this right, > > too? > > > > generic > > type T(<>) is limited private; -- gen. arg. type > > > > package What is > > > > type Void (<>) is private; > > > > function Impossible (X : T) return Void; > > > > private > > > > package Inner is > > type Void (<>) is private; > > private > > type Void is record > > null; > > end record; > > end Inner; > > > > type Void is new Inner.Void; > > > > end What; > > > > (If current Ada could still pass by reference in both call > > direction and return direction, then I'd have added *limited* > > to the Voids' declarations. Without it, a body of Impossible > > is closer to becoming possible by using Convention => Ada > > together with an 'Address clause on a Result object. I think.) > > Before Ada 95 or Ada 2005 it would have been a package > spec that had the following (with P1,P2,etc. being valid types): > > type Not_Objects_Just_for_Parameters is limited private; > function Return_A_Corresponding_Value(p1:t1;p2:t2;etc...) > return Not_Objects_Just_for_Parameters; > procedure Force_Call_Of_Function_1 > (Function_Call:Not_Objects_Just_for_Parameters; > Other_Param3:p3;etc...); > procedure Force_Call_Of_Function_2 > (Function_Call:Not_Objects_Just_for_Parameters; > Other_Param4:p4;etc...); > > I miss that way of forcing/ensuring new execution of some > code as a prerequisite of use of a subprogram. ;-( > Being able to hang on to the result of such a function > by using renames wrecks this usage. Oh, I think maybe (<>) had to be used also on the type definition just like you had. ^ permalink raw reply [flat|nested] 41+ messages in thread
* Re: A function that cannot be called? 2018-10-19 18:22 ` marciant @ 2018-10-20 1:36 ` Randy Brukardt 2018-10-20 2:54 ` marciant 0 siblings, 1 reply; 41+ messages in thread From: Randy Brukardt @ 2018-10-20 1:36 UTC (permalink / raw) <marciant@earthlink.net> wrote in message news:f58ce6ac-1737-4d5a-8d4e-14f7d2940711@googlegroups.com... > On Friday, October 19, 2018 at 2:19:07 PM UTC-4, marc...@earthlink.net > wrote: ... > Oh, I think maybe (<>) had to be used also on the type definition > just like you had. The (<>) was added by Ada 95, as was the rename of function results (a mistake, IMHO), so what you wrote wouldn't have been enough in any actual version of Ada. Ada 83 didn't have any way to prevent the creation of objects without initialization. Randy. ^ permalink raw reply [flat|nested] 41+ messages in thread
* Re: A function that cannot be called? 2018-10-20 1:36 ` Randy Brukardt @ 2018-10-20 2:54 ` marciant 0 siblings, 0 replies; 41+ messages in thread From: marciant @ 2018-10-20 2:54 UTC (permalink / raw) But the full type declaration in the package could have had a hidden Boolean discriminant named Valid that had default initialization to false that would be checked in each subprogram that had a parameter of that type, right? ^ permalink raw reply [flat|nested] 41+ messages in thread
* Re: A function that cannot be called? 2018-10-19 18:19 ` marciant 2018-10-19 18:22 ` marciant @ 2018-10-19 20:25 ` Shark8 2018-10-19 23:28 ` marciant 1 sibling, 1 reply; 41+ messages in thread From: Shark8 @ 2018-10-19 20:25 UTC (permalink / raw) On Friday, October 19, 2018 at 12:19:07 PM UTC-6, marc...@earthlink.net wrote: > On Thursday, October 18, 2018 at 8:14:32 AM UTC-4, G.B. wrote: > > There is a type declaration, I rememberd, in Ada, that > > does not allow any object of the type to be declared. > > I think the type should be along the lines below. Is > > this correct? > > > > Then, a function that nominally returns objects of > > this type should be impossible to call. Is this right, > > too? > > > > generic > > type T(<>) is limited private; -- gen. arg. type > > > > package What is > > > > type Void (<>) is private; > > > > function Impossible (X : T) return Void; > > > > private > > > > package Inner is > > type Void (<>) is private; > > private > > type Void is record > > null; > > end record; > > end Inner; > > > > type Void is new Inner.Void; > > > > end What; > > > > (If current Ada could still pass by reference in both call > > direction and return direction, then I'd have added *limited* > > to the Voids' declarations. Without it, a body of Impossible > > is closer to becoming possible by using Convention => Ada > > together with an 'Address clause on a Result object. I think.) > > Before Ada 95 or Ada 2005 it would have been a package > spec that had the following (with P1,P2,etc. being valid types): > > type Not_Objects_Just_for_Parameters is limited private; > function Return_A_Corresponding_Value(p1:t1;p2:t2;etc...) > return Not_Objects_Just_for_Parameters; > procedrure Force_Call_Of_Function_1 > (Function_Call:Not_Objects_Just_for_Parameters; > Other_Param3:p3;etc...); > procedrure Force_Call_Of_Function_2 > (Function_Call:Not_Objects_Just_for_Parameters; > Other_Param4:p4;etc...); > > I miss that way of forcing/ensuring new execution of some > code as a prerequisite of use of a subprogram. ;-( > Being able to hang on to the result of such a function > by using renames wrecks this usage. Isn't there a similar effect that can be had via Type Just_For_Parameters(<>) is limited private; Function Get_Param return Just_For_Parameters; --... PRIVATE Type Stub_Record is null record; Type Just_For_Parameters is not null access Stub_Record with Size => 0; --... Or am I misunderstanding what you're getting at? (Quite possible as I've never had occasion to use Size 0 "access"-types.) ^ permalink raw reply [flat|nested] 41+ messages in thread
* Re: A function that cannot be called? 2018-10-19 20:25 ` Shark8 @ 2018-10-19 23:28 ` marciant 0 siblings, 0 replies; 41+ messages in thread From: marciant @ 2018-10-19 23:28 UTC (permalink / raw) On Friday, October 19, 2018 at 4:25:53 PM UTC-4, Shark8 wrote: <snip> > > > > Before Ada 95 or Ada 2005 it would have been a package > > spec that had the following (with P1,P2,etc. being valid types): > > > > type Not_Objects_Just_for_Parameters is limited private; > > function Return_A_Corresponding_Value(p1:t1;p2:t2;etc...) > > return Not_Objects_Just_for_Parameters; > > procedrure Force_Call_Of_Function_1 > > (Function_Call:Not_Objects_Just_for_Parameters; > > Other_Param3:p3;etc...); > > procedrure Force_Call_Of_Function_2 > > (Function_Call:Not_Objects_Just_for_Parameters; > > Other_Param4:p4;etc...); > > > > I miss that way of forcing/ensuring new execution of some > > code as a prerequisite of use of a subprogram. ;-( > > Being able to hang on to the result of such a function > > by using renames wrecks this usage. > > Isn't there a similar effect that can be had via > > Type Just_For_Parameters(<>) is limited private; > Function Get_Param return Just_For_Parameters; > --... > PRIVATE > Type Stub_Record is null record; > Type Just_For_Parameters is not null access Stub_Record > with Size => 0; > --... > Or am I misunderstanding what you're getting at? (Quite possible as I've never had occasion to use Size 0 "access"-types.) I think you are but am not sure. I was focussing of the type from the point of view of an outside user of the package and the Size code that you presented would only affect use in the package body or child units. The big problem that messed things up for me was now being able to something like this: ... declare ob : Limitted_Private_Type renames Function_Call(...); begin Proc1(ob); Proc2(ob); Proc3(ob); ... all procs getting the same value/object (Function_Call is evaluated only once.) Oh! Maybe the bothersome thing now is that functions can no longer return a limited result. (Not sure if that was a correct statement.) Anyway, although I find that do not remember the exact details for now, but I do remember for sure that it once was possible to declare a visible type in a package spec that could not be used by an outside user as the type of a variable or constant and the only things that could be passed to any subprograms in the type's package were a call of a function from that package that returned that type (and maybe also deferred constants from that same package). Wow! It _has_ been a long ride. :-) :-/ ^ permalink raw reply [flat|nested] 41+ messages in thread
end of thread, other threads:[~2018-10-24 8:14 UTC | newest] Thread overview: 41+ messages (download: mbox.gz / follow: Atom feed) -- links below jump to the message on this page -- 2018-10-18 12:14 A function that cannot be called? G.B. 2018-10-18 15:33 ` Stefan.Lucks 2018-10-18 20:21 ` G.B. 2018-10-18 20:57 ` Niklas Holsti 2018-10-19 7:15 ` Dmitry A. Kazakov 2018-10-19 13:55 ` G.B. 2018-10-19 15:31 ` Dmitry A. Kazakov 2018-10-18 17:03 ` AdaMagica 2018-10-18 19:36 ` G.B. 2018-10-18 21:30 ` Randy Brukardt 2018-10-19 14:00 ` G.B. 2018-10-19 15:39 ` Dmitry A. Kazakov 2018-10-20 1:34 ` Randy Brukardt 2018-10-20 9:14 ` G.B. 2018-10-20 11:13 ` Simon Wright 2018-10-20 14:11 ` Dmitry A. Kazakov 2018-10-21 9:25 ` G.B. 2018-10-21 9:07 ` G.B. 2018-10-21 9:51 ` Dmitry A. Kazakov 2018-10-21 10:57 ` Niklas Holsti 2018-10-21 18:00 ` Simon Wright 2018-10-19 8:48 ` AdaMagica 2018-10-19 11:15 ` G.B. 2018-10-19 17:06 ` AdaMagica 2018-10-19 19:57 ` G.B. 2018-10-19 22:06 ` Jere 2018-10-21 10:14 ` G.B. 2018-10-21 11:30 ` Egil H H 2018-10-23 11:45 ` G.B. 2018-10-23 14:35 ` Jere 2018-10-23 14:57 ` Dmitry A. Kazakov 2018-10-23 17:49 ` G.B. 2018-10-23 19:25 ` Dmitry A. Kazakov 2018-10-24 7:35 ` G.B. 2018-10-24 8:14 ` Dmitry A. Kazakov 2018-10-19 18:19 ` marciant 2018-10-19 18:22 ` marciant 2018-10-20 1:36 ` Randy Brukardt 2018-10-20 2:54 ` marciant 2018-10-19 20:25 ` Shark8 2018-10-19 23:28 ` marciant
This is a public inbox, see mirroring instructions for how to clone and mirror all data and code used for this inbox