bug(?) for "or" in spad

[Ralf Hemmecke]

Is the following OK?

(325) -> 4 or 3

Argument number 1 to "or" must be a Boolean.

(325) -> 4 or true

Argument number 1 to "or" must be a Boolean.

(325) -> true or 3

(325) true

(326) -> zero? 3 or 3

Argument number 2 to "or" must be a Boolean.

(326) -> zero? 0 or 3

(326) true

(327) -> true or "foo"

(327) true

Well, it is clear that a shortcut happens here, but I wonder whether we
want the language to allow "or" to take non-boolean argument.

This also is a problem in SPAD

)abbrev package FOO Foo
Foo: with
foo: Integer -> Integer
== add
foo(x: Integer): Integer ==
zero? x or
return -13
return x

The following compiles and works as well.

)abbrev package FOO Foo
Foo: with
foo: Integer -> Integer
== add
foo(x: Integer): Integer ==
zero? x or (x := x+1)
return x

But what exactly is the type of

zero? x or (x := x+1)

?

Should I put this into the github issues?

Ralf

[Grégory Vanuxem]

Hello Ralf,

For me it's not an issue for the computational world.

I explain, and as an example, in the past I wrote code for FRiCAS with
GCL (lost code because of a hdd problem).
It was an interface to BLAS totally written with 'and' and 'or', I
love that and I am always inclined to do that instead, for example, of
using (progn ...), (if ...)... I sent the code privately to Tim but I
had no return, I guess this was because the code was unreadable :) A
game.

So, instead of using:
(if (that-is not-true)
(i-will-not-do-what-i-am-supposed-to-do)
; else
(i-will-do-my-job))

I used 'and' and 'or':
(or (and (that-is not-true) (i-will-not-do-what-i-am-supposed-to-do))
(i-will-do-my-jiob))

What I mean is, with imperative languages, statements are evaluated,
executed and change program's state, your example, and eventually
returns something. It's not from my point of view like pure
mathematical logic in its restrictive sense.
With mathematical logic, and also in mathematical articles, you read,
check, and use the theorem in another "article" if true
and interesting :)

So, even, if in pure boolean logic, 'and' and 'or' ('xor') are used
with only true and false, with imperative programming language this is
not only that. In your example, my point of view is that the important
thing to take into account is not the Type but what is done.

> zero? x or (x := x+1)

can be translated to
if not zero? x then x:= x+1

What I have in mind is for libraries and not for the interpreter who
shows if required and needs the output type.
So in your last example I agree with the interpreter it *evaluates*
the first statement but since it's false it *evaluates* the second
statement, but the output type of it is incorrect so it "barfs".

Just my two cents, and I don't know if I will be understood.
____
Greg

> --
> You received this message because you are subscribed to the Google Groups "FriCAS - computer algebra system" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to fricas-devel...@googlegroups.com.
> To view this discussion on the web visit https://groups.google.com/d/msgid/fricas-devel/abf1343a-458b-9990-4bd6-0344824bc468%40hemmecke.org.

[Grégory Vanuxem]

In a hypothetical language :)

zero? x or success? (x := x+1)

[Waldek Hebisch]

On Thu, Jan 26, 2023 at 10:03:12PM +0100, Ralf Hemmecke wrote:
> Is the following OK?
>
> (325) -> 4 or 3
>
> Argument number 1 to "or" must be a Boolean.
>
> (325) -> 4 or true
>
> Argument number 1 to "or" must be a Boolean.
>
> (325) -> true or 3
>
> (325) true
>
> (326) -> zero? 3 or 3
>
> Argument number 2 to "or" must be a Boolean.
>
> (326) -> zero? 0 or 3
>
> (326) true
>
> (327) -> true or "foo"
>
> (327) true
>
> Well, it is clear that a shortcut happens here, but I wonder whether we want
> the language to allow "or" to take non-boolean argument.

This is really artifact of true interpretation: true interpreter learn
types as by-product of evaluation. When second argument is not
evaluated its type is unknown and interpreter acts as if it was
good one.

This does not happen when "interpreter" compiles code:

(2) -> foo(x) == x or 3
Type: Void
(3) -> foo(false)

Argument number 2 to "or" must be a Boolean.

(3) -> foo(true)

Argument number 2 to "or" must be a Boolean.

(3) -> bar(x) == x or true
Type: Void
(4) -> bar(false)
Compiling function bar with type Boolean -> Boolean

(4) true
Type: Boolean

Maybe the above is not entirely clear, but interpreter allows
function definition "on faith". But on first use definitions
are compiled and AFAICS the errors came from compilation.
The last case is to show difference in messages when there
is correctly typed definition.

> This also is a problem in SPAD
>
> )abbrev package FOO Foo
> Foo: with
> foo: Integer -> Integer
> == add
> foo(x: Integer): Integer ==
> zero? x or
> return -13
> return x
>
> The following compiles and works as well.
>
> )abbrev package FOO Foo
> Foo: with
> foo: Integer -> Integer
> == add
> foo(x: Integer): Integer ==
> zero? x or (x := x+1)
> return x
>
> But what exactly is the type of
>
> zero? x or (x := x+1)

Would have to check compiler internals, but it is either Void or
maybe some internal equivalent. As general priciple, when
different branches of code with different types come to the
same program point compiler computes intersection of types.
It can happen that intersection has no valid values, this is
fine as long as you do not try to use such "thing". In both
your examples needed value is provided by return statement,
so conditions are satisfied.

Note that 'or' and 'and' are programming constructs. 'a or b'
essentially is the same as

if a then a else b

There may be some confusion, because Boolean defines 'or'
function. When you use function, then programming interpretation
does not apply. However, confusion is limited, when you have
pure correctly typed function, then possible short circuit
evaluation makes no difference.

--
Waldek Hebisch