Turing Completeness Generic Java Types

Periodically on Habré you can find articles about what incredible things can be done on C ++ templates: finite automata , lambda calculus , Turing machine and much more.

Parameterized types in Java are traditionally considered to be only a parody of C ++ templates (despite the fact that they are somehow incorrectly compared), and the reasons for this are easy to understand. Nevertheless, not everything is so bad, and the Java compiler can be made to perform any calculations during type checking, if only enough RAM is enough. A specific way to do this was described in November 2016 in this beautiful publication . I would like to explain it.

For the seed give the following code. Is it correct? I propose to compile and check whether you guessed the result.

class Sample { interface BadList<T> extends List<List<? super BadList<? super T>>> {} public static void main(String[] args) { BadList<? super String> badList = null; List<? super BadList<? super String>> list = badList; } }

Find out the answer

The compiler will throw java.lang.StackOverflowError regardless of the stack size.

Let us see why the compiler behaves exactly this way (I would not call it a bug), how understanding these reasons can be useful, and where does the Turing machine.

1. On covariance and contravariance

First of all, let's talk about the basics. The easiest way to use parameterized types is something like this:

 List<Integer> integerList = new ArrayList<>(); List<Number> numberList = new ArrayList<>();

Usually this is enough, but there is a problem - the type of elements is rigidly fixed. We are not able to use an integerList object where List<Number> needed, since inserting a Double element into such a list would break its integrity. Conversely, you cannot use the numberList where List<Integer> is expected, since this will lead to a ClassCastException when reading the list items if there are non-integer numbers in it. Of course, to solve the second problem, you can use such a small trick:

 <T extends Number> Number firstNum(List<T> xs) { return xs.get(0); }

I call this a trick, because this approach requires the introduction of an additional type T Moreover, the problem of insertion in a similar way does not solve in principle. An alternative and, in my opinion, more correct version of this method should look like this:

 Number firstNum(List<? extends Number> xs) { return xs.get(0); }

It is said that such types are covariant in their parameters. This means that if A is a subtype of B , then List<A> (as well as List<? extends A> ) is a subtype of List<? extends B> List<? extends B> , which means assignment is allowed between them. A side effect is that such a list will be read-only and we cannot violate the integrity of any objects.
For the case of recording, there is another construction:

 void addOne(List<? super Integer> xs) { xs.add(1); }

List<? super Integer> List<? super Integer> describes a collection of lists in which you can add integers, that is, its subtypes are List<Integer> , List<Number> and List<Object> (plus List<? super Integer> , List<? super Number> and List<? super Object> respectively). Such classes are contravariant to their parameters, that is, if A is a supertype of B , then List<A> is a subtype of List<? super B> List<? super B> . The situation is exactly the opposite of the covariant case.

Focus on contravariant types.

2. Formalization of a subset of contravariant types

So, we will define, which types in Java interest us. We introduce the concept of inductively:

type parameter t is type ;
if C is a class with one parameter and t is a type , then the entry $Ct$ - this is also the type . Denote it will be an abbreviation for such a record: C<? super t> C<? super t> .

More complex types will be written as $C_1C_2 ... C_nt$ , which corresponds to this code:
C1<? super C2<? super ...Cn<? super t>...>>

We define the inheritance relation. So let there be a type
interface C<T> extends C1<C2<? super ...Cn<? super t>...>> interface C<T> extends C1<C2<? super ...Cn<? super t>...>> , in this case, we say that for any type or class without parameters X , the following inheritance relation holds: $CX <:: C_1C_2 ... C_nX$ . Symbol $<:: ^ *$ denote the transitive closure of a relation $<::$ (that is, in addition to direct, also indirect inheritance through a chain of classes).
Have a relationship $<:: ^ *$ There is one useful property - acyclicity. Since there is no multiple inheritance in Java, we can declare that:

if a $t <:: ^ * Cu$ and $t <:: ^ * Cu '$ then $u = u '$ ;
in particular if $Cu <:: ^ * Cu '$ then $u = u '$ .

Now you can finally enter the relationship is a subtype " $<:$ ".

For any type T we assume that it is its own subtype: $T <: t$ .
If the inheritance relation is satisfied $CT_1 <:: ^ * C_1C_2 ... C_nT_1$ and it is known that $T_2 <: T_1$ then executed $CT_1 <: C_1C_2 ... C_nT_2$ (I was not mistaken with the order $T_1$ and $T_2$ , this is all contra-variant).

In this place there is a significant limitation. To attitude $<:$ coincided with the standard way of defining subtypes in Java, it is necessary that in clause 2 the value of n odd.

Why it should be like this

I will not give a complete formal proof, it would be inappropriate long. It would be more correct to consider the situation in examples.

n = 1 :
interface S<T> extends C<T> {}
In this case, there is no question that S<? super X> S<? super X> is a subtype of C<? super X> C<? super X> , since this is a direct substitution of the parameter T

n = 3 :
interface S<T> extends C1<C2<C3<? super T>>> {}
Prove that is true $SX <: C_1C_2C_3X$ :

take type $Z$ such that $X <: z$ ;
it follows that $C_3Z <: C_3X$ ;
Consequently $C_2C_3X <: C_2C_3Z$ ;
Consequently $C_1C_2C_3Z <: C_1C_2C_3X$ ;
since C1<C2<? super C3<? super Z>>> C1<C2<? super C3<? super Z>>> C1<C2<? super C3<? super Z>>> is a subtype $C_1C_2C_3Z$ , it is also a subtype $C_1C_2C_3X$ ;
which means that S<Z> is a subtype $C_1C_2C_3X$ ;
if we consider Capture#1 of (? super X) as Z , then we get the truth $SX <: C_1C_2C_3X$ . This conclusion is valid thanks to JLS 4.10.2, I quote:
Given a generic type declaration $C <F_1, ..., F_n>$ (n> 0), the direct supertypes of the parameterized type $C <R_1, ..., R_n>$ where at least one of the $R_i (1 \ leq i \ leq n)$ supertypes of the parameterized type $C <X_1, ..., X_n>$ conversion to $C <R_1, ..., R_n>$ (§5.1.10)

