Extensible type promotion for subtyping arithmetic

I thought the answer to abstracted algebra would be found from the type theory, but I ended up coming a full circle.

Back to where I started from last Autumn.

You have a set of type constructors, find an unique type, such that every type presented by type constructors can be converted into that form.

exist! y in S. forall x in S\{y}. x ---> y

If you have a consistently defined x ---> y -relation that can be reliably extended, then you can solve type promotion problems with relatively simple algorithm that you can derived directly from the above logical expression I just stated. The coercion result is the y type constructor in the set of type constructors.

When the operator has been decided, it will result in further coercions when the operation is evaluated.


{integer, rational} ===> rational
{rational, complex} ===> complex
{integer,   linalg} ===> linalg

The resulting coercion function does not depend on static typing, but neither prevents the static typing either.

The literals that appear in programs have to be sufficiently abstract. This means that they come to the bottom of the type promotion hierarchy. Integers, irrational and rational types are on bottom of the type promotion graph.

When you specify an exact shape for a type, you rarely want to deviate from that shape any further. This means that types such as uintN, intN, float, double terminate the promotion graph.

User defined base types come to the right side as well. Additionally new irrational constants can be described.

     |                               |---intN
                     |               |
                     |               |---double

The 'beef' in overloaded operators is the abstract algebraic modules though. The problem for type promotion is to decide which algebraic module to apply, if multiple modules appear in the same coercion.

The conclusion is that lifting between algebraic modules must be explicitly defined, although base types will be always attempted to be lifted into a module. This is not a perfect solution because not all base types can be reliably used in every module, and all valid liftings won't be necessarily defined.

The algebraic modules form their own coercion hierarchy such as below:

basetypes----dual----|                |----polynomial---linalg

Unlike in the case of base types, the user should be able to define arbitrary relations between coercions. If the coercions are too excessive, they will appear when using the type.

This is not the perfect solution I hoped for, but it is far much better than anything I have had so far.