[fricas-devel] unique Value of Void

[Ralf Hemmecke]

Ricardo made me aware that the formulations in
http://fricas.github.io/book.pdf Section 5.3 maybe a bit confusing to
new users.

We all know that Void is the type used in situations where there is no
value. However the Book says on page 149:

If the else clause is missing then the entire expression returns the
unique value of Void.

Uh? So Void doesn't mean "no value"?

Even more funny then is this

(1) -> A := if 1<2 then 1

(1) 1
Type: PositiveInteger
(2) -> A

(2) 1
Type: PositiveInteger
(3) -> B := if 2<1 then 1

You cannot assign an object of type Void to any identifier, (in
particular, ??? ).

(3) -> 3::Void
Type: Void
(4) -> C := 3::Void

You cannot assign an object of type Void to any identifier, (in
particular, ??? ).

So the Book uses the word "value" with different meanings. The value
with type Void cannot be used any further, i.e., is not assignable to
any identifier.

Furthermore, (1) does not behave as described, because "if 1<2 then 1"
should be of type Void and not of type PositiveInteger.

It's understandable that FriCAS chooses to return 1 in case (1), because
otherwise it wouldn't be intuitive for a user. I'm pretty sure that
something like (1) wouldn't work in the compiler, but shouldn't we
change the documentation and explain, that "if" behaves differently in
interpreter vs compiler?

Any suggestions?

Ralf

[Bill Page]

Post by Ralf Hemmecke
Ricardo made me aware that the formulations in
http://fricas.github.io/book.pdf Section 5.3 maybe a bit confusing to
new users.
We all know that Void is the type used in situations where there is
no value.

No that is not correct. 'void()$Void' is the value that is used when
"no value is needed". To say that no value is needed is not the same
as there being no value. Perhaps it would be better to say that "no
specific value is needed" - in other words we do not care about the
actual value. But by definition the 'Void' domain does have just one
value. 'Void' is the "unit type" (terminal object in the categorical
model of FriCAS the type system). In most type systems it would also
be the "empty tuple" () or what Aldor would call an empty 'Cross'
product. ('Tuple' in FriCAS actually means something else.)

From the source code for Void:

++ Description:
++ This type is used when no value is needed, e.g., in the
++ \spad{then} part of a one armed \spad{if}.
++ All values can be coerced to type Void. Once a value has
++ been coerced to Void, it cannot be recovered.

Oldk suggested the following addition

+++ \spadtype{Void} implements the unit type in type theory.
+++ It allows only one value thus can hold no information.
+++ Void is used in the \spad{then} part of a one armed \spad{if}.

It might be misleading to say that a domain that has only one value
can hold no information. E.g.

(4) -> C:Union(Void,PositiveInteger):=2

(4) 2
Type: Union(PositiveInteger,...)
(5) -> C case Void

(5) false
Type: Boolean

Post by Ralf Hemmecke
If the else clause is missing then the entire expression returns the
unique value of Void.
Uh? So Void doesn't mean "no value"?

No, it does not mean "no value". It means that we do not care what value.

'Exit' is the domain in FriCAS that has no value. 'Exit' is the "zero
type" (initial object in the categorical model).

Post by Ralf Hemmecke
Even more funny then is this
(1) -> A := if 1<2 then 1
(1) 1
Type: PositiveInteger
(2) -> A
(2) 1
Type: PositiveInteger
(3) -> B := if 2<1 then 1
You cannot assign an object of type Void to any identifier, (in
particular, ??? ).
(3) -> 3::Void
Type: Void
(4) -> C := 3::Void
You cannot assign an object of type Void to any identifier, (in
particular, ??? ).

The implementation in the interpreter is wrong. B and C should both
contain the same 'void()' value.

Post by Ralf Hemmecke
So the Book uses the word "value" with different meanings.

In this instance the book is correct.

Post by Ralf Hemmecke
The value with type Void cannot be used any further, i.e.,
is not assignable to any identifier.

No. There should be no problem handling the value of 'Void' in the
same way as any other value (provided that it is type-correct).

Post by Ralf Hemmecke
Furthermore, (1) does not behave as described, because
"if 1<2 then 1" should be of type Void and not of type
PositiveInteger.
It's understandable that FriCAS chooses to return 1 in case (1),
because otherwise it wouldn't be intuitive for a user. I'm pretty
sure that something like (1) wouldn't work in the compiler,

Try this:

-- file: one-armed.spad
)abbrev domain TEST Test
Test(): with
test1: ()->Integer
test2: ()->Void
== add
test1() ==
A := if 1<2 then 1
return A
test2() ==
B := if 2<1 then 1
return B
--

Result:

