# Applier target inferencing

Composition produces a tree of nodes and uses an applier to build and make changes to the tree
implied by composition. If a composable function directly or indirectly calls `ComposeNode` then it
is tied to an applier that can handle the type of node being emitted by the
`ComposeNode`. `ComposeNode` contains a runtime check to ensure that the applier is of the expected
type. However, currently, there is no warning or error generated when a composition function is
called that expects a different applier than is provided.

For Compose UI 1.0 this was not as important as there are only two appliers used by Compose UI, the
`UIApplier` and the `VectorApplier` and vector composable are rarely used so calling the incorrect
composable function is rare. However, as appliers proliferate, such as Wear projections,  or menu
trees for Compose Desktop, the likelihood of calling an incorrect composable grows larger and
detecting these statically is more important.

Requiring to specify the applier seems clumsy and inappropriate since, in 1.0, it wasn't necessary,
and especially since the inference rules are fairly simple. There is only one parameter that needs
to be determined, the type of the applier of the implied `$composer` parameter. From now on I will
be referring to this as the type of the applier when it technically is the type of the applier
instance used by the composer. In most cases the applier type is simply the applier type required
by composition functions it calls. For example, if a composable function calls `Text` it must be a
`UiApplier` composable because `Text` requires a `UIApplier`.

## Sketch of the algorithm

