1.Categories

Generic programming in Mathemagix is based on the notion of a category. When writing generic functions (also called templates) or classes (also called containers), it is usually necessary to make assumptions on the type parameters.

Consider for instance the container Polynomial R for univariate polynomials. It is natural to use an internal representation for which the leading coefficient is non zero. The mere existence of an instance “zero” of type R constitutes a condition on R. Similarly, the ring operations on polynomials are naturally defined in terms of the ring operations on coefficients in R. Hence, R should at least be a ring (even though more structure might be needed for certain operations, such as the computation of greatest common divisors).

Categories are defined using the following syntax:

category Category_Name == category_body;

The body of a category consists of a block of prototypes of functionality required by the category. For instance, a typical definition of the Ring category is the following:

category Ring == {
  convert: Int -> This;
  prefix -: This -> This;
  infix +: (This, This) -> This;
  infix -: (This, This) -> This;
  infix *: (This, This) -> This;
}

The special type This corresponds to the carrier of the category. A type T is said to satisfy the category Category_Name in a given context (and we write T: Category_Name) if the context provides the required functionality in the body of the category, with This replaced by T. In a context where basix/fundamental.mmx has been included, we thus have Int: Ring, since the context provides us with operations

convert: Int -> Int;
prefix -: Int -> Int;
infix +: (Int, Int) -> Int;
infix -: (Int, Int) -> Int;
infix *: (Int, Int) -> Int;

However, we do not have String: Ring, since there is no implementation of infix - on strings.

2.Mathematical properties

It should be noticed that the notion of category satisfaction is purely syntactic: we simply look whether all prototypes in the body of the category are implemented in the current context, but we do not check any of the customary properties that the names of the category might suggest. For example, the type Double satisfies the category Ring, since the operations

convert: Int -> Double;
prefix -: Double -> Double;
infix +: (Double, Double) -> Double;
infix -: (Double, Double) -> Double;
infix *: (Double, Double) -> Double;

are all defined in basix/double.mmx. However, these operations are not associative: we typically have (1.0e100 + 1.0) - 1.0e100 != 1.0, due to rounding errors.

From the programming point of view this is really a feature, since it is desirable that straightforward implementations of containers such as Polynomial R can be instantiated for R Double. However, from the mathematical point of view, the code cannot certified to be correct under all circumstances.

Since Mathemagix aims to be an efficient general purpose mathematical programmer language rather than an automatic theorem prover, we have integrated no support for checking mathematical relations. Nevertheless, nothing prevents the user to informally introduce dummy functions which correspond to mathematical properties which are intended to be satisfied. For instance, the user might replace the definition of a ring by something like

category Ring == {
  convert: Int -> This;
  prefix -: This -> This;
  infix +: (This, This) -> This;
  infix -: (This, This) -> This;
  infix *: (This, This) -> This;
  associative_addition: This -> Void;
  commutative_addition: This -> Void;
  additive_inverse: This -> Void;
  associative_multiplication: This -> Void;
  …
}

The idea is that each of these additional functions stands for a mathematical property. For instance, associative_addition would stand for the property that for all in the carrier. A dummy implementation

associative_addition (x: T): Void == {}

of associative_addition corresponds to the assertion that the corresponding mathematical property is satisfied for T. However, this assertion is not checked by the compiler, and simply admitted on good faith.

3.Inheritance

It frequently happens that we want to declare new categories which are really extensions of already existing categories. For instance, the following category Field is really the extension of the category Ring with a division:

category Field == {
  convert: Int -> This;
  prefix -: This -> This;
  infix +: (This, This) -> This;
  infix -: (This, This) -> This;
  infix *: (This, This) -> This;
  infix /: (This, This) -> This;  
}

A shorter and more comprehensive way to define this category is

category Field == {
  This: Ring;
  infix /: (This, This) -> This;  
}

In other words, in our specification of the functionality of categories, we allow for prototypes of the form

This: Other_Category;

which really correspond to inheriting all functionality from another category. Multiple inheritance is allowed in the same way. For instance, assuming

category Ordered == {
  infix <=: (This, This) -> Boolean;
}

we may define

category Ordered_Ring == {
  This: Ring;
  This: Ordered;
}

4.Parameterized categories

Categories are allowed to be parameterized. The syntax for defining parameterized categories is similar to the syntax for the definition of containers:

category Cat (Param_1: Type_1, …, Param_n: Type_n) == category_body

The parameters are allowed to depend on each other in an arbitrary order, although cyclic dependencies are not allowed. The parameters may either be types or ordinary values.

Two examples of parameterized categories To F and From T were already encountered in the section on type converters:

category To (T: Type) == {
  convert: This -> T;
}

category From (F: Type) == {
  convert: F -> This;
}

Another typical example of a parameterized category is

category Vector_Space (K: Field) == {
  This: Abelian_Group;
  infix *: (K, This) -> This;
}

5.Planned extensions

One planned extension for categories concerns default implementations of certain methods. For instance, in the category Ring, the operation infix - is really redundant, since it admits a reasonable default implementation

infix - (x: This, y: This): This == x + (-y);

In the future, Mathemagix should be able to use such default implementations except when a better method is explicitly provided by the user. Notice that this requires a mechanism for specifying the required functionality for default methods. This is not completely trivial, since it should also be possible to provide a default implementation of prefix - in terms of infix -:

prefix - (x: This): This == (0 :> This) - x;

Of course, this should not lead to infinite loops if neither prefix - nor infix - is present.

6.Efficiency considerations