(1) -> )co one-armed
Compiling FriCAS source code from file /home/wspage/one-armed.spad
using old system compiler.
TEST abbreviates domain Test
...
Test will be automatically loaded when needed from
/home/wspage/TEST.NRLIB/TEST

(1) -> test1()

(1) 1
Type: PositiveInteger
(2) -> test2()
Type: Void

Post by Ralf Hemmecke
but shouldn't we change the documentation and explain,
that "if" behaves differently in interpreter vs compiler?
Any suggestions?

I would rather change the interpreter to behave is the same way as the compiler.

--

BTW, here is another case where |$resolve_level| is needed:

(3) -> test2()=void()$Void
The variable |$resolve_level| is unbound.

Also as a one-element set I think 'Void' should really satisfy
'SetCategory' so then

(3) -> (test2()=void()$Void)@Boolean

and similar expressions would return 'true' by definition.

[Riccardo GUIDA]

Hi,

Thanks for your clarifications Bill.


Just to say that my original question to Ralf was a much more low level quest for clarifications in the user guide:

1) A user reads:

section 5.3 pag 149
"An if-then-else expression always returns a value. If the else clause is missing then the entire expression returns the unique value of Void. If both clauses are present, the type of the value returned by if is obtained by resolving the types of the values of the two clauses. See Section 2.10 on page 109 for more information." (Check also the boxed text above this statement.)

2) The user does not really understand the statement and, if he is motivated, tries to experiment:

(1) -> if 1>2 then 1 -- here he expects Void
Type: Void
(2) -> if 2>1 then 1 -- here he expects Void but gets PositiveInteger

(2) 1
Type: PositiveInteger
(3) -> if 2>1 then 1 else [1,2,3] -- here he expects common supertype, but which one?

(3) 1
Type: PositiveInteger
(4) -> if 1>2 then 1 else [1,2,3] -- here he expects common supertype, which one?

(4) [1, 2, 3]
Type: List(PositiveInteger)

3) The user is puzzled because

* in (2) below he gets Type: Positive Integer not Type: Void
* in (3) and (4) below he sees 2 different types and not a "common supertype"



From your explanations now I understand that there are a lot of hidden coercitions in the game and that what is said in the user guide does not contradict the experiments. But I feel it would be helpful to have some clarifying information in the user guide not after page 149. Writing "the unique value of Void" is not of help because what is not evident is the fact that "every value can be coerced to Void". I realize now that this is said at pag 763, sec 9.87 (in my version of FricasUG), but at least a footnote in page 149 would have helped.

ric

[Bill Page]

On Fri, Jun 29, 2018 at 10:10 AM, Riccardo GUIDA

Post by Riccardo GUIDA
Thanks for your clarifications Bill.

Thank you for asking the question.

Post by Riccardo GUIDA
Just to say that my original question to Ralf was a much more low

OK. I think I understand your motivation and Ralf's concerns about clarity.

Post by Riccardo GUIDA
section 5.3 pag 149
"An if-then-else expression always returns a value.

I think this is clear.

Post by Riccardo GUIDA
If the else clause is missing then the entire expression
returns the unique value of Void.

I agree that this sentence is either confusing or wrong. I would
suggest the following:

If the else clause is missing but the if condition is false then the
value of the if-then expression is the unique value of Void.

Post by Riccardo GUIDA
If both clauses are present, the type of the value returned by if is obtained
by resolving the types of the values of the two clauses. See Section 2.10
on page 109 for more information." (Check also the boxed text above this
statement.)

I suppose that the key issue is what might be meant by "resolving the
types". My interpretation is that that although both an if-then-else
expression and an if-then expression "always return a value", the
actual type is indeterminate and depends on knowing the types of both
clauses, i.e. the type of the then-part and the type of the (possibly
missing) else-part. But in the appropriate context the compiler (and
in principle the interpreter) are able to determine an appropriate for
the result.

Post by Riccardo GUIDA
2) The user does not really understand the statement and, if he is
(1) -> if 1>2 then 1 -- here he expects Void
Type: Void

OK.

Post by Riccardo GUIDA
(2) -> if 2>1 then 1 -- here he expects Void but gets PositiveInteger
(2) 1
Type: PositiveInteger

I can see that a naive interpretation of the statement in the guide
might lead to this expectation. But given a clear understanding of the
Void domain, it should be obvious that such a result could not be
useful.

Post by Riccardo GUIDA
(3) -> if 2>1 then 1 else [1,2,3] -- here he expects common supertype, but which one?
(3) 1
Type: PositiveInteger

