Bill Page wrote:
>
> 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.
I should be really doing something else, but could not
resit so I wrote quick answer.
> 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.
>
'Void' is used in situation when there is really _no_ value. Of
course, for formal reasons you may insist that there is special
value of type 'Void' but to get efficient code we do not want
any real computations on this values.
You write about 'useful formal operations'. I wonder what
applications you have in mind? The only potential application
I have found was to use 'Void' as a filler in places where
for come reasons we need code, but we do not want real
computation. To make it a bit more clearer: when writing
generic code for some specializations we may wish to
omit some data (and related computations). For example,
to skip a record field without using explicit conditionals
one could try to pass 'Void' as type of compontent.
Unfortunatly, when it was possible do do actual computations
with void types (for example in Pascal record with no components
is legal and may serve as void type) it turned out that
compilers simply did useless computations -- Gnu Pascal compiler
internally enlarged records with no components so that they
took 1 byte and slavishy did on it computations as on real
data.
Hence my conclusion is that it is better to leave 'Void' for
compiler, because once you invent something which is one
step beyond trivial it will be too hard for compiler.
And it seems foolish to spend effort implementing trivialities.
> >> 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
>
I am rather thinking about code like:
coerce(x) = coerce(y)
Or maybe:
if D has SetCategory then
x::D = y::D
Simply you create possibilty for strange combinations and Murphy
says that once you make then possible they will happen.
> 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.
So, what type the above should have? Do you want type error?
> 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.
>
I do not expect compiler to call this coerce, but I think that
the rule above is hardcoded in the compiler. In other words
this code is useful if you want to pretend that 'Void' is
defined by algebra sources.
> >> 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).
>
I am not sure what you mean here. Currently both 'None' and
'Void' allow coercion from any domain, so both could be
candidates for "terminal" domain.
But 'None' is _not_ a terminal object: to have terminal object
you need unique mapping. In other words arrows must commute.
But we have:
(22) -> pol := x^2 + 1
2
(22) x + 1
Type: Polynomial(Integer)
(23) -> PRETTYPRINT(pol)$Lisp
(1 |x| (2 0 . 1) (0 0 . 1))
(23) ()
Type: SExpression
(24) -> (pol::InputForm)::SEX
(24) (+ (^ x 2) 1)
Type: SExpression
Coercing to None will produce different values, and consequently
arrows do not comute.
> >?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?
>
Compiler internally needs to mark places where at first glance
we need or have value, but in fact there is no value. Compiler
could use some special marker to do this, but currently having
Void type is used for this purpose. If you allow real computation
on Void you will break this usage. If you only provide operation
which are consistent with 'Void' beeing a terminal object, then
I am not sure if you gain anything (because you are still not
able to get any nontrivial result) but compiler will have some
trouble handling trivialites.
> >> '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.
It will be consitent if you do not allow anybody to discover
that values are different. But then, why to store them at
all?
>
> >> 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?
>
If you allow storing and retriving values from 'Void' it no longer
will be terminal object (by the same reasoning which currently
applies to 'None')
> >> 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
>
This would be something quite different than our current 'None'.
Now, having real initial object may be nice from category
point of view, but I am not sure if it is useful for programming.
OTOH current 'None' is useful.
> 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.
If you want categorical interpretation both seem wrong.
The second one because from terminal object you can have only
trivial arrows, which probably implies that X is trivial.
The first one may be consistent if None is really initial
object, but then it almost useless.
--
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