n = 2 :
interface S<T> extends C1<C2<? super T>> {}
Let's pretend that $SX <: C_1C_2X$ :

in this case, there is a type Z = Capture of (? super X) (i.e. $X <: z$ ) such that S<Z> is a subtype $C_1C_2X$ ;
This place may seem controversial. I argue that since S<Z> is a subtype of C1<C2<? super Z>> C1<C2<? super Z>> , then C1<C2<? super Z>> C1<C2<? super Z>> also a subtype $C_1C_2X$ ;
from the previous paragraph it follows that $C_2X <: C_2Z$ ;
Consequently $Z <: x$ that is not exactly true. We have come to a contradiction.

Cases n> 2 are treated in the same way.

Now we can formulate the following theorem, which will be proved later:

Theorem 1
There is no algorithm that for any two given types $T_1$ and $T_2$ could determine if the statement is true $T_1 <: T_2$ .

In other words, it ’s generally not possible in Java to determine if one type is a subtype of another.

3. What do we mean by the Turing machine?

Turing Machine $\ tau$ - this is five $(Q, q_I, q_H, \ Sigma, \ delta)$ where $Q$ Is a finite set of states $q_I \ in Q$ Is the initial state $q_H \ in Q$ - this is the final state $\ Sigma$ Is the final alphabet and $\ delta: Q \ times \ Sigma_ \ bot \ rightarrow Q \ times \ Sigma \ times \ {\ bf {L}, \ bf {S}, \ bf {R} \}$ - This is a transition function . $\ bot$ Is an extra character not contained in $\ Sigma$ .

The configuration of the Turing machine is a four $(q, \ alpha, b, \ gamma)$ , wherein $q \ in Q$ Is the current state $\ alpha \ in \ Sigma ^ *$ - this is the left side of the tape , $b \ in \ Sigma_ \ bot$ Is the current character and $\ gamma \ in \ Sigma ^ *$ - this is the right side of the ribbon .

Machine step $\ tau$ displays many configurations in itself as follows:

$(q, \ alpha a, b, \ gamma) \ rightarrow (q ', \ alpha, a, b' \ gamma)$ for $\ delta (q, b) = (q ', b', \ bf {L})$ ;
$(q, \ alpha, b, \ gamma) \ rightarrow (q ', \ alpha, b', \ gamma)$ for $\ delta (q, b) = (q ', b', \ bf {S})$ ;
$(q, \ alpha, b, c \ gamma) \ rightarrow (q ', \ alpha b', c, \ gamma)$ for $\ delta (q, b) = (q ', b', \ bf {R})$ .

Border cases are also taken into account (the symbol $\ epsilon$ here means an empty string). They show that upon reaching the end of the line (on the left or on the right), the symbol is automatically added to it $\ bot$ :

$(q, \ epsilon, b, \ gamma) \ rightarrow (q ', \ epsilon, \ bot, b' \ gamma)$ for $\ delta (q, b) = (q ', b', \ bf {L})$ ;
$(q, \ alpha, b, \ epsilon) \ rightarrow (q ', \ alpha b', \ bot, \ epsilon)$ for $\ delta (q, b) = (q ', b', \ bf {R})$ .

Start the machine at the entrance $\ alpha_I$ Is a sequence of execution steps starting with the configuration $(q_I, \ epsilon, \ bot, \ alpha_I)$ . If a $\ tau$ reaches $q_H$ then we say the machine $\ tau$ completed ( halts ) at the entrance $\ alpha_I$ . If the transition function does not allow the next execution step, we will assume that the machine $\ tau$ breaks at the entrance $\ alpha_I$ .

4. Subtyping Machines

Let's start to tie together the concepts we have. The goal is to map the execution steps of the Turing machine to the type checking process in Java. Suppose we have such a query:

C_{1} C_{2} . . . C_{m} Z <: D_{1} D_{2} . . . D_{n} Z

$C_1C_2 ... C_mZ <: D_1D_2 ... D_nZ$

This statement, the truth or falsity of which is proposed to prove. For convenience, we introduce two alternative forms of recording:

\ begin {array} {ll} & ZC_mC_ {m-1} ... C_1 \ blacktriangleleft D_1D_2 ... D_nZ \\ = & ZD_nD_ {n-1} ... D_1 \ blacktriangleright C_1C_2 ... C_mZ \\ \ end {array}

$\ begin {array} {ll} & ZC_mC_ {m-1} ... C_1 \ blacktriangleleft D_1D_2 ... D_nZ \\ = & ZD_nD_ {n-1} ... D_1 \ blacktriangleright C_1C_2 ... C_mZ \\ \ end {array}$

We introduce two types of execution rules

c d o t r i g h t s q u i g a r r o w c d o t

$\ cdot \ rightsquigarrow \ cdot$ for our cars:

$(ZC_m ... C_1 \ blacktriangleleft Z) \ rightsquigarrow \ bullet$ , if a $C_1 ... C_mZ <:: ^ * Z$ ;
$(ZC_m ... C_1 \ blacktriangleleft D_1 ... D_nZ) \ rightsquigarrow (ZE_p ... E_2 \ blacktriangleright D_2 ... D_nZ)$ , if a $C_1 ... C_mZ <:: ^ * D_1E_2 ... E_pZ$ .

$\ bullet$ - This is a special configuration, called the final ( halting ).
Note that with the inheritance rule $C_1t <:: D_1E_2 ... E_pt$ and substituting type $t: = C_2 ... C_mZ$ , we get the following execution rule:

\ begin {array} {ll} & ZC_m ... C_2C_1 \ blacktriangleleft D_1D_2 ... D_nZ \\ \ rightsquigarrow & ZC_m ... C_2E_p ... E_2 \ blacktriangleright D_2 ... D_nZ \\ \ end {array}

$\ begin {array} {ll} & ZC_m ... C_2C_1 \ blacktriangleleft D_1D_2 ... D_nZ \\ \ rightsquigarrow & ZC_m ... C_2E_p ... E_2 \ blacktriangleright D_2 ... D_nZ \\ \ end {array}$

Also, due to contravariance of the types used, the following rule is true:

