On Mon, Oct 5, 2009 at 2:03 PM, Waldek Hebisch wrote:
>
> Bill Page wrote:
>> ...
>> 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.
>
I hope you do not mind continuation of this discussion. Perhaps I am
wrong but for me it seems important to agree on basic concepts such as
these. To often in the past I think the Axiom developers have started
to deal with these sort of issues but then stopped short of a good
general solution because other issues were seen as having higher
priority.
I do not agree that a value of type Void is not used in computation,
the requirement is only that we do not care what it's value is for a
particular computation. This does not preclude the definition of
certain useful formal operations on such a value. Equality is an
example. As far as I can see every domain in Axiom must have a
representation - even if it is just implicit.
>> 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 instead
> 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.
>
Axiom already has coercion to Void from every domain. This is not
something that is changed by my patch. What is a little different is
that equality is defined.
Do you mean that because we can do
x::Void = y::Void
for any domains x:X, and y:Y? This does not happen in the interpreter
and coercions must be explicit in the compiler so I am not convinced.
(1) -> test(1::Void = 2::Void)
(1) true
Type: Boolean
(2) -> test(1=2)
(2) false
Type: Boolean
On the other hand I agree that it does not really make sense that the
map from some domain to Void is called a "coercion". I would prefer
that every domain X in BasicType (including those in SetCategory)
export a special operation called:
terminal: X -> Void
The idea that Void should be automatically involved in the resolution
of types in expressions like
if n=0 then x::Integer else y::Float
does not make sense to me. See 'void.spad.pamphlet'
)abbrev package RESLATC ResolveLatticeCompletion
++ Author: Stephen M. Watt
++ Date Created: 1986
++ Date Last Updated: May 30, 1991
++ Related Domains: ErrorFunctions, Exit, Void
++ Keywords: mode, resolve, type lattice
++ Description:
++ This package provides coercions for the special types \spadtype{Exit}
++ and \spadtype{Void}.
ResolveLatticeCompletion(S: Type): with
coerce: S -> Void
++ coerce(s) throws all information about s away.
++ This coercion allows values of any type to appear
++ in contexts where they will not be used.
--
It seems to me that there are better ways to do this and it is not
even really clear to me that Axiom currently does use this straegy.
>> 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).
No I am not concerned about names. I am worried about logical
consistency. 'None' is something different, in fact quite opposite
from 'Void'. 'Void' is the empty or "initial" domain. It is (should
be) the result of an empty 'Union()'. 'Void' on the other hand is the
empty product or "terminal" domain. It should be the result of an
empty 'Record()' (or similar fundamental cross-product type).
> 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.
>
Could you explain again why you thing this change makes 'Void' useless?
>> 'None' on the other hand is called a "domain without any values"
>
> I feel that this description is wrong. Rather it is "domian
> of values with arbitrary unspecified type"
>
You could perhaps treat this the way Gaby proposed as the domain
'RuntimeValue' i.e. a domain with an unspecified *Axiom type* however
it still of course must inherit something from the underlying run time
system. For the most part 'SExpression' is already such a domain. At
least one could say that 'SExpression' and the built-in domain 'Lisp'
exposes part of this run time system.
However if all you want to do is (temporarily) ignore the type I do
not see anything wrong with my proposal that we simply allow 'Void' to
be non-canonical, i.e.
terminal(x:X) == rep(x) pretend Void
As long as we define equality as I did above this implementation
remains logically consistent.
>> 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.
>
Why do you think 'Void' can not (or should not?) be used for this purpose?
>> 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'.
>
'None' fits mathematical category theory quite well as an initial object.
http://en.wikipedia.org/wiki/Initial_and_terminal_objects
I think 'Any' is something else - the union of all domains
Union( X for X in Domain)
To implement this we need to know the values of 'Domain' and as Gaby
implied, this means having to deal with the run time system in some
way or another. As far as I can see this is currently done in Axiom
via 'pretend' together with 'SExpression' and some magic from 'Lisp'
to represent the run-time value of the type. I do not see any
immediate reason to prefer
per(x:None):% == x pretend X
instead of
per(x:Void):% == x pretend X
In fact I think the first one is logically inconsistent.
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
