Edit detail for FriCAS language revision 1 of 4

Axiom has the [Axiom interpreter]? for interaction with the user and the [Axiom compiler]? for building library modules.

Axiom Types

Types are one of the most important concepts in Axiom.

Like Modula 2, PASCAL, FORTRAN, and Ada, the programming language emphasizes strict type-checking. Unlike these languages, types in Axiom are dynamic objects: they are created at run-time in response to user commands.

The Axiom interactive language is oriented towards ease-of-use. The [Axiom interpreter]? uses type-inferencing to deduce the type of an object from user input. Type declarations can generally be omitted for common types in the interactive language.

The [Axiom compiler]? language (version 1 of the language is called SPAD, version 2 of the language is called [Aldor]?) on the other hand is based on strong static types that must be explicitly specified by the programmer.

Type Inference in the Axiom Interpreter

Consider

(1+2)/3

(1)

It is sort of interesting, isn't it, that Axiom insists on calling "1" a fraction just because of the way it was calculated? There is a way to say that you want the answer as an integer. Of course this isn't always possible:

(1/3)::Integer

   Cannot convert from type Fraction(Integer) to Integer for value
   1
   -
   3

But for this example it is:

((1+2)/3)::Integer

(2)

Axiom is very strict with types (meaning: that it must be completely unambiguous where each operation takes place). The division of 1+2 by 3 takes place in Fraction Integer (field of rational numbers) and that is where the answer will be, even if it is 1. Most people would automatically "retract" this to the integer 1. But in general, there is no natural way to do so (why not retract 1 to a natural number, for example?). So Axiom provides the user a way to "coerce" an answer to another type. You can coerce 1 to any of many, many types, for example, as a polynomial, or even as a matrix (or the unit element of any ring).

((1+2)/3)::Polynomial Integer

(3)

((1+2)/3)::SquareMatrix(1,Integer)

(4)

((1+2)/3)::SquareMatrix(3,Integer)

(5)

((1+2)/3)::SquareMatrix(3, Polynomial Complex Integer)

(6)

Types of Objects, Domains, and Categories

In Axiom the concept of "Type" is universally applied at all levels.

From the Axiom Book: Appendix B Glossary

• The type of any category is the unique symbol Category.
• The type of a domain is any category to which the domain belongs.
• The type of any other object is either the (unique) domain to which the object belongs or a subdomain of that domain.
• The type of objects is in general not unique.

From the Axiom Book: Technical Introduction

Every Axiom object is an instance of some domain. That domain is also called the type of the object. Thus the typeOf -1 is inferred by the interpret to be Integer and the typeOf the variable x:Integer is declared to be Integer. Similarly the typeOf "daniel" is String. The type of an object, however, is not unique. The type of integer 7 is not only Integer but also NonNegativeInteger, PositiveInteger, and possibly, in general, any other subdomain of the domain Integer.

Domains are defined by Axiom by programs of the form:

  Name(Parameters): JoinCategorys
    with Exports == Extends
      add Rep == RepDomain
        Implementation 

The Name of each domain is used to refer to the collection of its instances. For example, Integer denotes "the integers", Float denotes "the floating point numbers" etc. For example:

  Fraction(S: IntegralDomain): QuotientFieldCategory S with
       if S has canonical and S has GcdDomain
         and S has canonicalUnitNormal
           then canonical
    == LocalAlgebra(S, S, S) add
      Rep:= Record(num:S, den:S)
      coerce(d:S):% == [d,1]
      zero?(x:%) == zero? x.num

Thus the type of Fraction Integer is QuotientFieldCategory Integer with canonical. The axiom canonical means that equal elements of the domain are in fact identical.

We also say that the domain Fraction(S) extends the domain LocalAlgebera(S,S,S). Domains can extend each other in a circular mutually recursive manner so in general the extended relationship forms a directed graph with cycles.

Fractions are represented as the domain Record(num:S, den:S).

In Axiom domains and subdomains are themselves objects that have types. The type of a domain or subdomain is called a category. Categories are described by programs of the form:

   Name(...): Category == JoinCategorys
     with Exports
      add Imports
        Implementation 