\ begin {array} {ll} & ZC_m ... C_1N \ blacktriangleleft ND_1 ... D_nZ \\ \ rightsquigarrow & ZC_m ... C_1 \ blacktriangleright D_1 ... D_nZ \\ \ end {array}

$\ begin {array} {ll} & ZC_m ... C_1N \ blacktriangleleft ND_1 ... D_nZ \\ \ rightsquigarrow & ZC_m ... C_1 \ blacktriangleright D_1 ... D_nZ \\ \ end {array}$

Using the rules introduced, one can understand what happens during type checking in the example from the beginning of the article (they fully comply with the Java type checking algorithm on the subset of contravariant types we have selected). It sets the inheritance relationship.

B a d L i s t t <:: L i s t L i s t B a d L i s t t

$BadList \; t <:: List \; List \; BadList \; t$ and request

B a d L i s t S t r i n g <: L i s t B a d L i s t S t r i n g

$BadList \; String <: List \; BadList \; String$ .
The chain of execution rules will be as follows:

\ begin {array} {ll} & String \; BadList \ blacktriangleleft List \; BadList \; String \\ \ rightsquigarrow & String \; BadList \; List \; List \ blacktriangleleft List \; BadList \; String \\ \ rightsquigarrow & String \; BadList \; List \ blacktriangleright BadList \; String \\ \ rightsquigarrow & String \; BadList \; List \ blacktriangleright List \; List \; BadList \; String \\ \ rightsquigarrow & String \; BadList \ blacktriangleleft List \; BadList \; String \\ \ rightsquigarrow & ... \ end {array}

$\ begin {array} {ll} & String \; BadList \ blacktriangleleft List \; BadList \; String \\ \ rightsquigarrow & String \; BadList \; List \; List \ blacktriangleleft List \; BadList \; String \\ \ rightsquigarrow & String \; BadList \; List \ blacktriangleright BadList \; String \\ \ rightsquigarrow & String \; BadList \; List \ blacktriangleright List \; List \; BadList \; String \\ \ rightsquigarrow & String \; BadList \ blacktriangleleft List \; BadList \; String \\ \ rightsquigarrow & ... \ end {array}$

As you can see, type checking loops, which is the reason for stack overflow during compilation. In general, the described process can be expressed as:

Expression $C_1 ... C_mZ <: D_1 ... D_nZ$ true if and only if there is a terminating process $(ZC_m ... C_1 \ blacktriangleleft D_1 ... D_nZ) \ rightsquigarrow ^ * \ bullet$ .

The example is more complicated

Consider the following class table:

\ begin {array} {rllrll} Q ^ Lt & <:: & LNQ ^ LLNt & Q ^ Rt & <:: & LNQ ^ RLNt \\ Q ^ Lt & <:: & EQ ^ {LR} Nt & Q ^ Rt & <:: & EQ ^ {RL} Nt \\ Et & <:: & Q ^ {LR} NQ ^ REEt & Et & <:: & Q ^ {RL} NQ ^ LEEt \\ \ end {array}

$\ begin {array} {rllrll} Q ^ Lt & <:: & LNQ ^ LLNt & Q ^ Rt & <:: & LNQ ^ RLNt \\ Q ^ Lt & <:: & EQ ^ {LR} Nt & Q ^ Rt & <:: & EQ ^ {RL} Nt \\ Et & <:: & Q ^ {LR} NQ ^ REEt & Et & <:: & Q ^ {RL} NQ ^ LEEt \\ \ end {array}$

Relevant source code

 interface N<T> {} interface L<T> {} interface QLR<T> {} interface QRL<T> {} interface E<T> extends QLR<N<? super QR<? super E<? super E<? super T>>>>>, QRL<N<? super QL<? super E<? super E<? super T>>>>> {} interface QL<T> extends L<N<? super QL<? super L<? super N<? super T>>>>>, E<QLR<? super N<? super T>>> {} interface QR<T> extends L<N<? super QR<? super L<? super N<? super T>>>>>, E<QRL<? super N<? super T>>> {}

We follow the execution of the machine at the entrance

Q_{R} E E Z <: L N L N E E Z

$Q_REEZ <: LNLNEEZ$ (abridged version):

\ begin {array} {ll} & ZEEQ ^ r \ blacktriangleleft Q ^ LEEZ \\ \ rightsquigarrow & ZEENL \ blacktriangleright Q ^ LLNEEZ \\ \ rightsquigarrow & ZEE \ blacktriangleright Q ^ LLNLNEEZ \\ \ rightsquigarrow ZE \ blacktriangleleft Q ^ {LR} NLNLNEEZ \\ \\ \\ \\ z \\\\\ blacktriangleleft Q ^ {LR} \ \ end {array}

$\ begin {array} {ll} & ZEEQ ^ r \ blacktriangleleft Q ^ LEEZ \\ \ rightsquigarrow & ZEENL \ blacktriangleright Q ^ LLNEEZ \\ \ rightsquigarrow & ZEE \ blacktriangleright Q ^ LLNLNEEZ \\ \ rightsquigarrow ZE \ blacktriangleleft Q ^ {LR} NLNLNEEZ \\ \\ \\ \\ z \\\\\ blacktriangleleft Q ^ {LR} \ \ end {array}$

Detailed option

