|
The ultimate Mathemagix
type system |
|
We plan to improve the current Mathemagix type
system in the next years. The ultimate type system we have in mind
will be based on a few general principles:
-
The declaration of a symbol is seen as a notification of the
ability to carry out a certain task under certain
circumstances. Several solutions may be specified for the same task
under different circumstances (overloading and natural
extensability).
-
Ambiguous expressions systematically carry types and Mathemagix
contains a general mechanism for computations with ambiguous types.
-
As a counterpart to the powerful constructs which are provided by
the type system, the user has some responsability of using it in the
appropriate way. When used inappropriately, some of the type
checking algorithms may not terminate or abort prematurely.
-
The type system should be as “independent” as possible
from the rest of the language.
Concretely speaking, Mathemagix types are formed
from
-
Atomic symbols
-
Examples: String, Int,
etc.
-
Type constructors
-
Example: Polynomial(Int),Int→String,
etc.. Type constructors may also use instances, like in
Array(Int,3).
-
Logical constructors
-
Examples: IntString (overloaded
Int and String), X,X→X
(template type).
Let us explain these ideas in a bit more detail.
Logical supertypes
In classical type systems, each variable x has a type
T (written x:T). In Mathemagix,
one should rather see the fact that “the context provides a
symbol x of type T” (written
x:T) as a statement. Such statements
may be combined in the language of first order logic. Now logical
supertypes are new types which correspond to such combinations. For
instance, the type TU is the type such that for all
symbols x, we have
x:TU⟺x:T∧x:U.
In other words, if x:TU in a given context, then
x may both be used as an object of type T or as
an object of type U, i.e. x has
been overloaded, or the result of an ambiguous expression. The
following logical type constructors are currently implemented in the
type system (although only and are currently
available in the interpreter):
-
x:TU⇔x:T∧x:U
for overloading.
-
x:TU⇔x:T∨x:U
for union-like types.
-
x:a,T(a)⇔∀a,x:T(a)
for template types. For instance, if f:T,T→T, then
for any type T, we may use f as a function
from T to T.
-
x:a,T(a)⇔∃a,x:T(a)
for generic types. For instance, a routine to find the roots of a
polynomial might have the type T,U,Polynomial(T)→List(U).
In the future, we also plan to add conditional types
RT,
with x:RT⇔(R⇒x:T).
The relations R should be defined using first order logic
axioms (and possibly refer to predicate routines). For instance, this
would permit to use types like T,Ring(T)T→T.
Extensibility and exceptions
The advantage of logical supertypes is that it is possible to define
functions which are only valid under very precise circumstances, which
are modelized using first order logic. This makes the system very
extensible and customizable.
Indeed, assume for instance that you have functions f and
g, where g depends on f and where
f is valid under certain circumstances. Then it may be that
someone makes a new implementation of f under another
circumstance. Then it becomes automatically possible to apply
g in this new circumstance.
It may also be that the original implementation of f is
valid under very broad hypothesis, but also very unefficient. Then a
new user may reimplement f under more particular hypothesis
later. Here Mathemagix uses another general
principle: when applying an overloaded function to some type, then the
most particular implementation wins. In other words, if
f:T→()U→() is applied to
x:T, and the typechecker can prove
x:T→x:U, but not
x:U→x:T, then
f:T→() is applied. It should be noticed
that this principle makes it unnecessary to introduce negation in the
logical type system. In fact, negation would be harmful, because it
breaks the extensibility.
Another major advantange of the logical supertype approach is that it
allows for less hierarchic design of big projects. For example,
consider the problem where you have trees with n types of
possible nodes and that you need to define k types of
actions on trees which depend on the nodes, but where many
implementations can be grouped on either node type or action type. In
C++ this can essentially be done in two ways:
either you declare the tree class as a structure with k
virtual functions, which makes it possible to regroup the
implementations by node types, or you declare a simple tree class with
enumeration nodes, and you regroup the implementations by their action
type. In either case, one design style is priviledged: dispatching on
node type or dispatching on action type. In Mathemagix,
it is naturally possible to mix both styles.
Feasability
Of course, it is nice to design a very powerful type system, but it is
also nice if one can implement it. In the most general setting of
first order logic, this is quite hopeless. Nevertheless, only a tiny
part of the first order logic is used in practice, even though it may
be hard to indentify this part. Our approach is to progressively
extend the strength of the implementation of the type system and
accept the fact that it will not do everything. This should make
certain types of uses perfectly reliable, but it will remain up to the
user not to abuse the type system.
In order to make this philosophy fully functional, it is nice to make
the type system as independent as possible from the rest of the
language, so that it might actually be carried out by a dedicated
systeem, like a theorem proving system. In Mathemagix
the implementation of the type system is in the directory src/logic
and you may test it using mmx-convert. Typically the
type system should provide methods for type conversion, typing
function applications and controlling implicit conversions.
At the moment, the type system is able to handle pure predicate logic
(restricted to
and )
well. It can also deal with types of the form
a1,…,ak,b1,…,bl,T(a1,…,ak)→U(a1,…,ak,b1,…,bl)
in a systematic way, and conjunctions of such types. Many easy other
types can also be dealt with, though not systematically. A current
limitation is that when you have a method
f:X,(X,X)→()
and an implicit converter T↝U, then
f can not yet be applied to (T,U).
Semantics
The precise semantics of logical supertypes is still under
development. One has to decide in particular if one wants to restrict
the application of quantifiers to atomic supertypes (i.e. String, Polynomial(Int)
or List(StringInt)
are OK, but not StringInt). Indeed, consider the
function
f:X,(X,X)→()
If one may take X = TU, then, using the convertions
T↝TU and
U↝TU, it becomes possible to applie
f to (T,U) since this is the case for
all T and U, we obtain an implicit converter
X,(X,X)→()↝T,U,(T,U)→() |
(1) |
Here one hits the limitations of the approach of not requiring any
additional information on types, like a category in Aldor.
Indeed, if one writes a routine like
square:X,X→X;x↦x×x
then it is not really necessary to know the type of X,
since it is very likely that the user will only apply it in the case
when there is a multiplication defined on X. However, if
one has multiplications on T and U, then it is
highly unlikely to have a multiplication on TU, so the
implicit conversion (?) is generally abusive.
© 2003 Joris van der Hoeven
Permission is granted to copy, distribute and/or modify this document
under the terms of the
GNU General Public License. If you
don't have this file, write to the Free Software Foundation, Inc., 59
Temple Place - Suite 330, Boston, MA 02111-1307, USA.