This following shows that functions in Axiom have types and a domain for functions may be associated with an identifier.

(1) -> dom:=(INT->INT)

(1)

f:dom

f x == x-1

However, when the function is compiled, the returned type displayed may not agree with its declared type or even its apparent compiled type and depends on the input!

f 3

Compiling function f with type Integer -> Integer

(2)

f(-3)

(3)

This has nothing to do with the declaration of f.

f(x:INT):INT==x-1

   Function declaration f : Integer -> Integer has been added to 
      workspace.
   Compiled code for f has been cleared.
   1 old definition(s) deleted for function or rule f

f(3)

Compiling function f with type Integer -> Integer

(4)

f(-3)

(5)

Not even:

f(x:INT):INT==(x-1)::INT

   Function declaration f : Integer -> Integer has been added to 
      workspace.
   Compiled code for f has been cleared.
   1 old definition(s) deleted for function or rule f

f(3)

Compiling function f with type Integer -> Integer

(6)

f(-3)

(7)

Or even:

g(x:INT):NNI == 2^(sign(x)*x)::NNI

   Function declaration g : Integer -> NonNegativeInteger has been 
      added to workspace.

g 3

Compiling function g with type Integer -> NonNegativeInteger

Compiling function G0 with type Integer -> Boolean

(8)

The following deliberate "error" shows the Interpreter always assumes 3 is of type PositiveInteger.

f 3

(9)

f -3

   There are 9 exposed and 6 unexposed library operations named - 
      having 2 argument(s) but none was determined to be applicable. 
      Use HyperDoc Browse, or issue
                                )display op -
      to learn more about the available operations. Perhaps 
      package-calling the operation or using coercions on the arguments
      will allow you to apply the operation.

   Cannot find a definition or applicable library operation named - 
      with argument type(s) 
                              FunctionCalled(f)
                               PositiveInteger

      Perhaps you should use "@" to indicate the required return type, 
      or "$" to specify which version of the function you need.

Compare the type returned below for g 1, the retraction to PositiveInteger is not done.

g(x:INT): FRAC INT == 1/x

   Function declaration g : Integer -> Fraction(Integer) has been added
      to workspace.
   Compiled code for g has been cleared.
   1 old definition(s) deleted for function or rule g

g 1

Compiling function g with type Integer -> Fraction(Integer)

(10)

The difference may perhaps be due to the fact that the data structure of FRAC INT is very different from INT, whereas the data structure of INT is identical to that of PI. So the explanation that the reason 1/1 is not retracted because retract is not always possible is not the full story.

The report is confused. There is a distinction between function's declared type (which does not change), and the type inferred by the interpreter for the value computed by a function. These are two separate processes.