# Shifts & Lifts Interpretation

For inlining lifts, we use:

$$\begin{equation}
\mathrm{deref}\Bigr(\mathrm{shift}\bigl(o_1, …\bigr)\bigl(\mathrm{lift}(f)(x)\bigr)\Bigl) \equiv f\bigl(\mathrm{shift}(o_1, …)(x)\bigr),
\tag{1}\label{inline}
\end{equation}$$

which gives

$$\begin{equation}
\mathrm{deref}\bigl(\mathrm{lift}(f)(x)\bigr) \equiv f(x)
\tag{2}\label{inline-no-shifts}
\end{equation}$$

if there are no offsets. Using $\eqref{inline}$ and $\eqref{inline-no-shifts}$, we derive:

$$\begin{align}
\mathrm{deref}\Bigr(\mathrm{shift}\bigl(o_1, …\bigr)\bigl(\mathrm{lift}(f)(x)\bigr)\Bigl) &\equiv f\bigl(\mathrm{shift}(o_1, …)(x)\bigr), \\
\mathrm{deref}\Bigr(\mathrm{shift}\bigl(o_1, …\bigr)\bigl(\mathrm{lift}(f)(x)\bigr)\Bigl) &\equiv \mathrm{deref}\Bigl(\mathrm{lift}\bigl(f\bigr)\bigl(\mathrm{shift}(o_1, …)(x)\bigr)\Bigr), \\
\mathrm{shift}\bigl(o_1, …\bigr)\bigl(\mathrm{lift}(f)(x)\bigr) &\equiv \mathrm{lift}\bigl(f\bigr)\bigl(\mathrm{shift}(o_1, …)(x)\bigr) \\
\tag{3}\label{inline-derived}
\end{align}$$

and further

$$\begin{align}
\mathrm{deref}\bigl(\mathrm{lift}(\mathrm{deref})(x)\bigr) &\equiv \mathrm{deref}(x) \\
\mathrm{lift}(\mathrm{deref})(x) &\equiv x.
\tag{4}
\end{align}$$

Additionally, for shifts, we use:

$$\begin{equation}
\mathrm{shift}\bigl(o_1, …\bigr)\bigl(\mathrm{shift}(p_1,…)(x)\bigr) \equiv \mathrm{shift}(p_1, …, o_1, …)(x).
\tag{5}
\end{equation}$$

Now, assume $f = \lambda(x).\mathrm{deref}\bigl(\mathrm{shift}(\mathrm{E2V}, 0)(x)\bigr)$ with type $\mathrm{Iterator}[T, \mathrm{Edge}] → T$ or maybe $\mathrm{Iterator}[T, \mathrm{Edge}] → \mathrm{Value}[T, \mathrm{Vertex}]$ if we want to keep the location type of values. In any case, $\mathrm{lift}(f)$ obviously has the type $\mathrm{Iterator}[T, \mathrm{Edge}] → \mathrm{Iterator}[T, \mathrm{Vertex}]$.

So, if we look at the expression

$$\begin{equation}
\mathrm{shift}(\mathrm{V2E}, 0\bigr)\bigl(\mathrm{lift}(f)(y)\bigr) \equiv \mathrm{shift}(\mathrm{V2E}, 0\bigr)\biggl(\mathrm{lift}\Bigl(\lambda(x).\mathrm{deref}\bigl(\mathrm{shift}(\mathrm{E2V}, 0)(x)\bigr)\Bigr)(y)\biggr),
\end{equation}$$

it is clear that the type of $y$ is $\mathrm{Iterator}[T, \mathrm{Edge}]$, the type of $\mathrm{lift}(f)(y)$ is $\mathrm{Iterator}[T, \mathrm{Vertex}]$, and the type of the full expression is $\mathrm{Iterator}[T, \mathrm{Edge}]$.

But now, from $\eqref{inline-derived}$, we get

$$\begin{equation}
\mathrm{shift}(\mathrm{V2E}, 0\bigr)\biggl(\mathrm{lift}\Bigl(\lambda(x).\mathrm{deref}\bigl(\mathrm{shift}(\mathrm{E2V}, 0)(x)\bigr)\Bigr)(y)\biggr) \\
\hspace{5em}\equiv \mathrm{lift}\Bigl(\lambda(x).\mathrm{deref}\bigl(\mathrm{shift}(\mathrm{E2V}, 0)(x)\bigr)\Bigr)\bigl(\mathrm{shift}(\mathrm{V2E}, 0)(y)\bigr).
\end{equation}$$

That is, we want to evaluate $\mathrm{shift}(\mathrm{V2E}, 0)(y)$, but the location type of $y$ is $\mathrm{Edge}$, thus the expression is invalid.

## Post-meeting thoughts (Enrique):
I haven't verified if this new suggestion works for all our known examples and use cases, but I'm writing it here in case you want to give it a thought during my day off, while the last discussion is still fresh.

### Iterators
Let's define _Iterator_ as a generic type with 3 type parameters `It[I, P, DT]`:
- `I`: type of the current position.
- `P`: type of the target position on the field referenced by the iterator.
- `DT`: scalar data type of the elements of the field.

A naive implementation of `It` could be:

class It[I, P, DT]:
    pos: I
    field: Field[P, DT]   
    
def shift(conn: Callable[[I], J], it: It):
    return it(pos=conn(it.pos), field=it.context)

# def lift(f: Stencil):
#     return lambda it: It(pos=it.pos, field=f(it.field)

# def lifted_f(y: It[Edge, Vertex, f64]):
#     return it(pos=it.pos, field=field(domain=Edge, f(field.data))   

It's easy to see intuitively that an iterator can only be safely derreferenced when `I` == `P`.

In this formulation,`shift()` has the expected signature:

shift(I->J)(It[I, P, DT]): It[J, P, DT]

A `Stencil` is a function from iterators to values. Let's take the example of `f` below and annotate it with the right types:

E2V: Edge -> Vertex

# The type of `y` is constrained by the `shift()`
# and `deref()` operations in the body of the function
def f(y: It[Edge, Vertex, f64]) -> f64:
    shifted: It[Vertex, Vertex, f64] = shift(E2V)(y)
    return deref(shifted)

Given this function `f`, the problem is how to define the type of `lift(f)`. I have now strong reasons to suggest the following (being `I` a generic type variable as above):

lift(f): It[I, Vertex, f64] -> It[I, Edge, f64]

and therefore `lift()` has the following generic signature:

lift: (It[I, P, DT1] -> DT2) -> (It[J, P, DT1] -> It[J, I, DT2]) 

So `lift(f)` does not change the type of the current position of the function arguments, but it changes the type of their target positions.

### Fields

A _Field_ is a **Profunctor**, which can be intuitively defined as a generic type with two type parameters `a` and `b` usually representing some kind of mapping from an `a` input value to a `b` output value (this is not the real definition, just an intuition). Functions can be combined with profunctors to form new profunctors. At the output type `b`, functions are composed as usual; at the input type `a`, functions are composed in the opposite direction.