On Wed, Jun 27, 2018 at 5:15 PM, Ralf Hemmecke <r...@hemmecke.org> wrote:
> 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
>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"?
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).
>
> 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.
> So the Book uses the word "value" with different meanings.
In this instance the book is correct.
> 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).
> 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
> 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
>> System error:
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.
--
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+unsubscr...@googlegroups.com.
To post to this group, send email to fricas-devel@googlegroups.com.
Visit this group at https://groups.google.com/group/fricas-devel.
For more options, visit https://groups.google.com/d/optout.
