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

a₁,…,a_k,b₁,…,b_l,T(a₁,…,a_k)→U(a₁,…,a_k,b₁,…,b_l)

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.