[Prev][Next][Index][Thread]

Better vector math using dependent types

I finally found the solution to a type theory problem that's been bugging me for years.  It's a twist on the "function parameters are covariant" problem, in the special case of mathematical objects like vector spaces and matrices.
 
Here I will use functions from natural numbers (or an upper-bounded subset of natural numbers) to real numbers to represent vectors.  You can think of such functions as fixed-length arrays of real numbers, or of floating point numbers -- I will be lax with the terminology.
 
-- The Problem --
 
When determining whether one function type (or array type, or vector type) is a subtype of another, type systems treat the function parameter type contravariantly.  Conceptually, this isn't what one wants with mathematical objects like vectors.
 
I will use fixed-length arrays as an example below and assume classic array typing rules.  However, you could see the same issue in C++ by declaring a class vec2d {float x,y;} and a class vec3D: public vec2D {float z;}, and a subclass vec4D containing yet another component.
 
Example of the problem in C-style pseudocode:
 
void Use3DVector(float[3] my3DVector) {
    ...do something here
}
void Example() {
    // Declare a 2D vector and a 4D vector.
    my2DVector b={1,2};
    my4DVector a={1,2,3,4};
 
    // Use the 4D vector. This succeeds because it's typesafe:
    // a 4D vector has all the components of a 3D vector and more.
    Use3DVector(my4DVector);
 
    // Use the 2D vector. This fails because it's not typesafe: a 2D
    // vector doesn't have certain components that a 3D vector has.
    Use3DVector(my2DVector);
}
 
In other words, traditional type systems inherently use these subtyping relationships
 
    .. <: float[4] <: float[3] <: float[2] <: float[1]
 
This is the opposite of how mathematicians look at vector spaces.  They see 1D space as a subspace of 2D space; 2D space as a subspace of 3D space, etc:
 
    float[1] <: float[2] <: float[3] <: ..
 
-- The Solution --
 
Define a new type "zero" which is a subtype of "float".  Type "zero" has only one instance, the value "0".  By definition of subtyping, all zeros are floats, but not all floats are zeros.  This is sound.
 
Since "zero" has only one instance, variables of type "zero" don't need to be stored; they take up no runtime storage.  Since they take up no storage, you can store infinitely many of them in a fixed-sized data structure.  I exploit this to represent vectors as infinite-length arrays consisting of a finite number of reals, followed by an infinite number of zeros.
 
Now, instead of looking at vectors in the Java style (float[0], float[1], etc.), we view them with dependent types, like:
 
    ForAll(i nat).if i<3 then float else zero // a 3d vector
    ForAll(i nat).if i<1 then float else zero // a 1d vector
 
Or concepually, you can think of vectors as the examples below, where "..." stands for "followed by infinitely many zeros":
 
    {float,float,float,zero...}
    {float,zero...}
 
If you define a generic type constructor vec(i) in the style above, you'll find that it's exactly what mathematicians want:
 
    vec(1) <: vec(2) <: vec(3) <: ...
 
You can verify this by looking at the "ForAll" expressions above, verifying that for every possible input value "i", the corresponding subtyping rules hold.  For example: {real,zero...} <: {real,real,zero...} because (looking at the first elements) real<:real, and (second elements) zero<:real, and (subsequent elements) zero<:zero, etc.
 
-- Other Benefits --
 
You can then derive types from constants, i.e. {2,1,0} has the type of a 2D vector because the third component is 0, whose exact type is zero rather than the more general float.
 
You can also type strangely-shaped vector spaces like {float,zero,float,zero...} -- the space of vectors with only X and Z components.
 
In languages supporting dependent types and pattern matching, many mathematical rules automatically fall out of the results.  For example, transforming a vector by a matrix which has one column of zeros yields a vector with the corresponding component set to zero -- not just at runtime, but in the type system as well, as long as the zeros are statically known.
 
-- Summary and Future Work --
 
By changing our representation of vectors from fixed-length arrays of reals, to infinite-sized arrays containing finitely many reals and infinitely many zeros, vectors now obey the subtype=subspace rules mathematicians want, rather than the covariant subtyping of traditional fixed-length arrays and records.
 
I am currently working on extending this approach to deal with the multivectors of Geometric (Clifford) Algebra.  There are many ways of doing this which don't involve any new type-theory constructs, but clearly nothing we can build out of ordinary dependent types will admit ordinary scalars, and the newly-defined vectors here, as elements of any more general multivector type.
 
However, I've found a new construct, sort of a "dimensionality-indexed transparent product" that gives you multivectors compatible with traditional scalars, and the vectors defined here.  Better yet, it admits imaginary numbers, complex numbers, quaternions, and spinors of arbitrary dimensionality as subtypes; and it always knows the more specific derivable type of your result.  This is still somewhat sketchy but I'd be glad to share it if there is any interest.
 
-Tim