Bill Page <bill.p...@newsynthesis.org> writes: | > Bill Page <bill.p...@newsynthesis.org> writes: | > | > | On Thu, Dec 3, 2009 at 9:12 PM, Waldek Hebisch wrote: | > | > I just commited a patch which replaces uses of 'Domain' in interpreter | > | > by 'Type'. Similarely, it replaces uses of 'Subdomain(Domain)' | > | > by 'Category'. This makes interpreter and compiler more consistent. | > | > Additionally this patch allows limited (should be comparable to | > | > what OpenAxiom allows) use of type valued functions in interpeter. | > | > | > | | > | I rather strongly dislike this change. It seems to me that the | > | interpreter (almost) got it right and the older notions built in to | > | Spad were not. Consistency is a good thing but I would have much | > | preferred that Type be replaced with Domain and Category (as a type) | > | be replaced with Subdomain(Domain) - since that is what a category is | > | according to the original published intentions of the Axiom designers. | > | For what its worth, I also think OpenAxiom did the wrong thing here | > | (at least in part), although OpenAxiom does at least define Domain as | > | a Domain in the the library. | > | | On Fri, Dec 4, 2009 at 11:30 AM, Gabriel Dos Reis wrote: | > | > I'm unconvinced that there is a Single One True Answer here. The design | > space is huge -- to have a glimpse, have a look at the lambda cube. | | E.g. | | http://en.wikipedia.org/wiki/Lambda_cube | | and references therein. Perhaps you can suggest others?
well, the definitive guide is the book by Barendregt, and it is referenced there; also you might want to complement with Pure Type Systems (elaboration of Barendregt's ideas). | > Consequently, I would encourage people to explore other choices, and in | > case they find a choice to be wrong, I encourage them -- for the benefits | > of scientific discourse -- to provide logical arguments as to why. | > 'original published intentions' does not make it. | > | | In general I agree that citing original design documents for Axiom | does not constitute a logical argument. Nonetheless I do think that | the view of categories as subdomains of the domain of all domains as | exposed by Stephen Watt is logically consistent Please note that my encouraging people to explore other models (as opposed to presenting one particular as The Truth) is not based on the fact that the notion of 'subdomains' is logically inconsistent -- for I have never seen a formal presentation of the idea along with soundness proof, one way of the other. Again, I'm encouraging people from scientific curiosity point of view. | and could be implemented consistently by some future version of Axiom. consistent implementation would probably need a sound formal model... | Such subtyping however | | http://en.wikipedia.org/wiki/Subtyping | | is not usually included in the usual "lambda cube". but, it is relatively well understood, compared to other type systems such as those that generalize the lambda cube and opens up possibilities for different forms of mechanization of constructive or computational mathematics. | So the design space that I would like to consider is even larger. as I said, the design space is very large, and the lambda cube is only a *glimpse*. A nice thing about the lambda cube is that it clearly formalizes some parameters of the design space and gives a nice picture of what a given design choice leads to. http://www.rbjones.com/rbjpub/logic/cl/tlc001.htm However, it is far from being the definitive answer. But, it does suggest a minimum: a formalization of the dependencies. -- Gaby ------------------------------------------------------------------------------ Join us December 9, 2009 for the Red Hat Virtual Experience, a free event focused on virtualization and cloud computing. Attend in-depth sessions from your desk. Your couch. Anywhere. http://p.sf.net/sfu/redhat-sfdev2dev _______________________________________________ open-axiom-devel mailing list open-axiom-devel@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/open-axiom-devel
