# Typing Tasks Functional Cycle 13

_Note:_ The PR which introduces iterator locations to the type system is still open! Maybe it makes sense to merge that one first: https://github.com/GridTools/gt4py/pull/1037? The second task [‘Introducing a New List-Like Type to the Type System/Inference’](#Introducing-a-New-List-Like-Type-to-the-Type-SystemInference) would minimally change then (iterator location types have to be considered).

## Enable Type Inference on All IR Nodes

This requires registering all node types to the type unifier (respectively type renamer used by the unifier).

1. During the type collection (e.g., in `functional.iterator.type_inference._TypeInferrer` for the iterator IR), all node types have to be collected in some way. Could be stored directly within the IR nodes (e.g., in EVE’s metadata field) or in a dictionary mapping nodes to types.
- _Imporant:_ the type renamer must be able to modify these types, thus they should be put into a type ‘box’ (`functional.type_inference._Box`) at some point. With the dictionary-approach, this complexity can be hidden from the user. That is, the types can be collected as is, i.e., ‘unboxed’. So I would go with the dictionary strategy…
2. `functional.type_inference.unify` should accept a third optional argument. Some iterable of types or something similar (like `list[Type]`).
3. All types in the list should be boxed (that is, wrapped into a `_Box` instance).
4. All boxed types should be registered in `funtional.type_inference.unify` to the unifier’s renamer (i.e., using `unifier._renamer.register`).
5. After calling `unifier.unify`, all boxed types in the list should magically be correctly inferred.
6. The boxed types in the list can be unboxed.
7. Additionally to the main return type, the list of types can be returned.
8. Reindexing type variables and mapping from nodes to types can be handled in `functional.iterator.type_inference.infer`.

## Introducing a New List-Like Type to the Type System/Inference

This should be relatively straightforward:
1. Create a `class List(Type)` (or whatever its name should be) in `functional.iterator.type_inference`
2. The class should have one type parameter (that is, member), namely its type parameter (maybe called `element`) of type `Type`.
3. Done!

## Updating Builtin Functions

This is of course the pain point ;)

### Neighbor Shift

As discussed, we need two functions (using the notation introduced in [the intro slides of the type system](https://hackmd.io/@gridtools/Bkwp4lX75) plus `[T]` for the list type and `c` for a compile-time connectivity):

derefed_neighbor_shift(c) :: It[T₀¹] → [T₀]
neighbor_shift(c) :: It[T₀¹] → It[[T₀]¹] = lift(derefed_neighbor_shift)

If https://github.com/GridTools/gt4py/pull/1037 gets merged before (see note at beginning of document), you also have to consider the location types, which are actually the reason why the above definition makes sense while many others don’t. Then it would be (using the syntax introduced in the PR, i.e., first parameter of the iterator is the current location type, second parameter is the defined location type and third parameter is the value type):

derefed_neighbor_shift(c) :: It[T₂, T₃, T₀¹] → [T₀]
neighbor_shift(c) :: It[T₂, T₃, T₀¹] → It[T₂, src(c), [T₀]¹] = lift(derefed_neighbor_shift)

where `c` is again a compile-time connectivity and `src(c)` is the source location type of the connectivity (e.g., `Vertex` for `V2E`).

### A Generic Fold/Reduce

#### The Simple Base Case: Non-Variadic

If the newly introduced builtin (here called `fold`) for reductions is not variadic, things are quite simple, you just have to define its type like:

fold :: ((T₀, T₁) → T₀, T₀, [T₁]) → T₀  

Because the type system is a bit less straightforward and has `Val` as its general value type, this looks a bit more verbose, but is essentially the same:

fold :: ((Val[Value, T₀, T₁], Val[Value, T₂, T₁]) → Val[Value, T₀, T₁],
         Val[Value, T₀, T₁],
         Val[Value, List[T₂], T₁])
             → Val[Value, T₀, T₁]

In Python this would be (using the shortcut `Val_T0_T1` already available in `functional.iterator.type_inference`):

FunctionType(
    args=Tuple.from_elems(
        FunctionType(args=Tuple.from_elems(Val_T0_T1, 
                                           Val(kind=Value(),
                                               dtype=T2,
                                               size=T1)),
                     ret=Val_T0_T1),
        Val_T0_1,
        Val(kind=Value(), dtype=List(element=T2), size=T1),
    ),
    ret=Val_T0_T1,
)

This could be added to `BUILTIN_TYPES` as is.

Alternatively, you could also define the type of `fold` as partially curried, like:

fold :: ((T₀, T₁) → T₀, T₀) → [T₁] → T₀  

This would be a bit closer to the current definition of `reduce`, but does not matter here as the applied `fold` is anyway not liftable.

#### The Not-so-Simple Variadic Case

_But_ we have just ignored multi-argument reductions! There are multiple solutions:
1. Make `fold` variadic, like:

    fold :: ((T₀, T₁, T₂, …) → T₀, T₀, [T₁], [T₂], …) → T₀  

2. Introduce other non-variadic builtins, like `zip2`, `zip3`, …:

    zip2 :: ([T₀], [T₁]) → [(T₀, T₁)]
    zip2 :: ([T₀], [T₁], [T₃]) → [(T₀, T₁, T₃)]
    …

2. Introduce another variadic builtin, like `zip`:

    zip :: ([T₀], [T₁], …) → [(T₀, T₁, …)]

And as iterator IR _loves_ variadic functions (or rather single argument functions, that accept tuples of arbitrary size and adapt return types accordingly), you probably have to go one or another variadic path ;)

To understand how this can be achieved, you have to analyze the `ValTuple` class in `funtional.iterator.type_inference`. This is a very special type that handles comparison and constraint unification with ‘normal’ tuple types. You probably have to introduce a very similar thing, like `ValListTuple` or so, that stores the `element_dtypes` instead of `dtypes` and can be reduced to a tuple of `Val` with `List[element_dtype[…]]` as `dtype`.

Once this is done, the variadic `fold` can be implemented as follows. The key is the correspondence between the appearances of `T₂`, that is, the input value type of the reduction function (using `ValTuple`) and the type parameters of the lists (using proposed `ValListTuple`):

FunctionType(
    args=Tuple(
        front=FunctionType(args=Tuple(front=Val_T0_T1,
                                      others=ValTuple(kind=Value(),
                                                      dtypes=T2,
                                                      size=T1)),
                           ret=Val_T0_T1),
        others=Tuple(front=Val_T0_1,
                     others=ValListTuple(kind=Value(),
                                         element_dtypes=T2,
                                         size=T1))
    ),
    ret=Val_T0_T1,
)

### Make Lists?

Probably also add `make_list` to allow the user to construct sparse fields?