This following shows that functions in Axiom have types and a domain for functions may be associated with an identifier.
axiom
dom:=(INT->INT)
Type: Domain
axiom
f:dom
Type: Void
axiom
f x == x-1
Type: Void
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!
axiom
f 3
axiom
Compiling function f with type Integer -> Integer
axiom
f(-3)
Type: Integer
This has nothing to do with the declaration of f
.
axiom
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
Type: Void
axiom
f(3)
axiom
Compiling function f with type Integer -> Integer
axiom
f(-3)
Type: Integer
Not even:
axiom
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
Type: Void
axiom
f(3)
axiom
Compiling function f with type Integer -> Integer
axiom
f(-3)
Type: Integer
Or even:
axiom
g(x:INT):NNI == 2^(sign(x)*x)::NNI
Function declaration g : Integer -> NonNegativeInteger has been
added to workspace.
Type: Void
axiom
g 3
axiom
Compiling function g with type Integer -> NonNegativeInteger
axiom
Compiling function G1471 with type Integer -> Boolean
The following deliberate "error" shows the Interpreter always assumes 3
is of type PositiveInteger
.
axiom
f 3
axiom
f -3
There are 8 exposed and 3 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.
axiom
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
Type: Void
axiom
g 1
axiom
Compiling function g with type Integer -> Fraction Integer
Type: Fraction Integer
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.