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: Typeaxiom f:dom Type: Voidaxiom f x == x-1 Type: VoidHowever, 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: PositiveIntegeraxiom f(-3)
Type: IntegerThis has nothing to do with the declaration of axiom f(x:INT):INT==x-1 Type: Voidaxiom f(3) axiom Compiling function f with type Integer -> Integer
Type: PositiveIntegeraxiom f(-3)
Type: IntegerNot even: axiom f(x:INT):INT==(x-1)::INT Type: Voidaxiom f(3) axiom Compiling function f with type Integer -> Integer
Type: PositiveIntegeraxiom f(-3)
Type: IntegerOr even: axiom g(x:INT):NNI == 2^(sign(x)*x)::NNI Type: Voidaxiom g 3 axiom Compiling function g with type Integer -> NonNegativeInteger axiom Compiling function G695 with type Integer -> Boolean
Type: PositiveIntegerThe following deliberate "error" shows the Interpreter always assumes axiom f 3
Type: PositiveIntegeraxiom f -3 Compare the type returned below for axiom g(x:INT): FRAC INT == 1/x Type: Voidaxiom 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 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. |

Invalid--gdr, Tue, 25 Nov 2008 08:53:43 -0800 reply