So, to this user "resolving the type" seems to imply the existence of
a supertype. In fact such a supertype does exist in FriCAS (Union) and
given that the statement in the guide is not so clear this is
certainly a reasonable expectation but I do not think that it is
actually implied.

Post by Riccardo GUIDA
(4) -> if 1>2 then 1 else [1,2,3] -- here he expects common supertype, which one?
(4) [1, 2, 3]
List(PositiveInteger)

If we provide a bit more type information then the users expectations
can be met.

(1) -> A:Union(PositiveInteger, List PositiveInteger) := if 2>1 then 1
else [1,2,3]

(1) 1
Type: Union(PositiveInteger,...)
(2) -> A:Union(PositiveInteger, List PositiveInteger) := if 1>2 then 1
else [1,2,3]

(2) [1, 2, 3]
Type: Union(List(PositiveInteger),...)

Post by Riccardo GUIDA
3) The user is puzzled because
* in (2) below he gets Type: Positive Integer not Type: Void
* in (3) and (4) below he sees 2 different types and not a "common supertype"

Yes I see how this is possible.

Post by Riccardo GUIDA
From your explanations now I understand that there are a lot of
hidden coercion in the game and that what is said in the user
guide does not contradict the experiments. But I feel it would be
helpful to have some clarifying information in the user guide not
after page 149. Writing "the unique value of Void" is not of help
because what is not evident is the fact that "every value can be
coerced to Void". I realize now that this is said at pag 763,
sec 9.87 (in my version of FricasUG), but at least a footnote in
page 149 would have helped.

I think an important though somewhat less technical addition to the
user guide concerning the meaning and use of the Void and Exit domains
would indeed be quite useful.

[Waldek Hebisch]

Post by Riccardo GUIDA
section 5.3 pag 149
"An if-then-else expression always returns a value. If the else clause is missing then the entire expression returns the unique value of Void. If both clauses are present, the type of the value returned by if is obtained by resolving the types of the values of the two clauses. See Section 2.10 on page 109 for more information." (Check also the boxed text above this statement.)
(1) -> if 1>2 then 1 -- here he expects Void
Type: Void
(2) -> if 2>1 then 1 -- here he expects Void but gets PositiveInteger
(2) 1
Type: PositiveInteger
(3) -> if 2>1 then 1 else [1,2,3] -- here he expects common supertype, but which one?
(3) 1
Type: PositiveInteger
(4) -> if 1>2 then 1 else [1,2,3] -- here he expects common supertype, which one?
(4) [1, 2, 3]
Type: List(PositiveInteger)
3) The user is puzzled because

The command line is not representative of FriCAS language. On command
line interpreter evaluates things so can use actual values to guess
what would be useful. In the process it breaks several normal rules.

Try:

f(x) == if (x > 1) then 1
Type: Void
Time: 0 sec
(7) -> f(2)
Compiling function f with type PositiveInteger -> Void
Type: Void
Time: 0.02 (OT) = 0.02 sec
(8) -> f(0)
Compiling function f with type NonNegativeInteger -> Void
Type: Void
Time: 0.01 (OT) = 0.01 sec

In both cases you now get Void. Unlike Spad compiler trying to
declare type does not change the result:

(9) -> f2(x : Integer) : Integer == if (x > 1) then 1
Function declaration f2 : Integer -> Integer has been added to
workspace.
Type: Void
Time: 0 sec
(10) -> f2(2)
Compiling function f2 with type Integer -> Integer
Conversion failed in the compiled user function f2 .

Cannot convert the value from type Void to Integer .

(10) -> f2(0)
Conversion failed in the compiled user function f2 .

Cannot convert the value from type Void to Integer .

[Bill Page]

On Fri, Jun 29, 2018 at 11:22 AM, Waldek Hebisch

Post by Waldek Hebisch

Post by Riccardo GUIDA
...
3) The user is puzzled because

The command line is not representative of FriCAS language.

In my opinion it should be (almost) representative of FriCAS language (SPAD).

Post by Waldek Hebisch
On command line interpreter evaluates things so can use actual values
to guess what would be useful.

Yes, one should expect that the interpreter would try harder to guess
reasonable types in order to relieve the user of (some) of this
responsibility.

Post by Waldek Hebisch
In the process it breaks several normal rules.
f(x) == if (x > 1) then 1
Type: Void
Time: 0 sec
(7) -> f(2)
Compiling function f with type PositiveInteger -> Void
Type: Void
Time: 0.02 (OT) = 0.02 sec
(8) -> f(0)
Compiling function f with type NonNegativeInteger -> Void
Type: Void
Time: 0.01 (OT) = 0.01 sec
In both cases you now get Void.

Clearly this is a very poor (though technically correct) guess as to
what the user might have wanted.