The type of every category is the distinguished symbol Category. The category Name is used to denote the collection of domains of that type. For example, category Ring denotes the class of all rings.

For example:

  QuotientFieldCategory(S: IntegralDomain): Category ==
    Join(Field, Algebra S, RetractableTo S, FullyEvalableOver S,
         DifferentialExtension S, FullyLinearlyExplicitRingOver S,
           Patternable S, FullyPatternMatchable S) with
      _/     : (S, S) -> %
         ++ d1 / d2 returns the fraction d1 divided by d2.
      numer  : % -> S
         ++ numer(x) returns the numerator of the fraction x.
      denom  : % -> S
      ...
      if S has PolynomialFactorizationExplicit then
        PolynomialFactorizationExplicit
   add
      import MatrixCommonDenominator(S, %)
      numerator(x) == numer(x)::%
      denominator(x) == denom(x) ::%
      ...

Categories say nothing about representation. Domains, which are instances of category types, specify representations. See also [Rep And Per]?.

Categories form hierarchies (technically, directed-acyclic graphs). A simplified hierarchical world of algebraic categories is shown below. At the top of this world is SetCategory, the class of algebraic sets. The notions of parents, ancestors, and descendants is clear. Thus ordered sets (domains of category OrderedSet) and rings are also algebraic sets. Likewise, fields and integral domains are rings and algebraic sets. However fields and integral domains are not ordered sets:

  SetCategory +---- Ring ---- IntegralDomain ---- Field
              |
              +----  Finite    ---+
              |                    \
              +---- OrderedSet -----+ OrderedFinite

  Figure 1. A simplified category hierarchy.

Confusion of Type and Domain

The most basic category is Type. It denotes the collection of all domains and subdomains. Note carefully that Type does not denote the class of all types! The type of all categories is Category. The type of Type itself is undefined. For example: the domain List is able to build "lists of elements from domain D" for arbitrary D simply by requiring that D belong to category Type.

Another example. Enter the type Polynomial (Integer) as an expression to Axiom. This looks much like a function call as well. It is! The result is stated to be of type Domain, which denotes the collection of all domains.

Polynomial(Integer)

(7)

But note well that Domain is a domain but Type is a category. !!!?

Ref: Axoim Book "Chapter 2 Using Types and Modes".

Overloading and Dependent Types

Many Axiom operations have the same name but different types and these types can be dependent on other types. For example

)display operation differentiate

There are 15 exposed functions called differentiate :
   [1] (D,(D3 -> D3),NonNegativeInteger) -> D from D
            if D has DIFEXT(D3) and D3 has RING
   [2] (D,(D2 -> D2)) -> D from D if D has DIFEXT(D2) and D2 has RING

   [3] (D,NonNegativeInteger) -> D from D if D has DIFRING
   [4] D -> D from D if D has DIFRING
   [5] (D,NonNegativeInteger) -> D from D
            if D has DVARCAT(D2) and D2 has ORDSET
   [6] D -> D from D if D has DVARCAT(D1) and D1 has ORDSET
   [7] (D,(D3 -> D3)) -> D from D
            if D has FFCAT(D2,D3,D4) and D2 has UFD and D3 has UPOLYC(
            D2) and D4 has UPOLYC(FRAC(D3))
   [8] (FullPartialFractionExpansion(D2,D3),NonNegativeInteger) -> 
            FullPartialFractionExpansion(D2,D3)
            from FullPartialFractionExpansion(D2,D3)
            if D2 has Join(Field,CharacteristicZero) and D3 has UPOLYC(
            D2)
   [9] FullPartialFractionExpansion(D1,D2) -> 
            FullPartialFractionExpansion(D1,D2)
            from FullPartialFractionExpansion(D1,D2)
            if D1 has Join(Field,CharacteristicZero) and D2 has UPOLYC(
            D1)
   [10] (GeneralUnivariatePowerSeries(D2,D3,D4),Variable(D3)) -> 
            GeneralUnivariatePowerSeries(D2,D3,D4)
            from GeneralUnivariatePowerSeries(D2,D3,D4)
            if D3: SYMBOL and D2 has RING and D4: D2
   [11] (D,List(D3),List(NonNegativeInteger)) -> D from D
            if D has PDRING(D3) and D3 has SETCAT
   [12] (D,D1,NonNegativeInteger) -> D from D
            if D has PDRING(D1) and D1 has SETCAT
   [13] (D,List(D2)) -> D from D if D has PDRING(D2) and D2 has SETCAT

   [14] (D,D1) -> D from D if D has PDRING(D1) and D1 has SETCAT
   [15] (D,(D2 -> D2),D) -> D from D if D has UPOLYC(D2) and D2 has 
            RING

