[fricas-devel] [PATCH] None is the top type, fix documentation

[oldk1331]

Domain "None" is the top type in type theory:

https://en.wikipedia.org/wiki/Top_type



diff --git a/src/algebra/any.spad b/src/algebra/any.spad
index ada256fe..8a5b00d6 100644
--- a/src/algebra/any.spad
+++ b/src/algebra/any.spad
@@ -6,15 +6,19 @@
++ AMS Classification:
++ Keywords: none
++ Description:
-++ \spadtype{None} implements an universal type, that is type
+++ \spadtype{None} implements the top type (also known as universal type)
+++ in type theory. It is the type
++ which can represent values of any normal type. It is mainly
++ used in technical situations where such a thing is needed (e.g.
++ the interpreter and some of the internal \spadtype{Expression}
++ code).

-None() : SetCategory == add
+None() : CoercibleTo OutputForm with
+ eq? : (%, %) -> Boolean
+ ++ eq?(x, y) returns true if x and y are the same object at Lisp Level.
+ == add
coerce(none : %) : OutputForm == message("NONE")
- x : % = y : % == EQ(x, y)$Lisp
+ eq?(x, y) == EQ(x, y)$Lisp

)abbrev package NONE1 NoneFunctions1
++ Author:
diff --git a/src/algebra/opalg.spad b/src/algebra/opalg.spad
index 07dd772a..582bdaaf 100644
--- a/src/algebra/opalg.spad
+++ b/src/algebra/opalg.spad
@@ -41,7 +41,6 @@
++ makeop should be local but conditional

Implementation ==> FAB add
- import from NoneFunctions1(%)
import from BasicOperatorFunctions1(M)

Rep := FAB

[Waldek Hebisch]

Post by oldk1331
https://en.wikipedia.org/wiki/Top_type

We had discussions about None, Void and probably also Exit in
the past. People have nice ideas how to cleanly integrate
them into type system. But the botton line is: None is really
a big hole in type system, breaking normal rules. Exit
and to same degree Void are hardwired into compiler to
get specific functionality. Claiming clean semantics of
those types with current compiler is more or less misleading.

I do not see why you want to change code here: the types are
closely tied to compiler and seem to contain what is needed
(and probably nothing more). Trying to change them risks
obscure bugs. Any change there requires serious analysis
of effects.

[oldk1331]

On Thu, Jun 14, 2018 at 2:54 AM, Waldek Hebisch

Post by Waldek Hebisch

Post by oldk1331
https://en.wikipedia.org/wiki/Top_type

We had discussions about None, Void and probably also Exit in
the past. People have nice ideas how to cleanly integrate
them into type system. But the botton line is: None is really
a big hole in type system, breaking normal rules. Exit
and to same degree Void are hardwired into compiler to
get specific functionality. Claiming clean semantics of
those types with current compiler is more or less misleading.

Yes, because None/Void/Exit have specials places in type theory,
they are hard coded into compiler. We should recognize this.
(Exit is related with error handling, Void is related with one-arm-if,
None is related with coercion.) I have follow up commits that
improve the compiler bits that deals with None/Void/Exit.

Post by Waldek Hebisch
I do not see why you want to change code here: the types are
closely tied to compiler and seem to contain what is needed
(and probably nothing more). Trying to change them risks
obscure bugs. Any change there requires serious analysis
of effects.

I'm only modifying the Spad part right now, and mostly removing
signatures that no one uses. These changes are safe.