Post by Waldek Hebisch
(9) -> f2(x : Integer) : Integer == if (x > 1) then 1
Function declaration f2 : Integer -> Integer has been added to
workspace.
Type: Void
Time: 0 sec
(10) -> f2(2)
Compiling function f2 with type Integer -> Integer
Conversion failed in the compiled user function f2 .
Cannot convert the value from type Void to Integer .
(10) -> f2(0)
Conversion failed in the compiled user function f2 .
Cannot convert the value from type Void to Integer .

I cannot see any advantage in having this behavior in the
interpreter.I think the interpreter should be changed to do the same
thing as the Spad compiler. The function should attempt to coerce the
result of the if-then expression

if (x > 1) then 1

to Integer. Of course this might cause an error for certain values of
x but the user is not likely to be surprised by this.

[Waldek Hebisch]

Post by Bill Page
On Fri, Jun 29, 2018 at 11:22 AM, Waldek Hebisch

Post by Waldek Hebisch

Post by Riccardo GUIDA
...
3) The user is puzzled because

The command line is not representative of FriCAS language.

In my opinion it should be (almost) representative of FriCAS language (SPAD).

Post by Waldek Hebisch
On command line interpreter evaluates things so can use actual values
to guess what would be useful.

Yes, one should expect that the interpreter would try harder to guess
reasonable types in order to relieve the user of (some) of this
responsibility.

Post by Waldek Hebisch
In the process it breaks several normal rules.
f(x) == if (x > 1) then 1
Type: Void
Time: 0 sec
(7) -> f(2)
Compiling function f with type PositiveInteger -> Void
Type: Void
Time: 0.02 (OT) = 0.02 sec
(8) -> f(0)
Compiling function f with type NonNegativeInteger -> Void
Type: Void
Time: 0.01 (OT) = 0.01 sec
In both cases you now get Void.

Clearly this is a very poor (though technically correct) guess as to
what the user might have wanted.

Maybe I should say more: compiling a function interpreter can _not_
use value, the function has to work for any value of argument, so
in compiled function interpreter has to obey rules. In command
line expression interpreter can use values. Sometime you get
message that compilation failed, and that function will be
interpreted. In such case interpreter uses similar rules as
on command line. However, for serious computation such cases
should be avoided because assigning types takes quite a lot
of time. In compiled functions this is done once per type,
when interpreting type assignment is re-done on every execution
of a statement.

Post by Bill Page

Post by Waldek Hebisch
(9) -> f2(x : Integer) : Integer == if (x > 1) then 1
Function declaration f2 : Integer -> Integer has been added to
workspace.
Type: Void
Time: 0 sec
(10) -> f2(2)
Compiling function f2 with type Integer -> Integer
Conversion failed in the compiled user function f2 .
Cannot convert the value from type Void to Integer .
(10) -> f2(0)
Conversion failed in the compiled user function f2 .
Cannot convert the value from type Void to Integer .

I cannot see any advantage in having this behavior in the
interpreter.

Well, advantage is consistency with rules.

Post by Bill Page
I think the interpreter should be changed to do the same
thing as the Spad compiler. The function should attempt to coerce the
result of the if-then expression
if (x > 1) then 1
to Integer. Of course this might cause an error for certain values of
x but the user is not likely to be surprised by this.

Well, there are folks that want static checking, that is no type
errors at runtime. They prefer Void as a result type. And
there are folks who want to bend the rules. IMO some sloppines
on command line is OK. But already for "interpreter" functions
stricter type rules may be beneficial.

Of course, having more relaxed rule in Spad compiler and stricter
rule in intepreter is counterintuitive. The only explanation I
see is that original authors decided to change rules. Remember
that Spad is "old compiler" and compiler included in intepreter
is "new compiler".

[Bill Page]

On Sat, Jun 30, 2018 at 9:40 AM, Waldek Hebisch

Post by Waldek Hebisch

Post by Bill Page
On Fri, Jun 29, 2018 at 11:22 AM, Waldek Hebisch

Post by Waldek Hebisch
On command line interpreter evaluates things so can use actual
values to guess what would be useful.

Yes, one should expect that the interpreter would try harder to
guess reasonable types in order to relieve the user of (some)
of this responsibility.

Post by Waldek Hebisch
In the process it breaks several normal rules.
f(x) == if (x > 1) then 1
Type: Void
Time: 0 sec
(7) -> f(2)
Compiling function f with type PositiveInteger -> Void
Type: Void
Time: 0.02 (OT) = 0.02 sec
(8) -> f(0)
Compiling function f with type NonNegativeInteger -> Void
Type: Void
Time: 0.01 (OT) = 0.01 sec
In both cases you now get Void.