... blacktrianglelt EEZ & (Q ^ Rt <: EQ ^ {RL} Nt) Rl} nq ^ leet ^ LLNEEZ \\ \ rightsquigarrow & ZEENL \ blacktriangleright Q ^ LLNEEZ \\ \ rightsquigarrow & ZEENL \ blacktriangleright LNQ ^ LLNLNEEZ & (Q ^ Lt <: LNQ ^ LLNt) \\ \ rig htsquigarrow & ZEEN \ blacktriangleleft NQ ^ LLNLNEEZ \\ \ rightsquigarrow & ZEE \ blacktriangleright Q ^ LLNLNEEZ \ rights \ igquararrow & ZEE \ blacktriangleright EQ ^ {LR} NLNLNEEZ & (Q ^ Lt <forte) } NLNLNEEZ \\ \ rightsquigarrow & ZEEQ ^ RNQ ^ {LR} \ blacktriangleleft Q ^ LR NLNLNEEZ & (Et <Q: LNLNEEZ \\ \ rightsquigarrow & ... \\ \ end {array}

$... blacktrianglelt EEZ & (Q ^ Rt <: EQ ^ {RL} Nt) Rl} nq ^ leet ^ LLNEEZ \\ \ rightsquigarrow & ZEENL \ blacktriangleright Q ^ LLNEEZ \\ \ rightsquigarrow & ZEENL \ blacktriangleright LNQ ^ LLNLNEEZ & (Q ^ Lt <: LNQ ^ LLNt) \\ \ rig htsquigarrow & ZEEN \ blacktriangleleft NQ ^ LLNLNEEZ \\ \ rightsquigarrow & ZEE \ blacktriangleright Q ^ LLNLNEEZ \ rights \ igquararrow & ZEE \ blacktriangleright EQ ^ {LR} NLNLNEEZ & (Q ^ Lt <forte) } NLNLNEEZ \\ \ rightsquigarrow & ZEEQ ^ RNQ ^ {LR} \ blacktriangleleft Q ^ LR NLNLNEEZ & (Et <Q: LNLNEEZ \\ \ rightsquigarrow & ... \\ \ end {array}$

This query also leads to looping type checking, but now it is a non-trivial loop. We implemented a full-fledged walk of the "triangle" in both directions on our improvised tape. You can verify that type checking is looping by using the following code:

 interface Z {} class Main { L<? super N<? super L<? super N<? super E<? super E<? super Z>>>>>> doit(QR<? super E<? super E<? super Z>>> v) { return v; } }

5. Building a Turing Machine

Having a turing machine $\ tau$ and input tape $\ alpha_I$ let's build types $t_1$ and $t_2$ so that $t_1 <: t_2$ then and only if $\ tau$ stops at the entrance $\ alpha_I$ .
For each state $q_s \ in Q$ we introduce 6 classes: $Q_s ^ {wL}$ , $Q_s ^ {wR}$ , $Q_s ^ L$ , $Q_s ^ R$ , $Q_s ^ {LR}$ and $Q_s ^ {RL}$ ; for each character $a \ in \ Sigma$ let's build a class $L_a$ . Symbol $\ bot$ from the definition of the Turing machine for convenience, we will write as $\ #$ it will correspond to the class $L _ \ #$ . We will also add 4 classes: $N$ , $E$ , $M ^ L$ and $M ^ R$ .

It looks a bit like the last example. Next will be an approximate description of their meaning and a specific way of emulating the transition function of the corresponding Turing machine.

$Q_s ^ {wL}$ and $Q_s ^ {wR}$ - these are essentially types $Q ^ L$ and $Q ^ R$ from the last example. Most of the time they wander along the tape. The Meaning of Types $Q_s ^ {LR}$ and $Q_s ^ {RL}$ also saved: they are needed to turn at the end of the tape. The only exception is when $Q_s ^ {wX}$ ( $X$ this $L$ or $R$ ) meets with his corresponding $M ^ X$ : he thus "turns" into $Q ^ X$ . $Q_H ^ {wX}$ - class for the final state, processed in a special way.
The full description looks like this:

$\ begin {array} {rllrlll} Q_s ^ {wL} t & <:: & L_aNQ_s ^ {wL} L_aNt & Q_s ^ {wR} t & <:: & L_aNQ_s ^ {wR} L_aNt & \ forall q_s \ in Q, a \ in \ Sigma \ cup \ {\ # \} \\ Q_s ^ {wL} t & <:: & M ^ RNQ_s ^ {wL} M ^ RNt & Q_s ^ {wR} t & <:: & M ^ LNQ_s ^ {wR} M ^ LNt & \ forall q_s \ in Q \\ Q_s ^ {wL} t & <:: & M ^ LNQ_s ^ Lt & Q_s ^ {wR} t & <:: & M ^ RNQ_s ^ Rt & \ forall q_s \ in Q \\ Q_s ^ {wL} t & <:: & EQ_s ^ {LR} Nt & Q_s ^ {wR} t & <:: & EQ_s ^ {RL} Nt & \ forall q_s \ in Q \ setminus \ {q_H \} \\ Q_H ^ {wL} t & <:: & EEZ & Q_H ^ {wR} t & < :: & EEZ \\ Et & <:: & Q_s ^ {LR} NQ_s ^ {wR} EEt & Et & <:: & Q_s ^ {RL} NQ_s ^ {wL} EEt & \ forall q_s \ in Q \\ \ end {array}$
$\ begin {array} {rllrlll} Q_s ^ {wL} t & <:: & L_aNQ_s ^ {wL} L_aNt & Q_s ^ {wR} t & <:: & L_aNQ_s ^ {wR} L_aNt & \ forall q_s \ in Q, a \ in \ Sigma \ cup \ {\ # \} \\ Q_s ^ {wL} t & <:: & M ^ RNQ_s ^ {wL} M ^ RNt & Q_s ^ {wR} t & <:: & M ^ LNQ_s ^ {wR} M ^ LNt & \ forall q_s \ in Q \\ Q_s ^ {wL} t & <:: & M ^ LNQ_s ^ Lt & Q_s ^ {wR} t & <:: & M ^ RNQ_s ^ Rt & \ forall q_s \ in Q \\ Q_s ^ {wL} t & <:: & EQ_s ^ {LR} Nt & Q_s ^ {wR} t & <:: & EQ_s ^ {RL} Nt & \ forall q_s \ in Q \ setminus \ {q_H \} \\ Q_H ^ {wL} t & <:: & EEZ & Q_H ^ {wR} t & < :: & EEZ \\ Et & <:: & Q_s ^ {LR} NQ_s ^ {wR} EEt & Et & <:: & Q_s ^ {RL} NQ_s ^ {wL} EEt & \ forall q_s \ in Q \\ \ end {array}$
$Q_s ^ {L}$ and $Q_s ^ {R}$ indicate to the machine that the time has come for the next step. Accordingly, for each rule $\ delta (q_1, a_1) \ rightarrow (q_2, a_2, \ bf {X})$ in the turing machine $\ tau$ we build a special inheritance relationship. In this case, do not forget about the special rules for working with the class. $L _ \ #$ :

$\ begin {array} {rlll} Q_s ^ {R} t & <:: & L_aNQ_ {s '} ^ {wR} L_bNM ^ LNt & \ forall (q_s, a) \ rightarrow (q_ {s'}, b, \ bf {L}) \\ Q_s ^ {R} t & <:: & L_aNQ_ {s '} ^ {wR} M ^ LNL_bNt & \ forall (q_s, a) \ rightarrow (q_ {s'}, b, \ bf {S} ) \\ Q_s ^ {R} t & <:: & L_aNQ_ {s '} ^ {wR} M ^ RNL_bNt & \ forall (q_s, a) \ rightarrow (q_ {s'}, b, \ bf {R}) \\ Q_s ^ {R} t & <:: & L _ \ # NQ_ {s '} ^ {wR} L _ \ # NL_bNM ^ LNt & \ forall (q_s, \ bot) \ rightarrow (q_ {s'}, b, \ bf {L }) \\ Q_s ^ {R} t & <:: & L _ \ # NQ_ {s '} ^ {wR} L _ \ # NM ^ LNL_bNt & \ forall (q_s, \ bot) \ rightarrow (q_ {s'}, b, \ bf {S}) \\ Q_s ^ {R} t & <:: & L _ \ # NQ_ {s '} ^ {wR} L _ \ # NM ^ RNL_bNt & \ forall (q_s, \ bot) \ rightarrow (q_ {s' }, b, \ bf {R}) \\ \ end {array}$
$\ begin {array} {rlll} Q_s ^ {R} t & <:: & L_aNQ_ {s '} ^ {wR} L_bNM ^ LNt & \ forall (q_s, a) \ rightarrow (q_ {s'}, b, \ bf {L}) \\ Q_s ^ {R} t & <:: & L_aNQ_ {s '} ^ {wR} M ^ LNL_bNt & \ forall (q_s, a) \ rightarrow (q_ {s'}, b, \ bf {S} ) \\ Q_s ^ {R} t & <:: & L_aNQ_ {s '} ^ {wR} M ^ RNL_bNt & \ forall (q_s, a) \ rightarrow (q_ {s'}, b, \ bf {R}) \\ Q_s ^ {R} t & <:: & L _ \ # NQ_ {s '} ^ {wR} L _ \ # NL_bNM ^ LNt & \ forall (q_s, \ bot) \ rightarrow (q_ {s'}, b, \ bf {L }) \\ Q_s ^ {R} t & <:: & L _ \ # NQ_ {s '} ^ {wR} L _ \ # NM ^ LNL_bNt & \ forall (q_s, \ bot) \ rightarrow (q_ {s'}, b, \ bf {S}) \\ Q_s ^ {R} t & <:: & L _ \ # NQ_ {s '} ^ {wR} L _ \ # NM ^ RNL_bNt & \ forall (q_s, \ bot) \ rightarrow (q_ {s' }, b, \ bf {R}) \\ \ end {array}$

