[fricas-devel] [PATCH] Void is the unit type, fix doc and cleanup (use 0 as representation)

[oldk1331]

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

[Bill Page]

Post by oldk1331
https://en.wikipedia.org/wiki/Unit_type
So I'm clearing this up.

I think that fixes and better documentation of the Void, Exit, and
None domains are quite welcome but still warrant some discussion. From
a formal linguistic or categorical point of view Void (terminal
object) and Exit (initial object) are more important than they look.
As a category, FriCAS domains should form at least a Cartesian
category (although I think an even better model might be a topos).

However I am uncertain about your proposed changes to Void. Why do you
prefer a value of 0 instead of the symbol "()"? Note of course that
this is a Lisp symbol and not Lisp NIL. Although the value can be
anything, as the empty tuple, I think () is more intuitive than 0. A
value of 0 might be a bit confusing since the unit *type* is usually
denoted by 1, not 0. I see no harm in letting the Rep for Void be
String. In fact why not just define

void() == "()"

Is the Lisp function call voidValue really important for some reason
like in-line optimization?

Also, why did you make the following changes in Exit?

- coerce(n:%) == error "Cannot use an Exit value."
- n1 = n2 == error "Cannot use an Exit value."

From a formal point of view I am not certain at all about None. Since
FriCAS is a statically typed language I think it would be nice if None
could be eliminated from the library. FriCAS already has the type Any
which implements a type-correct version of "duck typing" and plays the
role of a universal type.

[oldk1331]

Post by Bill Page
However I am uncertain about your proposed changes to Void. Why do you
prefer a value of 0 instead of the symbol "()"? Note of course that
this is a Lisp symbol and not Lisp NIL. Although the value can be
anything, as the empty tuple, I think () is more intuitive than 0. A
value of 0 might be a bit confusing since the unit *type* is usually
denoted by 1, not 0. I see no harm in letting the Rep for Void be
String. In fact why not just define
void() == "()"

The underlying value of Void is not important, because the type Void
can only have one possible value. I don't want to use string because of
possible memory waste.

Post by Bill Page
Is the Lisp function call voidValue really important for some reason
like in-line optimization?

'voidValue' is used a few places in the compiler.

Post by Bill Page
Also, why did you make the following changes in Exit?
- coerce(n:%) == error "Cannot use an Exit value."
- n1 = n2 == error "Cannot use an Exit value."

Because Exit is the bottom type, no variable can have an Exit value,
therefore, it can't be printed or compared. When encountering Exit
type, the function aborts.

Post by Bill Page
From a formal point of view I am not certain at all about None. Since
FriCAS is a statically typed language I think it would be nice if None
could be eliminated from the library. FriCAS already has the type Any
which implements a type-correct version of "duck typing" and plays the
role of a universal type.

None as the top type is very necessary. The difference between Any and None
is that Any contains the value and type, None just contains the value. None is
widely used and can't be replaced. Although I think "None" is a terrible name.

[Bill Page]

Post by oldk1331

Post by Bill Page
However I am uncertain about your proposed changes to Void. Why do you
prefer a value of 0 instead of the symbol "()"? Note of course that
this is a Lisp symbol and not Lisp NIL. Although the value can be
anything, as the empty tuple, I think () is more intuitive than 0. A
value of 0 might be a bit confusing since the unit *type* is usually
denoted by 1, not 0. I see no harm in letting the Rep for Void be
String. In fact why not just define
void() == "()"

The underlying value of Void is not important, because the type Void
can only have one possible value. I don't want to use string because of
possible memory waste.

Does storing 0 take less space than a pointer to a string?

Post by oldk1331

Post by Bill Page
Is the Lisp function call voidValue really important for some reason
like in-line optimization?

'voidValue' is used a few places in the compiler.

OK. Maybe a global constant would be better?

Post by oldk1331

Post by Bill Page
Also, why did you make the following changes in Exit?
- coerce(n:%) == error "Cannot use an Exit value."
- n1 = n2 == error "Cannot use an Exit value."

Because Exit is the bottom type, no variable can have an Exit value,
therefore, it can't be printed or compared. When encountering Exit
type, the function aborts.

OK. A domain with no value is a categorical necessity (e.g. initial
object). You are right of course that the coding is non-functional
though perhaps it serves as a kind of documentation.

Post by oldk1331

Post by Bill Page
From a formal point of view I am not certain at all about None. Since
FriCAS is a statically typed language I think it would be nice if None
could be eliminated from the library. FriCAS already has the type Any
which implements a type-correct version of "duck typing" and plays the
role of a universal type.

None as the top type is very necessary. The difference between Any and None
is that Any contains the value and type, None just contains the value.

You should not think of FriCAS domains as "containers". A variable may
"contain" or a function may "return" something of a given type but as
types domains do not contain values.

Post by oldk1331
None is widely used and can't be replaced. Although I think "None" is a terrible name.

I disagree. None is both unnecessary and harmful, leading to many
potentially unsafe uses of 'pretend'

It is true that 'None' is currently used in the following 22 spad
files in FriCAS:

algfunc any combfunc exposed expr files fortout fspace jet kl
laplace liouv mkfunc omcat omdev op opalg openmath rdeefx rec table
xhash

with 'op' and domains that use properties being the worst offenders.

As an experiment I re-coded None as Any in the case of properties in
the following branch

https://github.com/billpage/fricas/tree/NotNone

There are 118 fewer uses of 'pretend'.

Now only the following uses of None remain:

any files fortout mkfunc omcat omdev openmath tablexhash

These cases can also be easily eliminated. As a result of this
re-coding the compiler was able to detect two cases of unsafe but
benign type errors (fixed in separate commits).

Timing of 'src/input/make' shows that no significant performance
penalty is incurred for safer coding.