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 1 of 3

1 2 3
Editor:
Time: 2007/11/17 21:53:04 GMT-8
Note:

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

\begin{axiom}
dom:=(INT->INT)
f:dom
f x == x-1
\end{axiom}

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!

\begin{axiom}
f 3
f(-3)
\end{axiom}

This has nothing to do with the declaration of <code>f</code>.

\begin{axiom}
f(x:INT):INT==x-1
f(3)
f(-3)
\end{axiom}

Not even:

\begin{axiom}
f(x:INT):INT==(x-1)::INT
f(3)
f(-3)
\end{axiom}
Or even:

\begin{axiom}
g(x:INT):NNI == 2^(sign(x)*x)::NNI
g 3
\end{axiom}

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

\begin{axiom}
f 3
f -3
\end{axiom}


Compare the type returned below for <code>g 1</code>, the retraction to <code>PositiveInteger</code> is not done.

\begin{axiom}
g(x:INT): FRAC INT == 1/x
g 1
\end{axiom}

The difference may perhaps be due to the fact that the data structure of <code>FRAC INT</code> is very different from <code>INT</code>, whereas the data structure of <code>INT</code> is identical to that of <code>PI</code>. So the explanation that the reason <code>1/1</code> is not retracted because <code>retract</code> is not always possible is not the full story.

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.

begin{axiom} dom:=(INT->INT) f:dom f x == x-1 end{axiom}

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!

begin{axiom} f 3 f(-3) end{axiom}

This has nothing to do with the declaration of <code>f</code>.

begin{axiom} f(x:INT):INT==x-1 f(3) f(-3) end{axiom}

Not even:

begin{axiom} f(x:INT):INT==(x-1)::INT f(3) f(-3) end{axiom} Or even:

begin{axiom} g(x:INT):NNI == 2^(sign(x)*x)::NNI g 3 end{axiom}

The following deliberate "error" shows the Interpreter always assumes <code>3</code> is of type <code>PositiveInteger?</code>.

begin{axiom} f 3 f -3 end{axiom}

Compare the type returned below for <code>g 1</code>, the retraction to <code>PositiveInteger?</code> is not done.

begin{axiom} g(x:INT): FRAC INT == 1/x g 1 end{axiom}

The difference may perhaps be due to the fact that the data structure of <code>FRAC INT</code> is very different from <code>INT</code>, whereas the data structure of <code>INT</code> is identical to that of <code>PI</code>. So the explanation that the reason <code>1/1</code> is not retracted because <code>retract</code> is not always possible is not the full story.