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

Edit detail for #112 Returned type of compiled function revision 2 of 3

1 2 3
Editor: kratt6
Time: 2007/12/28 13:16:15 GMT-8
Note:


        

Submitted by : (unknown) at: 2007-11-17T21:53:04-08:00 (15 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)
LatexWiki Image(1)
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
LatexWiki Image(2)
Type: PositiveInteger?
axiom
f(-3)
LatexWiki Image(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
LatexWiki Image(4)
Type: PositiveInteger?
axiom
f(-3)
LatexWiki Image(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
LatexWiki Image(6)
Type: PositiveInteger?
axiom
f(-3)
LatexWiki Image(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 G1471 with type Integer -> Boolean
LatexWiki Image(8)
Type: PositiveInteger?

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

axiom
f 3
LatexWiki Image(9)
Type: PositiveInteger?
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
LatexWiki Image(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.