Clearly this is a very poor (though technically correct) guess as
to what the user might have wanted.

Maybe I should say more: compiling a function interpreter can
_not_ use value, the function has to work for any value of
argument, so in compiled function interpreter has to obey rules.

OK. I understand the distinction.

Post by Waldek Hebisch
In command line expression interpreter can use values.
Sometime you get message that compilation failed, and
that function will be interpreted. In such case interpreter
uses similar rules as on command line. However, for serious
computation such cases should be avoided because assigning
types takes quite a lot of time. In compiled functions this is
done once per type, when interpreting type assignment is
re-done on every execution of a statement.

Yes. There is a system command:

)set function compile off/on (on by default)

which is described as

compile compile, don't just define function bodies

but when I set function compile off, I still got the following result:

(1) -> )set function compile off
(1) -> f2(x : Integer) : Integer == if (x > 1) then 1
Function declaration f2 : Integer -> Integer has been added to
workspace.
Type: Void
(2) -> f2(2)
Compiling function f2 with type Integer -> Integer
Conversion failed in the compiled user function f2 .

Cannot convert the value from type Void to Integer .

--

Does this option still work? Perhaps my expectation was wrong.

Post by Waldek Hebisch

Post by Bill Page
...
I cannot see any advantage in having this behavior in the
interpreter.

Well, advantage is consistency with rules.

Could you site specifically what rule is being violated?

Post by Waldek Hebisch

Post by Bill Page
I think the interpreter should be changed to do the same
thing as the Spad compiler. The function should attempt to coerce
the result of the if-then expression
if (x > 1) then 1
to Integer. Of course this might cause an error for certain values
of x but the user is not likely to be surprised by this.

Well, there are folks that want static checking, that is no type
errors at runtime. They prefer Void as a result type. And
there are folks who want to bend the rules. IMO some sloppines
on command line is OK. But already for "interpreter" functions
stricter type rules may be beneficial.
Of course, having more relaxed rule in Spad compiler and stricter
rule in intepreter is counterintuitive. The only explanation I
see is that original authors decided to change rules. Remember
that Spad is "old compiler" and compiler included in intepreter
is "new compiler".

In fact the Spad compiler does not always do what I had hoped. For
example compiling the following function using Spad:

f(x:Integer):PositiveInteger == if x<1 then 1

--

(1) -> f(0)

(1) 1
Type: PositiveInteger
(2) -> f(1)
Internal Error
Interpreter code generation failed for expression(|f| 1)

--

This is a rather unexpected and obscure errror message. However it is
possible to compile explicit code such as:

g(x:Integer):PositiveInteger == coerce((if x<1 then 1 else
void()$Void)::Union(Void,PositiveInteger))

--

2) -> g(0)

(2) 1
Type: PositiveInteger
(3) -> g(1)
"()" of mode Union(Void,PositiveInteger) cannot be coerced to mode
PositiveInteger

--

which does do what I had hoped, i.e. that the code generated for f
would be essentially the same as g.

[Waldek Hebisch]

Post by Bill Page
On Sat, Jun 30, 2018 at 9:40 AM, Waldek Hebisch

Post by Waldek Hebisch

Post by Bill Page
On Fri, Jun 29, 2018 at 11:22 AM, Waldek Hebisch

Post by Waldek Hebisch
On command line interpreter evaluates things so can use actual
values to guess what would be useful.

Yes, one should expect that the interpreter would try harder to
guess reasonable types in order to relieve the user of (some)
of this responsibility.

In command line expression interpreter can use values.
Sometime you get message that compilation failed, and
that function will be interpreted. In such case interpreter
uses similar rules as on command line. However, for serious
computation such cases should be avoided because assigning
types takes quite a lot of time. In compiled functions this is
done once per type, when interpreting type assignment is
re-done on every execution of a statement.

)set function compile off/on (on by default)
which is described as
compile compile, don't just define function bodies
(1) -> )set function compile off
(1) -> f2(x : Integer) : Integer == if (x > 1) then 1
Function declaration f2 : Integer -> Integer has been added to
workspace.
Type: Void
(2) -> f2(2)
Compiling function f2 with type Integer -> Integer
Conversion failed in the compiled user function f2 .
Cannot convert the value from type Void to Integer .
--
Does this option still work? Perhaps my expectation was wrong.

"Compile" have many meanings. The option concerns _Lisp_ compilation.
I wrote about higher level, where compilation assentially means
type assignment. AFAIK intepreter always tries to compile that
is perform types assignment. Only when it fails function is
interpteted (and this is lot slower then executiong function
compilered by interpteter to Lisp and intepreted by Lisp
implementation).