$\ begin {array} {rlll} Q_s ^ {L} t & <:: & L_aNQ_ {s '} ^ {wL} M ^ LNL_bNt & \ forall (q_s, a) \ rightarrow (q_ {s'}, b, \ bf {L}) \\ Q_s ^ {L} t & <:: & L_aNQ_ {s '} ^ {wL} M ^ RNL_bNt & \ forall (q_s, a) \ rightarrow (q_ {s'}, b, \ bf {S} ) \\ Q_s ^ {L} t & <:: & L_aNQ_ {s '} ^ {wL} L_bNM ^ RNt & \ forall (q_s, a) \ rightarrow (q_ {s'}, b, \ bf {R}) \\ Q_s ^ {L} t & <:: & L _ \ # NQ_ {s '} ^ {wL} L _ \ # NM ^ LNL_bNt & \ forall (q_s, \ bot) \ rightarrow (q_ {s'}, b, \ bf {L }) \\ Q_s ^ {L} t & <:: & L _ \ # NQ_ {s '} ^ {wL} L _ \ # NM ^ RNL_bNt & \ forall (q_s, \ bot) \ rightarrow (q_ {s'}, b, \ bf {S}) \\ Q_s ^ {L} t & <:: & L _ \ # NQ_ {s '} ^ {wL} L _ \ # NL_bNM ^ RNt & \ forall (q_s, \ bot) \ rightarrow (q_ {s' }, b, \ bf {R}) \\ \ end {array}$
$\ begin {array} {rlll} Q_s ^ {L} t & <:: & L_aNQ_ {s '} ^ {wL} M ^ LNL_bNt & \ forall (q_s, a) \ rightarrow (q_ {s'}, b, \ bf {L}) \\ Q_s ^ {L} t & <:: & L_aNQ_ {s '} ^ {wL} M ^ RNL_bNt & \ forall (q_s, a) \ rightarrow (q_ {s'}, b, \ bf {S} ) \\ Q_s ^ {L} t & <:: & L_aNQ_ {s '} ^ {wL} L_bNM ^ RNt & \ forall (q_s, a) \ rightarrow (q_ {s'}, b, \ bf {R}) \\ Q_s ^ {L} t & <:: & L _ \ # NQ_ {s '} ^ {wL} L _ \ # NM ^ LNL_bNt & \ forall (q_s, \ bot) \ rightarrow (q_ {s'}, b, \ bf {L }) \\ Q_s ^ {L} t & <:: & L _ \ # NQ_ {s '} ^ {wL} L _ \ # NM ^ RNL_bNt & \ forall (q_s, \ bot) \ rightarrow (q_ {s'}, b, \ bf {S}) \\ Q_s ^ {L} t & <:: & L _ \ # NQ_ {s '} ^ {wL} L _ \ # NL_bNM ^ RNt & \ forall (q_s, \ bot) \ rightarrow (q_ {s' }, b, \ bf {R}) \\ \ end {array}$

