Introduction to the |
Why develop or learn yet another programming language? At the start of
the
There were no high quality general purpose free computer algebra systems.
With the notable exception of
In the beginning, the
In its present state,
The requirement that programs be strongly typed has its pros and cons.
On the one hand, it puts some burden on the user, since the user must
carefully specify the type of every newly introduced symbol. For
instance, evaluation of the expression
On the other hand, specifying clean types for all newly introduced
notations makes the semantics of the language far more robust and
simplifies the task of writing compilers for the language which
transform the source code into highly efficient executables. For
instance, what do we actually mean by an expression such as ?
Is the multiplication necessary commutative, or not? Clean typing of
all declarations is a way to make potential implicit assumptions of
this kind more explicit. The increased robustness in the semantics
makes it also easier to develop large mathematical libraries.
Furthermore, whereas the memory layout of data can only be determined
at run time for untyped languages, this kind of information and other
assumptions on data are available at compile time in strongly typed
languages. This opens the route to all kinds of optimizations which
usually make strongly typed languages one order of magnitude faster
than their untyped homologues. This is particularly important in the
case of
Why did we not chose for an existing strongly typed language with an
optimizing compiler? There are a certain number of more traditional
languages which we have considered. First of all, there are the
languages
In section 2 of our paper “Overview of the acts on numbers,
polynomials, matrices, etc.
Conceptually speaking, we also believe that the prototype of a
function declaration is analogous to a mathematical definition or the
statement of a mathematical theorem, whereas the the implementation of
the function is analogous to giving a proof. The type system of
|
This declaration clearly corresponds to a mathematical definition:
,
and an element
, we define the cube of
by
.
Notice that this is far more precise than simply declaring
|
corresponds to the mathematical theorem that for any real closed field
and any polynomial
, we
may compute the vector of all complex roots of
.
Although this declaration is precise enough from the operational point
of view, we may actually refine the prototype as follows:
|
This refinement would correspond to the mathematical statement that
is algebraically closed (and that we may
actually compute the roots of polynomials). However,