Post by Bill Page

Post by Waldek Hebisch

Post by Bill Page
...
I cannot see any advantage in having this behavior in the
interpreter.

Well, advantage is consistency with rules.

Could you site specifically what rule is being violated?

The one that Ricardo was asking about: that 'if' always works,
but for one armed 'if' you get Void as a type.

Post by Bill Page

Post by Waldek Hebisch

Post by Bill Page
I think the interpreter should be changed to do the same
thing as the Spad compiler. The function should attempt to coerce
the result of the if-then expression
if (x > 1) then 1
to Integer. Of course this might cause an error for certain values
of x but the user is not likely to be surprised by this.

Well, there are folks that want static checking, that is no type
errors at runtime. They prefer Void as a result type. And
there are folks who want to bend the rules. IMO some sloppines
on command line is OK. But already for "interpreter" functions
stricter type rules may be beneficial.
Of course, having more relaxed rule in Spad compiler and stricter
rule in intepreter is counterintuitive. The only explanation I
see is that original authors decided to change rules. Remember
that Spad is "old compiler" and compiler included in intepreter
is "new compiler".

In fact the Spad compiler does not always do what I had hoped. For
f(x:Integer):PositiveInteger == if x<1 then 1
--
(1) -> f(0)
(1) 1
Type: PositiveInteger
(2) -> f(1)
Internal Error
Interpreter code generation failed for expression(|f| 1)

The message looks fishy. Do you really used _Spad_ function here?
The message looks like coming from interpreter and given Spad
function of correct type interpreter should just blindly call it.

Post by Bill Page
--
This is a rather unexpected and obscure errror message.

[Bill Page]

On Sat, Jun 30, 2018 at 11:30 AM, Waldek Hebisch

Post by Waldek Hebisch

Post by Bill Page

Post by Waldek Hebisch
Well, advantage is consistency with rules.

Could you site specifically what rule is being violated?

The one that Ricardo was asking about: that 'if' always works,
but for one armed 'if' you get Void as a type.

Post by Bill Page
...
In fact the Spad compiler does not always do what I had hoped. For
f(x:Integer):PositiveInteger == if x<1 then 1
--
(1) -> f(0)
(1) 1
Type: PositiveInteger
(2) -> f(1)
Internal Error
Interpreter code generation failed for expression(|f| 1)

The message looks fishy. Do you really used _Spad_ function here?

Yes, here is the exact code that I compiled:

-- file: one-armed.spad
)abbrev domain TEST Test
Test(): with
test1: ()->Integer
test2: ()->Void
f:Integer -> PositiveInteger
g:Integer -> PositiveInteger
h:Integer -> PositiveInteger
== add
z:Integer := 1
test1() ==
A := if z<2 then 1
return A
test2() ==
B := if 2<1 then 1
return B

f(x:Integer):PositiveInteger == if x<1 then 1
g(x:Integer):PositiveInteger == coerce((if x<1 then 1 else
void()$Void)::Union(Void,PositiveInteger))
h(x:Integer):PositiveInteger == g(x)+1
--

This is the result:

(1) -> )co one-armed
Compiling FriCAS source code from file /home/wspage/one-armed.spad
using old system compiler.
TEST abbreviates domain Test
...
Test is now explicitly exposed in frame frame1
Test will be automatically loaded when needed from
/home/wspage/TEST.NRLIB/TEST

(1) -> f(0)

(1) 1
Type: PositiveInteger
(2) -> f(1)
Internal Error
Interpreter code generation failed for expression(|f| 1)

(2) -> g(0)

(2) 1
Type: PositiveInteger
(3) -> g(1)
"()" of mode Union(Void,PositiveInteger) cannot be coerced to mode
PositiveInteger

(3) -> h(0)

(3) 2
Type: PositiveInteger
(4) -> h(1)
"()" of mode Union(Void,PositiveInteger) cannot be coerced to mode
PositiveInteger

(4) ->

Post by Waldek Hebisch
The message looks like coming from interpreter and given
Spad function of correct type interpreter should just blindly
call it.

Yes, I thought so too.

[Bill Page]

Post by Bill Page
...
(2) -> f(1)
Internal Error
Interpreter code generation failed for expression(|f| 1)
...
On Sat, Jun 30, 2018 at 11:30 AM, Waldek Hebisch

Post by Waldek Hebisch
The message looks like coming from interpreter and given
Spad function of correct type interpreter should just blindly
call it.

Yes, I thought so too.

Actually I just realized that this sort of error was already
anticipated by Oldk1331. It looks like evaluating the function f(1)
returns the wrong value for Void - NIL instead of voidValue().

See the comment about "getArgValue" in the following patch:

