A function that cannot be called?

A function that cannot be called?

[G.B.]

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.)

Re: A function that cannot be called?

[Stefan.Lucks]

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

Re: A function that cannot be called?

[G.B.]

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)
  

Re: A function that cannot be called?

[Niklas Holsti]

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
       .      @       .

Re: A function that cannot be called?

[Dmitry A. Kazakov]

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

Re: A function that cannot be called?

[G.B.]

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.

Re: A function that cannot be called?

[Dmitry A. Kazakov]

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

Re: A function that cannot be called?

[AdaMagica]

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.

Re: A function that cannot be called?

[G.B.]

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.

Re: A function that cannot be called?

[Randy Brukardt]

"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.

Re: A function that cannot be called?

[G.B.]

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?

Re: A function that cannot be called?

[Dmitry A. Kazakov]

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

Re: A function that cannot be called?

[Randy Brukardt]

"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. 

Re: A function that cannot be called?

[G.B.]

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

Re: A function that cannot be called?

[Simon Wright]

"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.

Re: A function that cannot be called?

[Dmitry A. Kazakov]

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

Re: A function that cannot be called?

[G.B.]

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.

Re: A function that cannot be called?

[G.B.]

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.

Re: A function that cannot be called?

[Dmitry A. Kazakov]

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

Re: A function that cannot be called?

[Niklas Holsti]

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
       .      @       .

Re: A function that cannot be called?

[Simon Wright]

"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.

Re: A function that cannot be called?

[AdaMagica]

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

Re: A function that cannot be called?

[G.B.]

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.

Re: A function that cannot be called?

[AdaMagica]

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.

Re: A function that cannot be called?

[G.B.]

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.

Re: A function that cannot be called?

[Jere]

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.

Re: A function that cannot be called?

[G.B.]

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.

Re: A function that cannot be called?

[Egil H H]

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

Re: A function that cannot be called?

[G.B.]

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

Re: A function that cannot be called?

[Jere]

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.

Re: A function that cannot be called?

[Dmitry A. Kazakov]

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

Re: A function that cannot be called?

[G.B.]

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.

Re: A function that cannot be called?

[Dmitry A. Kazakov]

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

Re: A function that cannot be called?

[G.B.]

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.

Re: A function that cannot be called?

[Dmitry A. Kazakov]

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

Re: A function that cannot be called?

[marciant]

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.
 

Re: A function that cannot be called?

[marciant]

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.

Re: A function that cannot be called?

[Randy Brukardt]

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

Re: A function that cannot be called?

[marciant]

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?

Re: A function that cannot be called?

[Shark8]

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.)

Re: A function that cannot be called?

[marciant]

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.  :-)  :-/