There are 14 unexposed functions called differentiate :
   [1] (IntegrationResult(D1),Symbol) -> D1 from IntegrationResult(D1)
            if D1 has FIELD and D1 has PDRING(SYMBOL)
   [2] (IntegrationResult(D1),(D1 -> D1)) -> D1 from IntegrationResult(
            D1)
            if D1 has FIELD
   [3] (D,PositiveInteger) -> Union(D,0) from D if D has JBC
   [4] (D,D1) -> D from D if D has JBFC(D1) and D1 has JBC
   [5] (OutputForm,NonNegativeInteger) -> OutputForm from OutputForm

   [6] (U32Vector,Integer) -> U32Vector from 
            U32VectorPolynomialOperations
   [7] (U32Vector,NonNegativeInteger,Integer) -> U32Vector
            from U32VectorPolynomialOperations
   [8] (SparseUnivariateLaurentSeries(D2,D3,D4),Variable(D3)) -> 
            SparseUnivariateLaurentSeries(D2,D3,D4)
            from SparseUnivariateLaurentSeries(D2,D3,D4)
            if D3: SYMBOL and D2 has RING and D4: D2
   [9] (SparseUnivariatePuiseuxSeries(D2,D3,D4),Variable(D3)) -> 
            SparseUnivariatePuiseuxSeries(D2,D3,D4)
            from SparseUnivariatePuiseuxSeries(D2,D3,D4)
            if D3: SYMBOL and D2 has RING and D4: D2
   [10] (SparseUnivariateTaylorSeries(D2,D3,D4),Variable(D3)) -> 
            SparseUnivariateTaylorSeries(D2,D3,D4)
            from SparseUnivariateTaylorSeries(D2,D3,D4)
            if D3: SYMBOL and D2 has RING and D4: D2
   [11] (UnivariateFormalPowerSeries(D2),Variable(QUOTE(x))) -> 
            UnivariateFormalPowerSeries(D2)
            from UnivariateFormalPowerSeries(D2) if D2 has RING
   [12] (UnivariateLaurentSeries(D2,D3,D4),Variable(D3)) -> 
            UnivariateLaurentSeries(D2,D3,D4)
            from UnivariateLaurentSeries(D2,D3,D4)
            if D3: SYMBOL and D2 has RING and D4: D2
   [13] (UnivariatePuiseuxSeries(D2,D3,D4),Variable(D3)) -> 
            UnivariatePuiseuxSeries(D2,D3,D4)
            from UnivariatePuiseuxSeries(D2,D3,D4)
            if D3: SYMBOL and D2 has RING and D4: D2
   [14] (UnivariateTaylorSeries(D2,D3,D4),Variable(D3)) -> 
            UnivariateTaylorSeries(D2,D3,D4)
            from UnivariateTaylorSeries(D2,D3,D4)
            if D3: SYMBOL and D2 has RING and D4: D2

We can see how the interpreter resolves the type:

  [14] (D,D1) -> D from D if D has PDRING D1 and D1 has SETCAT

in the following example

)set message bottomup on

differentiate(sin(x),x)

 Function Selection for sin
      Arguments: VARIABLE(x) 
   -> no appropriate sin found in Variable(x) 
   -> no appropriate sin found in Symbol 
   -> no appropriate sin found in Variable(x) 
   -> no appropriate sin found in Symbol 

 Modemaps from Associated Packages 
   no modemaps

 Remaining General Modemaps 
   [1] D -> D from D if D has TRIGCAT

 [1]  signature:   EXPR(INT) -> EXPR(INT)
      implemented: slot $$ from EXPR(INT)

 Function Selection for differentiate
      Arguments: (EXPR(INT),VARIABLE(x)) 
   -> no appropriate differentiate found in Variable(x) 

 [1]  signature:   (EXPR(INT),SYMBOL) -> EXPR(INT)
      implemented: slot $$(Symbol) from EXPR(INT)