The following Prolog program demonstrates how type type of the applier can be inferred from the
content of the function (https://swish.swi-prolog.org/p/Composer%20Inference.swinb):

```
% An empty list can have any applier.
applier([], _).

% A list elements must have identical appliers.
applier([H|T], A) :- applier(H, A), applier(T, A).

% A layout has a uiApplier
applier(layout, uiApplier).

% A layout with content has a uiApplier and its content must have a uiApplier.
applier(layout(C), uiApplier) :- applier(C, uiApplier).

% A vector has a vector Applier.
applier(vector, vectorApplier).

% A vector with content has a vector applier and its content must have a vector applier
applier(vector(C), vectorApplier) :- applier(C, vectorApplier).
```


The above corresponds to calling `ComposeNode` (from Layout.kt and Vector.kt) and can easily be
derived from the body of the call. Taking advantage of of Prolog's unification algorithm, this can
also express open composition functions like the `CompositionLocalProvider`,

```
% provider provides information to its content for all appliers.
applier(provider(C), A) :- applier(C, A).
```

This predicate binds `A` to whatever applier the content `C` requires. In other words, `A` is an
open applier bound by the lambda passed into `provider`.

The above allows the validation that the composition function represented by, for example,

```
program(
           row([
               drawing([
                    provider([
                             circle,
                             square
                    ])
               ])
            ])
).
```


will not generate an applier runtime error (demonstrated in the link above).

## Declarations

Inferring the applier type is translated into inferring one of two attributes for every composable
function or composable lambda type, `ComposableTarget` and `ComposableOpenTarget`.

```
@Retention(AnnotationRetention.BINARY)
@Target(
    AnnotationTarget.FUNCTION,
    AnnotationTarget.PROPERTY_GETTER,
    AnnotationTarget.TYPE,
    AnnotationTarget.TYPE_PARAMETER,
)
annotation class ComposableTarget(val applier: String)
```

```
@Retention(AnnotationRetention.BINARY)
@Target(
    AnnotationTarget.FUNCTION,
    AnnotationTarget.PROPERTY_GETTER,
    AnnotationTarget.TYPE,
    AnnotationTarget.TYPE_PARAMETER,
)
annotation class ComposableOpenTarget(val index: Int)
```

## Inferring appliers

Every composable function has an applier scheme determined by the composable functions it calls or
by explicit declarations. The scheme for a function is the applier token or open token variable for
each `@Composable` function type in the description including the description itself and
corresponds to the applier required by the respective composable function.

For the purposes of this document, the scheme is represented by a Prolog-like list with identifier
symbols being bound and [deBruijn](https://en.wikipedia.org/wiki/De_Bruijn_index) indices (written
as a backslash followed by the index such as `\1`) are unbound variables and unbound variables with
the same index bind together. A scheme is a list where the first element is the variable or token
for the `$composer` of the function followed by the schemes for each composable parameter (which
might also contain schemes for its parameters).

For example, a composable function declared as,

```
@Composable
@ComposableTarget("UI")
fun Text(value: String) { … }
```

has the scheme `[UI]`.

Open appliers, such as,

```
@Composable
@ComposableOpenTarget(0)
fun Providers(
  providers: vararg values: ProvidedValue<*>,
  content: @ComposableOpenTarget(0) @Composable () -> Unit
) {
  …
  content()
  …
}
```

Has the scheme `[\0, [\0]]` meaning the applier for `Providers` and the `content` lambda must be
the same but they can be any applier. Using these schemes an algorithm similar to the Prolog
algorithm can be implemented. That is, when type variables are bound, the variables are unified
using a normal unify algorithm. As backtracking is not needed so a simple mutating unify algorithm
can be used as once unification fails the failure is reported, the requested binding is ignored,
and the algorithm continues without backtracking.

When inferring an applier scheme,

1. The applier schemes are determined for each composable call directly in the body of the
   composable function.  If the function is inferred recursively while its scheme is being inferred
   then a scheme with all unique deBruijn indices matching the shape of the expected scheme is used
   instead.
2. A scheme is recursively inferred for all nested lambdas literals.
3. Applier variables are created for the function and each composable lambda parameter of the
   function.
4. For each call, fresh applier variables are created and are bound as defined by the scheme
   of the call; the symbols are bound and type variables with the same index in the scheme are
   bound together. Then,
    1. the first fresh variable is bound to the function's variable
    2. the composable lambda parameters are bound to the lambda literals or variable references
    3. if a lambda expression is passed as a parameter it is treated as if it was called at the
       point of the parameter expression evaluation using the scheme declared or inferred for the
       type of the formal lambda parameter. If the expression is a lambda literal the variables are
       bound to both the scheme inferred for the lambda literal and the scheme of the type.
5. The scheme is created by resolving each applier variable for the function. If it is bound to a
   token then the token is placed in the scheme. If it is bound to a still open variable then the
   variable group is given a number (if it doesn't have one already) and the corresponding deBruijn
   index is produced. A variable's group is the set of type variables that are bound together with
   the type variable. An open type parameter can only be a member of one group as, once it is bound
   to another variable, it either is bound to a token or the variable groups are merged together.

For each function or type with an inferred scheme the declaration is augmented with attributes
where `CompositionTarget` is produced for tokens and `CompositionOpenTarget` is produced with the
deBruijn index. This records the information necessary to infer appliers across module boundaries.

If any of the bindings fails (that is if it tries to unify to two different tokens) a diagnostic is
produced and the binding is ignored. Each variable can contain the location (e.g. PsiElement) that
it was created for. When the binding fails, the locations associated with each variable in the
binding group can be reported as being in error.

# Implementation Notes

## `ComposableInferredTarget`

Due to a limitation in how annotations are currently handled in the Kotlin compiler, a plugin
cannot add annotation to types, specifically the lambda types in a composable function. To work
around this the plugin will infer a `ComposableInferredTarget` on the composable function which
contains the scheme, as described above, instead of adding annotations to the composable lambda
types in the function. For the target type checking described here `ComposableInferredTarget`
takes presedence over any other attriutes present on the function. The implementation dropped
the leading `\` from the deBruijn indexes, to save space, as they were unnecessary.

## Unification

Because backtracking is not required, the unify algorithm implemented takes advantage of this
by using a circular-linked-list to track the binding variables (two circular-linked lists can
be concatenated together in `O(1)` time by swapping next pointer of just one element in each).
The bindings can be reversed (e.g. swapping the next pointers back), but the code is not
included to do so, so if backtracking is later required, `Bindings` would need to be updated
accordingly. Details are provided in the class.
