Formalization of the Mathemagix language

Let us start with formalizing the part of the Mathemagix language which is relevant to the type system. We start by fixing a set of constant symbols. Expanding by the constant symbols , and the function symbols , , and , we obtain the set of terms . More precisely, is the smallest set which contains and such that:

Remark 1. The symbols “” and will be assumed to be binary operators with neutral elements and . For instance and . Using the operators “,” and , we can thus form -ary tuples. In combination with the primitive for function application, we can thus form -ary function applications, even though only contains constant symbols.

Remark 2. The notation will be used for the tuple type, which is recursively defined by .

Expanding with the binary relation and the usual logical connectors and quantifiers, we obtain the set of formulas. More precisely, is the smallest set such that

In the case of the expressions and we will always assume that , whenever or is a subexpression of . We will also use and as abbreviations for and .

Remark 3. The formula should be read “ admits an interpretation of type ”. Indeed, Mathemagix allows for ambiguous expressions: if is an overloaded function, then we may for instance both have and . Similarly, in presence of an automatic converter , the relation will automatically imply .

The formal theory for Mathemagix

The formal theory for the Mathemagix language described in the previous section starts with the following type conditions for tuples and functions:

We recall our conventions concerning “,” and , which can be restated as axioms:

It will convenient to define the relation by

Then product, tuple and function types are required to satisfy the following conversion axioms:

We will denote by the above formal theory for Mathemagix. Given a set with incarnations of the functions and relations of the Mathemagix language, we will write if is a model for .

From the typing point of view, an environment corresponds to a finite set of additional hypotheses in . For instance, an environment in which we have functions , and a converter simply corresponds to the set . Again, we may consider models of the theory enriched with .

Logical types

Given a model or , we say that is a type if . In that case, we call

the set of instances of . Inversely, given a subset , it is natural to search for a type with . In order to ensure the existence of such types for simple sets, such as , it is useful to increase the expressiveness of our language through the possibility to form so called logical types.

More precisely, let and be the counterparts of , and , modulo the addition of new primitives and . The set is defined in a similar way as , modulo the following additional constructions:

The corresponding theory is obtained by adding the following axioms to :

In particular, , , etc.

Remark 4. The added primitive logical types correspond very naturally to basic programming constructs in Mathemagix:

1. The type corresponds to overloading. Indeed, an overloaded function , with two definitions and corresponds to the overloaded type .

2. The type corresponds to an anonymous union of and .

3. The type corresponds to a template type. For instance, the C++ template template<typename T> T square (T) gives rise to . In Mathemagix, template types are usually combined with a condition on the quantifier (see below).

4. The type corresponds to a generic type. For instance, is equivalent to the type of Mathemagix. Similarly, corresponds to a polynomial over some generic ring.

5. The type corresponds to a conditional type. The condition usually concerns a quantifier. For instance, a clean specification of squaring a ring element would be given by , which is really a notation for .

Initial models

Type resolution

Priorities