[open-axiom-devel] OpenAxiom semantics

[Bill P. <bil...@ne...>]

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

2) Domains satisfy categories only by assertion, e.g.

      Integer():Join(IntegerNumberSystem, ...)
      ---------
      Integer has IntegerNumberSystem

3) It is possible to construct domains that contain types

      x:List Type := [SetCategory,BasicType]

4) 'Void' is a domain that satisfies no categories except 'Type'

      Void has Type

5) Objects /1 are members of 'Domains'

      1$Integer

6) In the interpreter the type (domain) of variables can be declared

      x:Integer

7) Categories can be passed as arguments

      f(x:Type):Integer == 1
      f(SetCategory)

8) But at the present time the type of a variable cannot be a category

      x:Type := SetCategory

9) Is 'Category' the domain of all categories

      )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]

11) 'Domain' is the domain of all domains.

      x:Domain := Domain

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)

 13) And to construct domains whose members are domains

      x:List Domain := [Integer,Float]

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.

Regards,
Bill Page.