The 'force' Keyword: Coordinate System and Reference Frame Congruence

Introduction

Tracking coordinate systems and reference frames is a difficult but often mechanical task. Many operations can be performed congruently in any space, requiring only that every participating geometric object share a space representation.

We instruct Linguine to automate the unification of geometric objects using the force keyword. Specifically, code blocked off with force informs the compiler to attempt to unify the types of interacting vectors rather than raise a type error. Consider, for example, the following code:

// This syntax is not final, just what I'll use for examples
cartesian<world>.point x;
cartesian<model>.vector y;
force {
	cartesian<world>.point z = x + y;
}

Normally, this code would fail when attempting to typecheck x+y -- you can't operate between two geometric objects in different reference frames. With the force block, however, this code is actually replaced with the following type-correct code:

cartesian<world>.point x;
cartesian<model>.vector y;
cartesian<world>.point z = x + (y in world);

Automating space transformations cannot always be done safely or efficiently, however. In this document, we will explore the requirements, results, and optimization restrictions of applying automatic space unification.

Force Requirements

There are several type-level requirements we must enforce on automatic space unification to avoid unexpected or undefined behavior.

The first and most immediate of these requirements is that an operation is permitted on the provided geometric objects. This avoids the user being able to, say, add two positions, as these operations have undefined geometric behavior regardless of coordinate system or reference frame.

The second requirement is that there actually exists an in expression path between reference frames. Specifically, for an operation between an n-tuple x in reference frame A and an n-tuple y in reference frame B, we require that either x in B or y in A typecheck.

Third, Linguine requires that the given operation be defined in a coordinate system reachable by both components. This introduces an important distinction from reference frames -- not every operation is defined or even definable in every coordinate system. Concretely, to apply force on an operation defined in coordinate system C to n-tuples x and y, respectively, the following statements must typecheck: x in C and y in C.

Finally, there is a requirement not enforced by Linguine that geometric operations applied under force are space congruent. Informally, this requirement is simply that geometric operations act on objects the same regardless of which coordinate system and reference frame these objects are in. That is, for geometric operation op, all objects x and y (which are in the same space) and all reachable reference frames and coordinate systems A, the following must hold:

op(x, y) in A == op(x in A, y in A)

The foundation for this requirement is the notion that coordinate systems and reference frames simply provide different numeric representations of the same geometric objects. Any well=formed geometric operation should thus have equivalent definitions in all spaces (or undefined in a coordinate system).

Application Results

When the conditions defined in \ref{Force Requirements} are fulfilled, Linguine can begin inserting in expressions on operations recursively. Types are unified starting with the outermost operation and working inward, with the goal of minimizing the number of space transformations. Consider the following code snippet:

cartesian<model>.point pixel = ...;
cartesian<world>.vector offset = ...;
spherical<world>.rotation rotation = ...;

force {
	cartesian<view>.point result = rotate(pixel + offset, rotation);
}

To resolve this force block, Linguine needs to reduce the operation cartesian~point~world result = rotate(pixel + offset, rotation);. In expressions are introduced and checked through the following steps:

cartesian<view>.point result = ... ->
cartesian<camera>.point result = ... in camera ->
... = rotate(pixel + offset, rotation) in camera ->
... = rotate(pixel + offset, rotation in world) in camera ->
... = rotate(pixel in world + offset, rotation in cartesian) in camera ->

As can be seen in this example, this strategy avoids issues such as applying (pixel + offset) in spherical. While this cast would be valid and perhaps even intuitive, it would require that we immediately cast back to cartesian coordinates -- an extra operation which this optimization can eliminate.

As usual, there are restrictions and cases where the inference provided by force fails which require further examination.

For the force operation to work properly, Linguine needs a resultant type -- a 'starting point' for the algorithm. This can be kept as auto, in which case Linguine will simply unify to whichever space is closest. Avoiding auto is recommended, however, since writing correct and efficient code can be difficult when the space types are completely abstracted.

in expressions have special meaning in a force block. While force normally has the flexibility to apply in expressions as needed to unify n-tuples for operations, in expressions act as invariants indicating that the space of the transformed object is fixed. In the case where these invariants produce a program that cannot be unified, the Linguine compiler produces a type error. This feature allows the user to specify a unchanging space in force blocks, either for efficiency or clarity. Additionally, this allows partial removal of a force block to 'lock in' certain transformations within a block of code. NOTE: I'm on the fence if the above paragraph should be true. It might be too confusing / specific of a feature, and I'm not sure the use-case of partial forcing is worth the mental overhead.

Optimizations

Linguine will only attempt to 'pre-unify' types in cases where the target space has a definition for the given operation. In the above example, if we chose not to provide a definition of rotate in cartesian coordinates, then Linguine would unify pixel + offset to spherical coordinates to make the rotate operation possible. Linguine will not, however, attempt to reason about the optimal choice of space for an operation beyond minimizing the number of transformations. This sort of 'space' optimization can be required by the user by omitting definitions for operations in spaces that are suboptimal.

TODO: Finish this paragraph describing the repetition of spaces permitted over a total force block.