login  home  contents  what's new  discussion  bug reports     help  links  subscribe  changes  refresh  edit

Submitted by : (unknown) at: 2007-11-17T21:53:04-08:00 (16 years ago)
Name :
Axiom Version :
Category : Severity : Status :
Optional subject :  
Optional comment :

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

axiom
dom:=(INT->INT)

\label{eq1}\mbox{\rm (\hbox{\axiomType{Integer}\ } - > \hbox{\axiomType{Integer}\ })}(1)
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

\label{eq2}2(2)
Type: PositiveInteger?
axiom
f(-3)

\label{eq3}- 4(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

\label{eq4}2(4)
Type: PositiveInteger?
axiom
f(-3)

\label{eq5}- 4(5)
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

\label{eq6}2(6)
Type: PositiveInteger?
axiom
f(-3)

\label{eq7}- 4(7)
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 G695 with type Integer -> Boolean

\label{eq8}8(8)
Type: PositiveInteger?

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

axiom
f 3

\label{eq9}2(9)
Type: PositiveInteger?
axiom
f -3
There are 8 exposed and 4 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)

\label{eq10}1(10)
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.

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.




  Subject:   Be Bold !!
  ( 14 subscribers )  
Please rate this page: