Am Fr., 18. Feb. 2022 um 18:52 Uhr schrieb Ray Dillinger <xxxxxx@sonic.net>:

[...]

> ObNitpick;  There is no such thing as a 'three-valued binary' or 'three-valued boolean' logic.
>
> What you are talking about is called ternary logic.
>
> The third value is NotABoolean in the same way that NaN is not a number; it has the same type as a logical value, so it works for purposes of type proofs, etc, but it is 'void.'  It expresses either that no valid truth value is known or that none is defined.

For those who are interested in mathematics (and in particular its
foundational aspects connected to computer science), take a look at
the treasure trove called the nLab. Here's its page about truth
values, but there is more to find when you look up "logic":
https://ncatlab.org/nlab/show/truth+value.

> I think that it would be valuable as the result of undecidable predicates - for example comparisons involving one or more NaN values.
>
> Given my own druthers and proclivities I'd call it NaB - emphasizing that it belongs to the same family of void values as NaN.  Of course that would bring up debates about the usefulness of other void values: NaS, NaC, NaL, and NaP (not-a-string, not-a-character, not-a-list, not-a-port).
>
> I for one would welcome void values. I think that typed constants indicating the unavailability of a proper value would be useful.  This is probably because I prefer not to use exceptions and would rather use out-of-band values to indicate error conditions without breaking flow of control.  Void values that don't break type consistency would be a big win for my style.  Others disagree and I respect that, but hear me out.
>
> I am tremendously grateful for NaN - it means I don't have to trace arithmetic errors through layers of exceptions defined in nine dependent libraries, etc, because NaN is consistent, locally generated, locally handled, and doesn't screw up type consistency.  At the same time NaN has the property of void contagion, which means I don't have to check the outcome of every individual arithmetic operation and make the code ninety percent error handling.  If something goes wrong in the middle I get a 'nan' at the end. I can check for it once and I can deal with it or track it down.  I wish EVERY type had such a value.
>
>
> When something calls 'cdr' for example it's supposed to return a list-typed value.  But if the thing whose 'cdr' was taken was an integer, then I would prefer to see NotAList as a return value.  Locally generated, locally handled, and subject to local contagion to allow error-handling in the calling tree.
>
> • A portable way to implement this would a procedure or macro which returns/expands to this single value. So you have to evaluate (none), or a similar expression, to get the value. But giving it reader notation like #none or #0 or #∅ or similar would make it available in non-evaluated contexts, a significant benefit.
>
> Using `null` gives you both advantages with no additional machinery, as it can be used in both evaluated and non-evaluated contexts and can already be compared with `eq?`
>
>
> This is a related issue but not the same issue.  The empty list (which is what we usually mean by 'nil' or test for with 'null?') is a valid list the same way zero is a valid number.  NotAList is a different idea.  It is a void list, not an empty list.  It means that no valid list value exists (eg, that an integer has no 'cdr' list, not even an empty one).
>
> The big benefit, IME, would be void contagion - local error contagion that respects type equations.  So you would have
>
> (/ 42 0) => NaN
> (cdr (/ 42 0))=> NaL and
> (null? (cdr (/ 42 0))) => NaB
>
> for example - each routine returning the type it's expected to return and not screwing up your type proofs, each returning to the address it's expected to return to and not screwing up the flow-of-control proofs on which your type proofs depend.
>
> Where there's a locally generated error  returning a 'void' value of that type which can be locally detected and handled is simple, consistent, and keeps the 'hair' you have to contend with to a minimum if you're trying to develop correctness proofs.

While I see use cases for what you propose and like the reasoning
behind it, for most programs it would probably result in a debugging
nightmare.

I'm not sure whether the typing in your examples is sound. For example,

(/ 42 0)

returns NaN because the result type of / should be a number. On the
other hand, cdr in general does not return lists, so having

(cdr (/ 42 0))

return a (void) list value doesn't make that much sense. An even
clearer example would be given by a record-type accessor when applied
to a non-record type:

(define-record-type address (fields name street))
(address-name 'foo)

It should not evaluate to NanA (= not an address), but to something
like NaS (= not a string) under the assumption that names are encoded
by strings. But how could the Scheme system know the latter?

Finally, won't most formal arguments reasoning about the program
become trivial when one adjoins a bottom value to every type?