These relationships look quite tricky, nevertheless, they can be traced a number of patterns. I will not analyze the mechanics of each, we will consider only a part.
$(q_s, a) \ rightarrow (q_ {s'}, x, \ bf {R})$ :

$\ begin {array} {ll} & ... Q_s ^ R \ blacktriangleleft L_aNL_bN ... \\ \ rightsquigarrow & ... NL_xNM ^ RQ_ {s'} ^ {wR} \ blacktriangleleft L_bN ... \\ \ rightsquigarrow & ... wandering ... \\ \ rightsquigarrow & ... NL_xQ_ {s '} ^ {wR} \ blacktriangleleft M ^ RNL_bN ... \\ \ rightsquigarrow & ... NL_xQ_ {s'} ^ {R} \ blacktriangleleft L_bN ... \\ \ rightsquigarrow & ... \\ \ end {array}$
$\ begin {array} {ll} & ... Q_s ^ R \ blacktriangleleft L_aNL_bN ... \\ \ rightsquigarrow & ... NL_xNM ^ RQ_ {s'} ^ {wR} \ blacktriangleleft L_bN ... \\ \ rightsquigarrow & ... wandering ... \\ \ rightsquigarrow & ... NL_xQ_ {s '} ^ {wR} \ blacktriangleleft M ^ RNL_bN ... \\ \ rightsquigarrow & ... NL_xQ_ {s'} ^ {R} \ blacktriangleleft L_bN ... \\ \ rightsquigarrow & ... \\ \ end {array}$

$(q_s, a) \ rightarrow (q_ {s'}, x, \ bf {S})$ :

$\ begin {array} {ll} & ... Q_s ^ R \ blacktriangleleft L_aNL_bN ... \\ \ rightsquigarrow & ... NL_xNM ^ LQ_ {s'} ^ {wR} \ blacktriangleleft L_bN ... \\ \ rightsquigarrow & ... wandering ... \\ \ rightsquigarrow & ... NL_xNM ^ L \ blacktriangleright Q_ {s '} ^ {wL} L_bN ... \\ \ rightsquigarrow & ... NL_x \ blacktriangleright Q_ {s'} ^ {L } L_bN ... \\ \ rightsquigarrow & ... \\ \ end {array}$
$\ begin {array} {ll} & ... Q_s ^ R \ blacktriangleleft L_aNL_bN ... \\ \ rightsquigarrow & ... NL_xNM ^ LQ_ {s'} ^ {wR} \ blacktriangleleft L_bN ... \\ \ rightsquigarrow & ... wandering ... \\ \ rightsquigarrow & ... NL_xNM ^ L \ blacktriangleright Q_ {s '} ^ {wL} L_bN ... \\ \ rightsquigarrow & ... NL_x \ blacktriangleright Q_ {s'} ^ {L } L_bN ... \\ \ rightsquigarrow & ... \\ \ end {array}$

$(q_s, a) \ rightarrow (q_ {s'}, x, \ bf {L})$ :

$\ begin {array} {ll} & ... NL_bQ_s ^ R \ blacktriangleleft L_aNL_yN ... \\ \ rightsquigarrow & ... NL_bNM ^ LNL_xQ_ {s'} ^ {wR} \ blacktriangleleft L_yN ... \\ \ rightsquigarrow & ... wandering ... \\ \ rightsquigarrow & ... NL_bNM ^ L \ blacktriangleright Q_ {s '} ^ {wL} L_xNL_yN ... \\ \ rightsquigarrow & ... NL_b \ blacktriangleright Q_ {s'} ^ {L } L_xNL_yN ... \\ \ rightsquigarrow & ... \\ \ end {array}$
$\ begin {array} {ll} & ... NL_bQ_s ^ R \ blacktriangleleft L_aNL_yN ... \\ \ rightsquigarrow & ... NL_bNM ^ LNL_xQ_ {s'} ^ {wR} \ blacktriangleleft L_yN ... \\ \ rightsquigarrow & ... wandering ... \\ \ rightsquigarrow & ... NL_bNM ^ L \ blacktriangleright Q_ {s '} ^ {wL} L_xNL_yN ... \\ \ rightsquigarrow & ... NL_b \ blacktriangleright Q_ {s'} ^ {L } L_xNL_yN ... \\ \ rightsquigarrow & ... \\ \ end {array}$

The remaining 9 cases are painted in the same way.

6. Fluent interface

Let's go back to the real world. We are talking about Java, which means that our reasoning should eventually lead to the writing of some code, preferably useful.
In the OOP world, there is such a thing as a fluid interface . You, probably, never met this name, but for certain saw its implementation in a code. In essence, this is just a cascade method call, the use of which is aimed at increasing readability, or something else. It looks like this:

 String s = new StringBuilder(a) .append(b) .append(c) .toString();

You can look at such a call chain in a new way - as a word . In this example, we have the alphabet {append, toString} and the word append append toString .
Suppose we want to ask the Java compiler to validate our call chain by checking if the corresponding word belongs to a predefined grammar. For example, do not allow words longer than 10 characters. It is clear that for the class StringBuilder nothing of the kind can be done, but you can try for your own interfaces.

Let, for example, we want to validate the call chains of the a , b and c methods. Also, let us have a Turing machine that can validate the words of the corresponding language ( subtyping machine with all its interfaces is attached).
Our goal is to ensure that for the a().b().c() call chain, the compiler runs the following query: $ZEENL _ \ # NM ^ LNL_aNL_bNL_cNL _ \ # Q_I ^ {wR} \ blacktriangleleft EEZ$ .

To do this, we write the following class:

 abstract class B<T> { static B<ML<? super N<? super LHash<? super N<? super E<? super E<? super Z>>>>>>> start; abstract QWRStart<? super LHash<? super N<? super T>>> stop(); abstract B<La<? super N<? super T>>> a(); abstract B<Lb<? super N<? super T>>> b(); abstract B<Lc<? super N<? super T>>> c(); }

It should be understood that here I describe only the signature, and not the implementation of the corresponding methods. On the implementation will be later.

If you look closely, you can see that the type of expression B.start.a().b().c().stop , written like this:

 QWRStart<? super LHash<? super N<? super Lc<? super N<? super Lb<? super N<? super La<? super N<? super ML<? super N<? super LHash<? super N<? super E<? super E<? super Z>>>>>>>>>>>>>>>

completely repeats the left side of the requested request. That is, the following line of code actually starts the required Turing machine while the type-checking algorithm is running:

 E<? super E<? super Z>> res = B.start.a().b().c().stop;

7. Safe Builder

Got it! With such a rich toolkit, it's time to create something intelligible.
I remember reading this article , I thought: "Interesting idea!". So, now it's my turn to do a safe Builder . The appearance of class B from the previous part dictates some restrictions, so my Builder will be a bit verbose.

So, I want to have the following code that could be validated by the compiler:

 User user = build(user() .withFirstName("John") .withLastName("Doe") .please() );

The requirements will be the simplest - so that both fields are initialized, and in that order and not more than once (I understand perfectly well that such a simple task can be solved with more suitable methods; the grammar example will be more complicated later).

The Turing machine for such a case will be quite simple. It has only 5 states: Start , First , Last , Finish and Halt . The alphabet will contain 3 characters: FirstName , LastName and Hash .
The transition function is as follows:

$(Start, Hash) \ rightarrow (First, Hash, \ bf {R})$
$(First, FirstName) \ rightarrow (Last, FirstName, \ bf {R})$
$(Last, LastName) \ rightarrow (Finish, LastName, \ bf {R})$
$(Finish, Hash) \ rightarrow (Halt, Hash, \ bf {R})$

Pretty straightforward. The car will only stop at the entrance $FirstName, LastName$ .

Source code describing this machine (will be inside UserBuilder)

 public interface N<X> {} public interface ML<X> {} public interface MR<X> {} public interface LFirstName<X> {} public interface LLastName<X> {} public interface LHash<X> {} public interface E<X> extends QLRStart<N<? super QWRStart<? super E<? super E<? super X>>>>>, QRLStart<N<? super QWLStart<? super E<? super E<? super X>>>>>, QLRFirst<N<? super QWRFirst<? super E<? super E<? super X>>>>>, QRLFirst<N<? super QWLFirst<? super E<? super E<? super X>>>>>, QLRLast<N<? super QWRLast<? super E<? super E<? super X>>>>>, QRLLast<N<? super QWLLast<? super E<? super E<? super X>>>>>, QLRFinish<N<? super QWRFinish<? super E<? super E<? super X>>>>>, QRLFinish<N<? super QWLFinish<? super E<? super E<? super X>>>>>, QLRHalt<N<? super QWRHalt<? super E<? super E<? super X>>>>>, QRLHalt<N<? super QWLHalt<? super E<? super E<? super X>>>>> {} public interface QLRStart<X> {} public interface QWLStart<X> extends ML<N<? super QLStart<? super X>>>, MR<N<? super QWLStart<? super MR<? super N<? super X>>>>>, LFirstName<N<? super QWLStart<? super LFirstName<? super N<? super X>>>>>, LLastName<N<? super QWLStart<? super LLastName<? super N<? super X>>>>>, LHash<N<? super QWLStart<? super LHash<? super N<? super X>>>>>, E<QLRStart<? super N<? super X>>> {} public interface QRLStart<X> {} public interface QWRStart<X> extends MR<N<? super QRStart<? super X>>>, ML<N<? super QWRStart<? super ML<? super N<? super X>>>>>, LFirstName<N<? super QWRStart<? super LFirstName<? super N<? super X>>>>>, LLastName<N<? super QWRStart<? super LLastName<? super N<? super X>>>>>, LHash<N<? super QWRStart<? super LHash<? super N<? super X>>>>>, E<QRLStart<? super N<? super X>>> {} public interface QLRFirst<X> {} public interface QWLFirst<X> extends ML<N<? super QLFirst<? super X>>>, MR<N<? super QWLFirst<? super MR<? super N<? super X>>>>>, LFirstName<N<? super QWLFirst<? super LFirstName<? super N<? super X>>>>>, LLastName<N<? super QWLFirst<? super LLastName<? super N<? super X>>>>>, LHash<N<? super QWLFirst<? super LHash<? super N<? super X>>>>>, E<QLRFirst<? super N<? super X>>> {} public interface QRLFirst<X> {} public interface QWRFirst<X> extends MR<N<? super QRFirst<? super X>>>, ML<N<? super QWRFirst<? super ML<? super N<? super X>>>>>, LFirstName<N<? super QWRFirst<? super LFirstName<? super N<? super X>>>>>, LLastName<N<? super QWRFirst<? super LLastName<? super N<? super X>>>>>, LHash<N<? super QWRFirst<? super LHash<? super N<? super X>>>>>, E<QRLFirst<? super N<? super X>>> {} public interface QLRLast<X> {} public interface QWLLast<X> extends ML<N<? super QLLast<? super X>>>, MR<N<? super QWLLast<? super MR<? super N<? super X>>>>>, LFirstName<N<? super QWLLast<? super LFirstName<? super N<? super X>>>>>, LLastName<N<? super QWLLast<? super LLastName<? super N<? super X>>>>>, LHash<N<? super QWLLast<? super LHash<? super N<? super X>>>>>, E<QLRLast<? super N<? super X>>> {} public interface QRLLast<X> {} public interface QWRLast<X> extends MR<N<? super QRLast<? super X>>>, ML<N<? super QWRLast<? super ML<? super N<? super X>>>>>, LFirstName<N<? super QWRLast<? super LFirstName<? super N<? super X>>>>>, LLastName<N<? super QWRLast<? super LLastName<? super N<? super X>>>>>, LHash<N<? super QWRLast<? super LHash<? super N<? super X>>>>>, E<QRLLast<? super N<? super X>>> {} public interface QLRFinish<X> {} public interface QWLFinish<X> extends ML<N<? super QLFinish<? super X>>>, MR<N<? super QWLFinish<? super MR<? super N<? super X>>>>>, LFirstName<N<? super QWLFinish<? super LFirstName<? super N<? super X>>>>>, LLastName<N<? super QWLFinish<? super LLastName<? super N<? super X>>>>>, LHash<N<? super QWLFinish<? super LHash<? super N<? super X>>>>>, E<QLRFinish<? super N<? super X>>> {} public interface QRLFinish<X> {} public interface QWRFinish<X> extends MR<N<? super QRFinish<? super X>>>, ML<N<? super QWRFinish<? super ML<? super N<? super X>>>>>, LFirstName<N<? super QWRFinish<? super LFirstName<? super N<? super X>>>>>, LLastName<N<? super QWRFinish<? super LLastName<? super N<? super X>>>>>, LHash<N<? super QWRFinish<? super LHash<? super N<? super X>>>>>, E<QRLFinish<? super N<? super X>>> {} public interface QLRHalt<X> {} public interface QWLHalt<X> extends ML<N<? super QLHalt<? super X>>>, MR<N<? super QWLHalt<? super MR<? super N<? super X>>>>>, LFirstName<N<? super QWLHalt<? super LFirstName<? super N<? super X>>>>>, LLastName<N<? super QWLHalt<? super LLastName<? super N<? super X>>>>>, LHash<N<? super QWLHalt<? super LHash<? super N<? super X>>>>>, E<E<? super User>> {} public interface QRLHalt<X> {} public interface QWRHalt<X> extends MR<N<? super QRHalt<? super X>>>, ML<N<? super QWRHalt<? super ML<? super N<? super X>>>>>, LFirstName<N<? super QWRHalt<? super LFirstName<? super N<? super X>>>>>, LLastName<N<? super QWRHalt<? super LLastName<? super N<? super X>>>>>, LHash<N<? super QWRHalt<? super LHash<? super N<? super X>>>>>, E<E<? super User>> {} public interface QLStart<X> extends LHash<N<? super QWLFirst<? super LHash<? super N<? super LHash<? super N<? super MR<? super N<? super X>>>>>>>>> {} public interface QRStart<X> extends LHash<N<? super QWRFirst<? super LHash<? super N<? super MR<? super N<? super LHash<? super N<? super X>>>>>>>>> {} public interface QLFirst<X> extends LFirstName<N<? super QWLLast<? super LFirstName<? super N<? super MR<? super N<? super X>>>>>>> {} public interface QRFirst<X> extends LFirstName<N<? super QWRLast<? super MR<? super N<? super LFirstName<? super N<? super X>>>>>>> {} public interface QLLast<X> extends LLastName<N<? super QWLFinish<? super LLastName<? super N<? super MR<? super N<? super X>>>>>>> {} public interface QRLast<X> extends LLastName<N<? super QWRFinish<? super MR<? super N<? super LLastName<? super N<? super X>>>>>>> {} public interface QLFinish<X> extends LHash<N<? super QWLHalt<? super LHash<? super N<? super MR<? super N<? super LHash<? super N<? super X>>>>>>>>> {} public interface QRFinish<X> extends LHash<N<? super QWRHalt<? super LHash<? super N<? super ML<? super N<? super LHash<? super N<? super X>>>>>>>>> {} public interface QLHalt<X> {} public interface QRHalt<X> {}

User UserBuilder ( ):

 public class User { private final String firstName; private final String lastName; private User(UserBuilder<?> builder) { this.firstName = builder.firstName; this.lastName = builder.lastName; } public String getFirstName() { return firstName; } public String getLastName() { return lastName; } public static User build(E<? super E<? super User>> e) { ... } public static UserBuilder<ML<? super N<? super LHash<? super N<? super E<? super E<? super User>>>>>>> user() { return new UserBuilder<>(); } public static class UserBuilder<X> { private String firstName; private String lastName; public UserBuilder<LFirstName<? super N<? super X>>> withFirstName(String firstName) { this.firstName = firstName; return (UserBuilder<LFirstName<? super N<? super X>>>) this; } public UserBuilder<LLastName<? super N<? super X>>> withLastName(String lastName) { this.lastName = lastName; return (UserBuilder<LLastName<? super N<? super X>>>) this; } public QWRStart<? super LHash<? super N<? super X>>> please() { ... } // interfaces ... } }

build .
— E<? super E<? super User>> , E . , e User , - . , , PECS (Producer Extends, Consumer Super). E :

 public interface E<X> extends Consumer<X>, ...

e void accept(E<? super User>) , E . Consumer User . , e.accept(callback) , build :

 public static User build(E<? super E<? super User>> e) { User[] ref = { null }; E<? super User> callback = user -> ref[0] = user; e.accept(callback); return ref[0]; }

;

please QWRStart , E<? super E<? super User>> . , , (, QWRStart E ):

 public QWRStart<? super LHash<? super N<? super X>>> please() { return (QWRStart) o -> { E<? super User> e = (E<? super User>) o; e.accept(new User(this)); }; }

, . , , , .. ()(()()) , ()())(() — . A B ( x — , , ).
:

$(Start, Hash)\rightarrow(Scan, Hash, \bf{R})$

$(Scan, B)\rightarrow(Back, x, \bf{L})$
$(Scan, Hash)\rightarrow(Check, Hash, \bf{L})$
$(Scan, A)\rightarrow(Scan, A, \bf{R})$
$(Scan, x)\rightarrow(Scan, x, \bf{R})$

$(Back, A)\rightarrow(Scan, x, \bf{R})$
$(Back, B)\rightarrow(Back, B, \bf{L})$
$(Back, x)\rightarrow(Back, x, \bf{L})$

$(Check, Hash)\rightarrow(Halt, Hash, \bf{S})$
$(Check, x)\rightarrow(Check, x, \bf{L})$

, , .
, .

 E<? super E<? super String>> e = start.A().A().B().B().stop();

 E<? super E<? super String>> e = start.B().A().B().A().stop();

8. Conclusion

. , .

— .
-, , Builder .
-, , . — .
-, . - ( ):

 incompatible types: QWRStart<capture#1 of ? super LHash<? super N<? super LFirstName<? super N<? super LLastName<? super N<? super ML<? super N<? super LHash<? super N<? super E<? super E<? super User>>>>>>>>>>>>> cannot be converted to E<? super E<? super User>>

. , :

;
, . .

? , , :

for fun;
. — .

Kotlin, , , Java , , .. Non-Expansive Inheritance Restriction . :

 interface A<T> interface B<T> : A<B<Anything<T>>>

Kotlin, . - , B B , T , . , .

— " " , . - Kotlin . , Kotlin .

, Java-, Kotlin , Java — . , Kotlin Java, , .

Links

Source: https://habr.com/ru/post/330724/

All Articles