We seldom seem to make much progress with foundational issues in Axiom
(where I write Axiom in this email, it should be understood that I am
also referring to FriCAS and OpenAxiom) but I thought I would like to
bring up a subject that has bother me a little and ask for comments.
'None' and 'Void' are two rather "special" domains in Axiom. It seems
that were mostly considered a "technical necessity" by the original
Axiom developers and not necessarily something of deeper significance
but I think this attitude is wrong when it comes to Axiom and can lead
to inconsistency.
'Void' is the type of the value returned when one does not want the
value, e.g. when a function is executed for it's side-effects only.
All Axiom domains can be coerced to 'Void'. According to documentation
in the source this is also used to resolve the types in an expression
like:
x:=if n=0 then a::Float else b::Integer
Printing of a "value" of type 'Void' is controlled by the command
(1) -> )set message void on
(1) -> void()
(1) "()"
Type: Void
Formally 'Void' is similar to the "value" that is passed to functions
that do not require a value. E.g.
(2) -> f()==1
(2) "()"
Type: Void
(3) -> f()
Compiling function f with type () -> PositiveInteger
(3) 1
Type: PositiveInteger
In fact logically 'Void' is closely related to the cross-product. If
'Product(X,Y)' is the domain of pairs of values (x:X, y:Y) and
'Product(X)' is just X, then 'Product()' should be 'Void'. In
reference to mathematical category theory 'Void' would be called a
'terminal' domain (object) since coercion to 'Void; is trivial and
unique. 'Void' contains a single canonical value generated by
'void()'. The domain 'Void' is used extensively throughout Axiom where
ever values are not needed.
Although it is currently a stand alone domain, 'Void' could be easily
made to satisfy 'SetCategory' by providing a simple '=' operation.
Since by definition 'Void' has only a single "canonical" value we can
simply write:
(x:% = y:%):Boolean == true
Unfortunately the following simple patch causes the unexpected
regression that I mentioned in a previous thread (see "bad code or
side-effects?").
wsp...@debian:~/fricas-src/src/algebra$ svn diff void.spad.pamphlet
Index: void.spad.pamphlet
===================================================================
--- void.spad.pamphlet (revision 675)
+++ void.spad.pamphlet (working copy)
@@ -30,13 +30,13 @@
++ All values can be coerced to type Void. Once a value has been coerced
++ to Void, it cannot be recovered.
-Void: with
+Void: SetCategory with
void: () -> % ++ void() produces a void object.
- coerce: % -> OutputForm ++ coerce(v) coerces void object to
outputForm.
== add
- Rep := String
+ Rep := SExpression
void() == voidValue()$Lisp
- coerce(v:%) == coerce(void())$Rep
+ coerce(v:%):OutputForm == coerce(void())$Rep
+ (x:% = y:%):Boolean == true
@
\section{domain EXIT Exit}
@@ -60,7 +60,7 @@
++ type Exit. This allows, for example, errors to be raised in
++ one half of a type-balanced \spad{if}.
Exit: SetCategory == add
- coerce(n:%) == error "Cannot use an Exit value."
+ coerce(n:%):OutputForm == error "Cannot use an Exit value."
n1 = n2 == error "Cannot use an Exit value."
@
I do not yet know why this causes a regression and because 'Void' is
used so extensively it might be hard to track down on a case-by-case
basis.
BTW, I don't understand why the current 'Rep' of 'Void' is 'String'.
Changing it to 'SExpression" has the nice side-effect of avoiding the
"..." in the value of 'Void' if/when it is displayed.
In principle I do not see any reason why 'Void' needs to be canonical
so long as equality is defined as above. This would mean that values
from other domains could be coerced to 'Void' without changing their
underlying representation. Although the type information is lost by
the coercion, it could still be recovered in specific situations such
as those discussed below.
'None' on the other hand is called a "domain without any values" but
it is typically used in situations where one apparently needs to
temporarily avoid (duck?) the type checking, e.g. in the domain 'Any',
but also in several other places in Axiom:
algfunc.spad.pamphlet
any.spad.pamphlet
combfunc.spad.pamphlet
exposed.lsp.pamphlet
expr.spad.pamphlet
fspace.spad.pamphlet
kl.spad.pamphlet
laplace.spad.pamphlet
liouv.spad.pamphlet
opalg.spad.pamphlet
op.spad.pamphlet
rec.spad.pamphlet
In spite of the fact that 'None' is supposed to have no values, it
does export 'SetCategory' and equality is defined in terms of the
underlying Lisp equality 'EQ'. I think this is fundamentally wrong
however as far as I can see this equality is never called in Axiom.
>From the point of view of mathematical category theory 'None' should
be an initial domain. If 'None' is supposed to satisfy 'SetCategory'
then equality in this domain should be defined as follows:
(x:% = y:%):Boolean == false
and the function 'None->X' for any domain X in 'SetCategory' should be
trivial and unique. Since 'None' has no values this function is never
actually evaluated but might be important for other reasons (although
I can not think of one right now). Similarly, there should be no
coercion of other values into 'None'.
As far as I can see everything that is done by 'None' in Axiom right
now can easily and more consistently be done by 'Void'.
So I would like to replace 'None' with 'Void', make 'None' logically
correct and 'void' satisfy 'SetCategory'. is anyone else here
interested and think that this is important? Any ideas about how to
debug the above patch would be greatly appreciated.
Regards,
Bill Page.
------------------------------------------------------------------------------
Come build with us! The BlackBerry® Developer Conference in SF, CA
is the only developer event you need to attend this year. Jumpstart your
developing skills, take BlackBerry mobile applications to market and stay
ahead of the curve. Join us from November 9-12, 2009. Register now!
http://p.sf.net/sfu/devconf
_______________________________________________
open-axiom-devel mailing list
open-axiom-devel@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/open-axiom-devel