(8)

Notice that

EXPR INT has PDRING SYMBOL

(9)

SYMBOL has SETCAT

(10)

In light of the above definitions of Type in Axiom, it would seem that the type of

I:=Integer

(11)

which Axiom prints as Domain is actually a Category. That certainly is confusing terminology... I guess we just have to remember that whenever we see Type: Domain what Axiom really means is Type: SomeCategory(...).

Issue report #209 however shows that perhaps it would be useful to flatten Axiom's two-level object model of categories and domains by embedding Categories into the domain called Domain. This would allow convenient things like evaluating the expression:

  (Integer,Float)

as type Tuple(Domain).

As #209 reports, Axiom internally generates a call to the function |Domain| and then fails with an undefined. That seems peculiarly broken to me and I wonder if the last commercial version of Axiom has this same behaviour or was something lost in the porting to the open source gcl-based version? I thorough search of the current Axiom sources did not turn up any function, package or domain named Domain.

There are numerous places in the Axiom BOOT code that seems to treat this name in a special manner as if it might be "built-in". Eg. :

  interp/bootfuns.lisp.pamphlet:(def-boot-val |$Domain| '(|Domain|)        
  interp/br-con.boot.pamphlet:    is [[h,:.],:t] and MEMBER(h,'(Domain SubDomain))
  interp/clammed.boot.pamphlet:  form in '((Mode) (Domain) (SubDomain (Domain))) = 
  interp/g-cndata.boot.pamphlet:      domain in '((Mode) (Domain) (SubDomain (Doma
  interp/i-analy.boot.pamphlet:  if ( oo = "%" ) or ( oo = "Domain" ) or ( domainF
  interp/i-coerce.boot.pamphlet:    t1 in '((Mode)  (Domain) (SubDomain (Domain))) =>
  interp/i-funsel.boot.pamphlet:  MEMBER('(SubDomain (Domain)),types1) => NIL
  interp/i-output.boot.pamphlet:  categoryForm? domain or domain in '((Mode) (Domain) (SubDomain (Domain))) =>
  interp/i-spec1.boot.pamphlet:  saeTypeSynonymValue := objNew(sae,'(Domain))
  interp/i-spec1.boot.pamphlet:  objMode triple = '(Domain) => triple
  interp/i-spec1.boot.pamphlet:      objMode(val) in '((Domain) (SubDomain (Domain))) =>
  interp/i-spec2.boot.pamphlet:    else if categoryForm?(type) then '(SubDomain (Domain))
  interp/i-spec2.boot.pamphlet:  type in '((Mode) (Domain)) => '(SubDomain (Domain))
  interp/parse.boot.pamphlet:        and m in '((Mode) (Domain) (SubDomain (Domain))) => D
  interp/setq.lisp.pamphlet:  CAPSULE |Union| |Record| |SubDomain| |Mapping| |Enumeration| |Domain| |Mode|))
  interp/setq.lisp.pamphlet:(SETQ |$Domain| '(|Domain|))
  interp/sys-pkg.lisp.pamphlet:    BOOT::YIELD BOOT::|Polynomial| BOOT::|$Domain| BOOT::STRINGPAD
  interp/trace.boot.pamphlet:      (objMode value in '((Mode) (Domain) (SubDomain (Domain)))) =>

However in searching for use and meaning of the domain Domain, in all the Axiom algebra library I can find only one place that explicity uses this domain.

In algebra/forttyp.spad.pamphlet in the domain TheSymbolTable it reads:

    Entry : Domain  := Record(symtab:SymbolTable, _
                              returnType:FSTU, _
                              argList:List Symbol)

For details see [SandBox Domains And Types]?.

So apparently at least in 1992, such a domain might have existed in Axiom.

Oddly (or perhaps as we might expect :) compiling this code in the current version of Axiom produces some error messages:

   Semantic Errors: 
      [1]  Domain is not a known type
      [2]  void is not a known type

yet the compile does apparently successfully complete. But does it work?