Bill Page wrote:
>
> 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
>
I think this is misguided: fundamental property of Void is that
its values are _not used_ in normal computation. The coercion
to OutputForm exists only because our printing and tracing routines
use it. So from fundamental point of view Void should have no
operations. Once you have no operations there is no need
for representation.
> Unfortunately the following simple patch causes the unexpected
> regression that I mentioned in a previous thread (see "bad code or
> side-effects?").
>
<snip>
> 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.
While I can not see any specific reason for failure, let me say
that what you are trying to do is asking for trouble. Namely,
since everything can be coerced to Void you risk that insted
of operation you want you will use operation from Void. Typically
coercions are homomorhisms, so spurious coercion may be performance
loss but should preserve correctness. But coercion to Void
almost surely will break things.
> In principle I do not see any reason why 'Void' needs to be canonical
> so long as equality is defined as above.
I think you are confused about names. 'None' would be a reasonable
alternative name, except that the name 'Void' is used also in other
languages (and 'None' is taken for different use). Some folks
tried to have multiple 'Void' type (lazy and eager ones IIRC),
but still 'Void' is special because it represents very special
concept. You are trying to turn 'Void' into ordinary type,
which would make is useless from compiler point of view.
> 'None' on the other hand is called a "domain without any values"
I feel that this decription is wrong. Rather it is "domian
of values with arbitrary unspecified type"
> 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:
Yes, exactly.
> 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
>
You are trying to turn 'None' into something different than
it is now an in the process you risk loosing properties that
make it useful.
'None' really does not fit category theory: if you want elegant
system you would only have 'Any'. Currently we need 'None'
to implement 'Any'.
--
Waldek Hebisch
hebi...@math.uni.wroc.pl
------------------------------------------------------------------------------
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
