Types and Indeterminates

Type-level indeterminate variables may allow ML-style full type inference cope with user-defined type promotions. I haven't worked out all the details, but here I have some theory for how this could work.

My rambling on type systems has been going on for a good while. I would really love to return to doing all the cool stuff I did but unfortunately it still has to wait. To really shine, I must figure this out!

Basis

The previous exploration I've covered in my blog posts has provided a basis during the last months. I found out how to create a subtyping prototype that produces binary relations to solve during type inference.

Here's an example of how it would work:

fibonacci(a) = 
    if a < 2 then 1
    else fibonacci(a-1) + fibonacci(a-2)

fibonacci :: a -> int
    (<) :: (a, int) -> T
    (-) :: (a, int) -> T

This means that fibonacci gets in some value and returns an integer. That value has to fit into binary relations for comparison and subtraction with an integer.

The binary relations leak out along the types that populate them. The relations that do not leak out among the type annotation can be already solved. Such is the one produced by (+) operation in fibonacci. It resolves to (int, int) -> int.

Problem

Many mathematical structures such as polynomials, complex and dual numbers are compatible with each other and can be mixed without violating any rules. On computers each mathematical structure needs a type to represent it.

Computer types have to match in order to allow calculations on them. Most type inferenced programming languages make this the responsibility of the programmer. Those language aren't helpful for people who write algebraically rich code.

You eventually end up with an arithmetic operation. Bivariate polynomials on the one side and the autodifferentiator on the another side. When that happens you would have to insert a conversion, but you also happen to use the same code with many other different types as an input.

People affected by this issue often get to hear how matrix multiplication is not arithmetic multiplication and that they should use a different operation and different routines to represent what they want to do. Before the sentence has been finished some of them have already abandoned Haskell or the other ML-variant they were going to try.

Computer representation of algebra

The types on a computer are usually made to compose the representation for a structure from the pieces that are currently available. Here are few examples with their corresponding computer representations.

Polynomials:        ax³ + bx² + cx + d  ......  [3.a, 2.b, 1.c, 0.d]
Complex numbers:    a + bi  ..................  {a, b}
Dual numbers:       a + bd  ..................  {a, b}

These are in a canonicalized form that form by pulling an indeterminate outside from them.

Note that the variable ends up being omitted. But we can reintroduce variables by assigning De-Bruijn indices for structures we use, in order they are stacked.

It's also useful to notice that we are solely working with polynomial representations here. I find polynomials themselves to be valuable enough for the subsequent ideas to matter.

Indeterminates mixed into types

Now lets get on to the types.

The De-Bruijn indices resolve many problems here. For example it allows us to treat complex(complex(a)) as a Cayley-Dickson construction. This type forms quaternions. Basically the first imaginary variable becomes distinct from the second imaginary variable because they implicitly get different indices.

We could also explicitly notate the indeterminates associated to the types. Eg. complex(complex(a, i), j). This has the benefit that we can change the outermost indeterminate in a value without changing the meaning of the value.

Pivot away from outermost indeterminate

Changing the outermost indeterminate is difficult, but can be done once you observe that calling a constructor with accessor produces a copy of the value. For example, with linked lists this gives you:

cons(car(a), cdr(a)) = copy(a)

This allows to automatically define map and traverse over any datatype you have.

map      :: (C(a), a -> b) -> C(b)
traverse :: (C(a), a -> unit) -> unit

The user needs to define operation pivot, function for embedding is provided as reference.

embed    :: a -> C(a)
pivot    :: (traverse(a{C(b)}), mapping(a{C(b)})) -> C(a{b})

An example of the pivot for complex numbers:

Complex(
    map(a, (i) -> i.real),
    map(a, (i) -> i.imag))

And the embed:

Complex(a, 0)

To maintain same meaning, for this kind of pivot it would appear to be necessary that the algebra formed by structures is distributive. Eg. For complex numbers and polynomials, the following equation holds:

(a+bi) + x*(c+di) = (a+x*c) + (b+x*d)i

Most specific common shape

The indeterminates in types give a sensible framework to describe what is involved in coercing two different values into the same format.

I still have not determined how traits affect all of this, a wrong structure in wrong place may violate the distributivity constraint and prevent the pivoting in coercion.

Isomorphisms and indeterminates

If you have conversions a -> b, b -> a, you have isomorphic objects. Theoretically if b is some common representation, then you can convert any other representation of that object to any other incommon representation.

The type conversion can be pinpointed with indeterminates. For example, if you wanted to transform imaginary number into a polynomial, you would substitute the imaginary value with the polynomial of your choice. In this case you could select the indeterminate for substitution and give it some value to substitute.

In the similar way, one could change between sparse and dense representation of polynomials or matrices. These would require explicit conversions, but would not intefere with use where you don't have imaginary or polynomial values.

Subtyping and Coercion

There have been research papers proposing that implicit coercion could be represented as subtyping. Although coercion can be treated as subtyping, I think that coercion is not subtyping.

Subtyping means that object satisfies constraints as it stands whereas coercion requires that there are points where the conversion happens. Object being coerced both gains properties it did not have and loses those that it had.

I'm not comfortable with the idea that the imag(5) would return 0 instead of a type error. At least for now.

Next

I am intending to turn this theory into a working prototype within the next two weeks. I may end up being interrupted by surprises so it's not certain that I get this technique implemented by then, but that's the goal.

I am going to post this to lobters because I'd like to get some visibility for these ideas, and I could use some feedback from people who have tried to solve this kind of a problem.

Similar posts