---------- Forwarded message ----------
From: oldk1331 <***@gmail.com>
Date: Tue, Jun 12, 2018 at 9:37 AM
Subject: [fricas-devel] [PATCH] Void is the unit type, fix doc and
cleanup (use 0 as representation)
To: fricas-devel <fricas-***@googlegroups.com>


Clearly domain "Void" is the unit type:
https://en.wikipedia.org/wiki/Unit_type

So I'm clearing this up.



diff --git a/src/algebra/any.spad b/src/algebra/any.spad
index 02602da6..4d46a77c 100644
--- a/src/algebra/any.spad
+++ b/src/algebra/any.spad
@@ -168,31 +168,28 @@
error "Cannot retract value."

)abbrev domain VOID Void
--- These types act as the top and bottom of the type lattice
--- and are known to the compiler and interpreter for type resolution.
++ Author: Stephen M. Watt
++ Date Created: 1986
++ Basic Operations:
++ Related Domains: ErrorFunctions, ResolveLatticeCompletion, Exit
++ Also See:
++ AMS Classifications:
-++ Keywords: type, mode, coerce, no value
+++ Keywords: type, mode, coerce, unit type
++ Examples:
++ References:
++ Description:
-++ This type is used when no value is needed, e.g., in the \spad{then}
-++ part of a one armed \spad{if}.
+++ \spadtype{Void} implements the unit type in type theory.
+++ It allows only one value thus can hold no information.
+++ Void is used in the \spad{then} part of a one armed \spad{if}.
++ All values can be coerced to type Void. Once a value has been coerced
++ to Void, it cannot be recovered.

-Void : with
- void : () -> % ++ void() produces a void object.
- coerce : % -> OutputForm
- ++ coerce(v) coerces void object to OutputForm.
+Void : CoercibleTo OutputForm with
+ void : () -> %
+ ++ void() returns the void object.
== add
- Rep := String
- void() == voidValue()$Lisp
- coerce(v : %) == coerce(void())$Rep
+ void() == voidValue()$Lisp
+ coerce(v : %) == message "()"

)abbrev domain EXIT Exit
++ Author: Stephen M. Watt
diff --git a/src/interp/i-spec1.boot b/src/interp/i-spec1.boot
index 863355a7..4f92dede 100644
--- a/src/interp/i-spec1.boot
+++ b/src/interp/i-spec1.boot
@@ -81,9 +81,11 @@
DEFPARAMETER($breakCount, 0)
DEFPARAMETER($anonymousMapCounter, 0)

---% Void stuff
+--% Void is the unit type that allows only one value.
+--% It can be anything and we use 0 here.
+--% It can't be NIL, see function "getArgValue" in "interpret1".

-voidValue() == '"()"
+voidValue() == 0

--% Handlers for Anonymous Function Definitions

--

[Riccardo GUIDA]

Post by Bill Page
If the else clause is missing but the if condition is false then the
value of the if-then expression is the unique value of Void.

+1

Post by Bill Page
I think an important though somewhat less technical addition to the
user guide concerning the meaning and use of the Void and Exit domains
would indeed be quite useful.

+1

(Maybe adding also something on None if this Type will still be around. Somewhere near section 2.6 might be a good place.)

@ Waldek

Post by Bill Page
The command line is not representative of FriCAS language.

OK, crystal clear.

The pedagogical problem is that, maybe not to scare the reader, the FricasUG is somehow vague on the differences among interpreter and compiler. For instance note that the chapter 5 (which raised my questions) is titled "Introduction to the FriCAS Interactive Language", while it is presently more like an (incomplete) SPAD reference.

riccardo

[Waldek Hebisch]

Post by Riccardo GUIDA
@ Waldek

Post by Waldek Hebisch
The command line is not representative of FriCAS language.

OK, crystal clear.
The pedagogical problem is that, maybe not to scare the reader, the FricasUG is somehow vague on the differences among interpreter and compiler. For instance note that the chapter 5 (which raised my questions) is titled "Introduction to the FriCAS Interactive Language", while it is presently more like an (incomplete) SPAD reference.

You seem to use different terminology. Spad is language of .spad files.
They are intended for non-interactive use -- basicaly enhancements to
FriCAS library. Spad is different than language of .input files.
.input files are intended for interactive use. Now, with "interactive
language" there is some confusion, as functions are normally compiled
while command line gets special treatment.

[Riccardo GUIDA]

Post by Waldek Hebisch
You seem to use different terminology. Spad is language of .spad files.
They are intended for non-interactive use -- basicaly enhancements to
FriCAS library. Spad is different than language of .input files.
.input files are intended for interactive use. Now, with "interactive
language" there is some confusion, as functions are normally compiled
while command line gets special treatment.

