Re: A function that cannot be called?

["Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de>]

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