* 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 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 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 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 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-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 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-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 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-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 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-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 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 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 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 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
* 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-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-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 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-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-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-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 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 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 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-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
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