Dear Waldek,

to explain: my answer relied on the following hypotheses

* SPAD is the language of .spad files, invoked by )compile
* the interpreter =
interprets a subset of SPAD language (eg no definitions of domain) on command line and via )read .input files
+ heuristics guesses & coercitions on types
+ SPAD compilation of functions in case of complete type resolutions


... so naively I thought that, if the interpreter is so unpredictable on types, maybe it was more pedagogical to present things as subsets of SPAD, which is well defined, but now I realize that maybe the examples given maybe do not compile in SPAD, even if embedded in functions of user-defined packages, I do not know, I'm learning using the command line.


I guess I need some official glossary, could you please enlighten me?

* How should be called "The language of .input files?"

* Is "The language of .input files" the same thing as "the language of command line"?, and if not how is called the latter?

* Is the compiler invoked by the interpreter when compiling functions the same compiler (same language) as the SPAD compiler invoked by )compile ?

* Which language is meant by 'The FriCAS language' and 'The FriCAS interactive language'?

A post on a related question will follow.

riccardo

[Waldek Hebisch]

Post by Riccardo GUIDA

Post by Waldek Hebisch
You seem to use different terminology. Spad is language of .spad files.
They are intended for non-interactive use -- basicaly enhancements to
FriCAS library. Spad is different than language of .input files.
.input files are intended for interactive use. Now, with "interactive
language" there is some confusion, as functions are normally compiled
while command line gets special treatment.

Dear Waldek,
to explain: my answer relied on the following hypotheses
* SPAD is the language of .spad files, invoked by )compile

Yes

Post by Riccardo GUIDA
* the interpreter =
interprets a subset of SPAD language (eg no definitions of domain) on command line and via )read .input files

not "a subset" but rather "a variant". Once you get to tiny details
it make sense to treat it a a separate language, very similar, but
not identical to Spad.

Post by Riccardo GUIDA
+ heuristics guesses & coercitions on types
+ SPAD compilation of functions in case of complete type resolutions

No Spad. Despite the name interpreter is a full-fledged compiler.
It has "interpret" mode for cases where it can not assign
types during compilation and for cases when value is requested.

Post by Riccardo GUIDA
... so naively I thought that, if the interpreter is so unpredictable on types, maybe it was more pedagogical to present things as subsets of SPAD, which is well defined, but now I realize that maybe the examples given maybe do not compile in SPAD, even if embedded in functions of user-defined packages, I do not know, I'm learning using the command line.
I guess I need some official glossary, could you please enlighten me?
* How should be called "The language of .input files?"

On the list we usually write about "interpeter". If you want
to be more precise use "interpeter language". This is what
FriCAS book calls "interactive language".

Post by Riccardo GUIDA
* Is "The language of .input files" the same thing as "the language of command line"?, and if not how is called the latter?

I affraid it is question to philosophers if it is the same or not.
Command line and .input files are handled by the same code (called
"interpreter"). But there is bunch of variables which make
things different. Main difference is that you can not make piles
on command line. There is important difference between functions (which
"interpreter" tries to compile) and code outside functions
(which is evaluated to produce a value).

There is pragmatic difference: it is incovenient to define larger
functions on command line, so they are usually defined in .input
files. OTOH commands (code outside functions) are more useful
on command line. So pragmaticaly, rules for functions are
more important for '.input' files. Special handling for
command is more visible on command line.

Post by Riccardo GUIDA
* Is the compiler invoked by the interpreter when compiling functions the same compiler (same language) as the SPAD compiler invoked by )compile ?

No. The first stage, that is splitting input into tokens is
common to interpreter and Spad compiler. After that Spad compilation
and interpreter are separate. In particular there are two
different parsers. Different parsers means that syntax is
slightly different.

"interpreter" has two modes of operation. In one
it compiles (produces code). In other it produces values.
As I wrote there is bunch of variables which decides in
which mode "interpreter" operates.

Post by Riccardo GUIDA
* Which language is meant by 'The FriCAS language' and 'The FriCAS interactive language'?

Phrase 'The FriCAS interactive language' in FriCAS book refers to
language of '.input' files. 'The FriCAS language' is more fuzzy,
so it is useful for cases when we do not want to specify variant.

Extra explanation: all languages involved are intended to be
compatible, ideally identical. Historical developement caused
more differences than desired. To say the truth before your
original message I was happy to accept statement in FriCAS
book about type of one-armed 'if' at face value. I like
to write well-typed code so I use one-armed 'if' only in
context where 'Void' is right type. I was not aware that
Spad compiler allowed getting different type.