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 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.