On Mon, Oct 5, 2009 at 6:37 PM, Waldek Hebisch wrote: > Bill Page wrote: >> I hope you do not mind continuation of this discussion. > > I should be really doing something else, but could not > resist so I wrote quick answer. >
Thanks. :-) i do appreciate that this discussion might seem too "philosophical" and you might have the feeling that it would be better to spend time on something else. Still I would prefer it if we could reach some kind of agreement or at least understand why we don't agree. I will certainly try, where possible, to backup this discussion with actual code. > ... > 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. > I agree that ideally 'Void' and 'None' should be essentially trivial and that they should be known and handled by the compiler in the same way that 'Record' and 'Union' are handled now - although of course the treatment of all of these could be better than it is now. It may seem foolish to spend time implementing trivialities but it if we do not get the trivial things correct I think it almost always makes implementing non-trivial things in a consistent and general manner that much harder. >> ... >> 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? > A good type for if n=0 then x::Integer else y::Float might be 'Union(Integer,Float)'. Such a construction is "free" in the sense that 'Union' implements a corresponding 'case'. >> ... >> 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. For the domains in 'SetCategory' it does not make sense that there is an operation that maps values from some domain into 'None' since there are not supposed to be any values in 'None'. 'None' is an *initial* domain which means that for every domain X in 'SetCategory', there exists exactly one (trivial) operation with the signature 'None -> X'. > But 'None' is _not_ a terminal object: to have terminal object > you need unique mapping. I agree that 'None' is not a terminal object but 'Void' is a terminal object which just means that for every domain X in 'SetCategory' there exists a single unique (and trivial) operation with signature 'X->Void'. In fact any one-element domain in 'SetCategory' can be considered a terminal domain since then there is only one way to define an operation to produce such a value from any given domain. 'Void' is just singled-out as a canonical representative of all such domains. > In other words arrows must commute. I do not understand what you mean by commute in this context. > 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 commute. > Coercing something to 'None' is logically inconsistent. But there is always a unique way to map anything to 'Void'. Internally (inside Void) the representation of these values might be different but as long as equality is defined properly, externally they all represent the "same" value of 'Void'. > > 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. What do you mean by "real computation". Is an operation such as (x:% = y:%) == true a real computation? Rather than being defined in the library this fact could simply be "known" to the compiler and no real computation would be necessary. > If you only provide operation which are consistent with 'Void' > being 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. The properties of 'Void' as a domain in 'SetCategory' are important for the formal definition of 'SetCategory' as the (mathematical) category of sets. Although 'Void' itself is (mostly) trivial, the proper definition makes the definition of other not-so-trivial things possible. In principle I do not understand why the compiler should have trouble handling such trivialities, although in practice I think my current problem with defining 'Void' as a domain in 'SetCategory' is probably an example of such difficulties. Clearly if the definition of some domain is split between being at least partly built-in to the compiler and partly defined in the library, then these definitions must be consistent. >> ... >> 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 consistent if you do not allow anybody to discover > that values are different. But then, why to store them at > all? > Well, I did suggest that such an implementation of 'Void' is a logically consistent alternative to the current abuse of 'None'. I think that is a good reason. >> >> Why do you think 'Void' can not (or should not?) be used for this purpose? >> > > If you allow storing and retrieving values from 'Void' it no longer > will be terminal object (by the same reasoning which currently > applies to 'None') Retrieving values from 'Void' could only be done using 'pretend'. 'pretend' is a marker that something other than the usual operations of the library are required and that there is no inherent guarantee of (static) type-correctness. The need for 'pretend' in this case (and also as it is now currently implemented inconsistently using 'None') is to help deal with run-time types. >> ... >> '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 'None' is currently useful only because it is implemented in an inconsistent manner. >> 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. I disagree. Each operation from a terminal object to some domain X represents an "element" of the domain X. This is not entirely trivial. > The first one may be consistent if None is really initial > object, but then it almost useless. > I do not understand why you think it makes sense to define an operation that by definition requires some input value from a domain that has no values. 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
