On Wed, May 28, 2008 at 8:29 PM, Bill Page <[EMAIL PROTECTED]> wrote: > Gaby, e. al. > > Although the type system of OpenAxiom has some improvements over Axiom > and FriCAS, I still find some of the fundamentals confusing (or > confused :-) > > I would be very interested in your opinions on the following claims > and questions. Which of these are true "by definition" and which might > represent conceptual problems or bugs? What fundamental type > constructions am I missing? > > 1) Categories and domains are types. All types satisfy the category > 'Type' , i.e. > > x has Type > > is true for any domain X or category X, including: > > Type has Type
true by definition. Note: this includes packages too. > > 2) Domains satisfy categories only by assertion, e.g. > > Integer():Join(IntegerNumberSystem, ...) > --------- > Integer has IntegerNumberSystem > true by definition. > 3) It is possible to construct domains that contain types > > x:List Type := [SetCategory,BasicType] True in OpenAxiom. You'll see buggy output for List Type, but not for List Category or List Domain. Fixing that requires clarifying along the lines of questions you are asking plus proper handling of types. This can be confusing in a system where we are trying hard to confuse everything :-) > > 4) 'Void' is a domain that satisfies no categories except 'Type' > > Void has Type I would *think* that this is true by definition. > > 5) Objects /1 are members of 'Domains' > > 1$Integer true by definition. Domains are the types that provide representation for object, and an object can belong to exactly one domain. In some object oriented languages, this would correspond to the notion of `dynamic type'. > > 6) In the interpreter the type (domain) of variables can be declared > > x:Integer true by definition. > > 7) Categories can be passed as arguments > > f(x:Type):Integer == 1 > f(SetCategory) OpenAxiom wants to do this -- and I think there already is basic support for that. > > 8) But at the present time the type of a variable cannot be a category > > x:Type := SetCategory This is a restriction of the original axiom system. I would like to remove it. That however poses some interesting problems for compilation. If we do only interpretation then I do not foresee any difficult problem. However, when we do compilation, it becomes tricky because we don't have types that oversees categories so we basically don't know how to typecheck them for compilation purposes, especially if they are used to describe domains. > > 9) Is 'Category' the domain of all categories Category is the category of all domains and packages. There are things that do not belong to Category. An example is Mode. Note that, although )show Category would report that it is a domain constructor, from the abstract semantics point of view, it is not a domain. > > )show Category > x:Category := Categoy > f(x:Category):Integer == 1 > f(Integer) > > 10) or is 'Category' a category? > > Category has Category > f(x:Category):Integer == 1 > f(SetCategory) > x:List Category := [SetCategory,BasicType] this is well formed in OpenAxiom. > > 11) 'Domain' is the domain of all domains. > > x:Domain := Domain This is correct. > > 12) The existence of the domain 'Domain' makes is possible for > functions in the interpreter to return domain-values > > MyType(x:Integer):Domain == (x>0 => Float; Integer) > i:MyType(0) this is correct. > > 13) And to construct domains whose members are domains > > x:List Domain := [Integer,Float] this is correct. > > Ref: > ----- > > 1) Axiom Book > > 2) Aldor User's Guide > > 3) The file 'algebra/coerce.spad.pamphlet' contains the following definitions: > > )abbrev category TYPE Type > ++ The new fundamental Type (keeping Object for 1.5 as well) > ++ Author: Richard Jenks > ++ Date Created: 14 May 1992 > ++ Date Last Updated: 14 May 1992 > ++ Description: The fundamental Type; > Type(): Category == with nil > > 4) The file 'algebra/domain.spad.pamphlet' contains these definitions: > > )abbrev domain CATEGORY Category > ++ Author: Gabriel Dos Reis > ++ Date Create: February 16, 2008. > ++ Date Last Updated: February 16, 2008. > ++ Basic Operations: coerce > ... > > )abbrev domain DOMAIN Domain > ++ Author: Gabriel Dos Reis > ++ Date Create: October 18, 2007. > ++ Date Last Updated: January 19, 2008. > ++ Basic Operations: coerce, reify > ... > > --------- > > 1/ In a couple of places in the documentation reference is made to an > 'Object' type as well, but no definition of this type seems to remain > in the source. In some version of the system (a long time ago), there was a category called Object. It never existed in the open source version. -- Gaby ------------------------------------------------------------------------- This SF.net email is sponsored by: Microsoft Defy all challenges. Microsoft(R) Visual Studio 2008. http://clk.atdmt.com/MRT/go/vse0120000070mrt/direct/01/ _______________________________________________ open-axiom-devel mailing list open-axiom-devel@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/open-axiom-devel
