Re: A function that cannot be called?

["G.B." <bauhaus@notmyhomepage.invalid>]

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.