Affine Spaces and Type Theory

Question

From Wikipedia:

In an affine space, there is no distinguished point that serves as an origin. Hence, no vector has a fixed origin and no vector can be uniquely associated to a point. In an affine space, there are instead displacement vectors [...] between two points of the space.
Thus it makes sense to subtract two points of the space, giving a translation vector, but it does not make sense to add two points of the space. Likewise, it makes sense to add a displacement vector to a point of an affine space, resulting in a new point translated from the starting point by that vector.

Type or category theoretically (or API design-wise), a displacement vector is conceptually of a different type than than the points in the space (despite both being representable as vectors), and operators/operations exist such that they take an return arguments of different types.

C++ has several examples of of such types and associated algebras:

1. The most basic: Pointers (addresses in the memory address space) are distinct types from integers, they cannot be added together, but can be subtracted to give an integer or incremented by integers.
2. The standard <chrono> time header defines time_points and durations.

Other examples include geometry primitives like 2D, 3D...ND points or physical measurements like distances, time (see above), or any SI units.
Interestingly this aspect is orthogonal to aspects of unit-types.

I'm looking for literature and discussion of Affine Spaces in the context of Type-Theory (or Abstract Algebra). Specifically any formal definition of an algebra or specifications of the axioms or properties.

(I am not a mathematician so please forgive (and correct) any erroneous terminology).

Answer 1

nLab provides a multitude of axiomatic descriptions and (above where the link points) many conceptual descriptions. The simplest way of defining affine spaces is to say they are equipped with a "difference" operation that produces values in a vector space.

For APIs, I usually use an approach like the following (using C# syntax). (I also use a similar approach for torsors aka heaps which are a direct generalization of affine spaces and handles things like orientations versus rotations.)

interface Vector<V> where V : Vector<V> {
    V Add(V v);
    V Minus(V v);
    V Scale(double s);
}

interface Point<P, V> where V : Vector<V> where P : Point<P, V> {
    P Add(V v);
    V Minus(P p);
}

The $\Lambda$ operation specified in the first axiomatization on the nLab page corresponds to the Minus method on Point. The Add method on Point provides the unique $y$ such that $\Lambda(y,x)=v$. Rewriting the axioms in C#, it would look like (using x, y, and z for Points and v for Vectors):

x.Minus(x) = zero
x.Minus(y).Add(y.Minus(z)) = x.Minus(z)
x.Add(v).Minus(x) = v

zero is the zero vector of the corresponding vector space which I couldn't add as part of the C# interface. However, assuming any vector, v, exists then it is equal to v.Minus(v). If I wanted to avoid using zero in the first axiom I could have written: x.Minus(x) = x.Minus(x).Minus(x.Minus(x)) but that's a bit silly. We'd also have all the laws for vector spaces. As just one example, (u.Add(v)).Scale(r) = u.Scale(r).Add(v.scale(r)). For a practical API, you would likely arrange for operator overloading and to be able to add vectors to points on either side, i.e. x+v = v+x, and multiplying vectors by scalars on either side, i.e. r*v = v*r.