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 x*y in a shell
session will not work directly, since we first have to specify the
types of x and y. Also, there may be
some loss of flexibility. For instance, in more classical computer
algebra systems, it is easy to construct vectors with entries of
different types, such as [ 2, "hello", x+y
]. In
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 x*y? Is this just a symbolic expression or rather an element of the polynomial ring ? 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
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
forall (R: Ring) cube (x: R): R == x*x*x; |
This declaration clearly corresponds to a mathematical definition:
Notice that this is far more precise than simply declaring cube(x) == x*x*x. Similarly, the declaration of the function
forall (R: Real_Closed_Field) complex_roots (p: Polynomial R): Vector Complex R == { … } |
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:
forall (R: Real_Closed_Field) complex_roots (p: Polynomial R): (v: Vector Complex R | #v = deg p) == { … } |
This refinement would correspond to the mathematical statement that
is algebraically closed (and that we may
actually compute the roots of polynomials). However,