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: Type
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
Type: PositiveInteger?
axiom f(-3)
Type: Integer
This has nothing to do with the declaration of axiom f(x:INT):INT==x-1 Type: Void
axiom f(3) axiom Compiling function f with type Integer -> Integer
Type: PositiveInteger?
axiom f(-3)
Type: Integer
Not even: axiom f(x:INT):INT==(x-1)::INT Type: Void
axiom f(3) axiom Compiling function f with type Integer -> Integer
Type: PositiveInteger?
axiom f(-3)
Type: Integer
Or even: axiom g(x:INT):NNI == 2^(sign(x)*x)::NNI Type: Void
axiom g 3 axiom Compiling function g with type Integer -> NonNegativeInteger axiom Compiling function G695 with type Integer -> Boolean
Type: PositiveInteger?
The following deliberate "error" shows the Interpreter always assumes axiom f 3
Type: PositiveInteger?
axiom f -3 Compare the type returned below for axiom g(x:INT): FRAC INT == 1/x 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 Invalid --gdr, Tue, 25 Nov 2008 08:53:43 -0800 reply Status: open => rejected
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. |