{'fraction_non_alphanumeric': 0.036966286333832414, 'fraction_numerical': 0.004840208580721772, 'mean_word_length': 4.586746466685896, 'pattern_counts': {'":': 0, '<': 1, '<?xml version=': 0, '>': 0, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 21, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
A systematic approach to deriving incremental type checkers

Static typing can guide programmers if feedback is immediate. Therefore, all major IDEs incrementalize type checking in some way. However, prior approaches to incremental type checking are often specialized and hard to transfer to new type systems. In this paper, we propose a systematic approach for deriving incremental type checkers from textbook-style type system specifications. Our approach is based on compiling inference rules to Datalog, a carefully limited logic programming language for which incremental solvers exist. The key contribution of this paper is to discover an encoding of the infinite typing relation as a finite Datalog relation in a way that yields efficient incremental updates. We implemented the compiler as part of a type system DSL and show that it supports simple types, some local type inference, operator overloading, universal types, and iso-recursive types.


INTRODUCTION
Many programming languages employ a static type system to check user-defined invariants at compile time. Indeed, programmers of statically typed languages often rely on feedback from the type checker for guidance. Unfortunately, type checking can take significant time for larger programs and can interrupt the programmer's development flow. Therefore, it is hardly surprising that virtually all major IDEs incrementalize type checking in some way. Unfortunately, most of these solutions are highly specialized and generally hard to transfer to a new type system. We lack a principled solution for incrementalizing type checkers. This paper presents a systematic approach for deriving incremental type checkers from textbookstyle type system specifications. While we hope to incrementalize advanced type systems eventually, in this paper we focus on building a sound foundation for the most elemental type system features: name binding and type errors. These features constitute fundamental challenges for incremental type checking, and we believe it is essential to develop principled solutions to such fundamental challenges first. Nonetheless, our approach already supports a number of sophisticated type systems.
Our approach is based on the idea of compiling inference rules to the logic programming language Datalog. Targeting Datalog is promising because efficient incremental Datalog solvers already exist [Ujhelyi et al. 2015]. However, targeting Datalog is also challenging because Datalog's expressivity is carefully limited. Datalog programs can only compute finite relations, whereas the typing relation usually is an inductively defined infinite relation. Although this makes compiling type checkers to Datalog seemingly impossible, we have discovered a sequence of systematic transformations that make the resulting inference rules expressible in Datalog.
The first transformation utilizes a new property we call co-functional dependencies. While a functional dependency describes a uniquely determined output, a co-functional dependency describes a uniquely determined input. In particular, for algorithmic type systems, the typing context and other contextual information is co-functionally dependent on the syntax tree. Our transformation exploits this property to factor out the context from the typing relation, making the typing relation computable in Datalog. Unfortunately, the resulting type system won't admit efficient incrementalization, because even a small change to the typing context will affect large parts of the typing derivation. We discovered that we can eliminate this issue by complete deforestation [Wadler 1990] of all typing contexts. Thus, our second transformation is a specialized deforestation of Datalog programs. Our third and final transformation makes sure ill-typed terms do not unnecessarily prune typing derivations. Otherwise, any code change that fixes a type error would entail significant reanalysis. To this end, we developed a reformulation of type systems that separates error handling from computing a type. Our transformation rewrites any algorithmic type checker into one that collects type errors separately from the typing relation. This transformation may well be useful independent of the rest of our work.
Based on our transformations, we developed a domain-specific language (DSL) for type system descriptions that compiles to Datalog. Our compiler implements the three transformations by rewriting inference rules and only lowers those inference rules to Datalog as the last step. Thus, the DSL compiler can be used to simplify type systems independent of Datalog. We have used the DSL to express a wide range of type system features. In addition to PCF with product and sum types, we modeled bi-directional type checking, operator overloading, universal types in the style of System F, and iso-recursive types. We can confirm that all these features can be compiled to Datalog by our transformations and that the resulting Datalog program is incrementally solvable. Effectively, our DSL derives incremental type checkers from textbook-like type system specifications. We also measured the incremental performance of compiled type systems for synthesized PCF programs. We designed a range of change scenarios to challenge the incremental performance. We found that even when large parts of the program are affected by a change, we still deliver updated typing information in at most several tens of milliseconds.
In summary, we make the following contributions: • We analyze the challenges associated with compiling type systems to Datalog (Section 2).
• We introduce co-functional dependencies and define a Datalog transformation that moves co-functionally dependent data into a separate relation (Section 3). • We show how to eliminate typing context propagation from type systems (Section 4).
• We show how to transform a type system to collect type errors on the side (Section 5).
• We implement all three transformations in the compiler of a type systems DSL (Section 6), demonstrate its applicability (Section 7), and benchmark its performance (Section 8).

WHY ARE TYPE SYSTEMS IN DATALOG CHALLENGING?
This paper proposes to incrementalize type checkers by translation to Datalog. Our hypothesis is that such translation can be done systematically and is useful: Existing incremental Datalog solvers provide efficient incremental running times. In the present section, we illustrate why encoding type checkers in Datalog is challenging in the first place. We highlight the challenges while translating a number of exemplary type systems, all using the following syntax: (program) p ::= main e (expression) e ::= unit | x | λx:T . e | e e (type) T ::= Unit | T → T (context) C ::= ε | C, x:T Our motivating examples will only differ in their typing relation but reuse the same syntax. For each typing relation, we show how the type rules can be translated to Datalog and discuss if and how a state-of-the-art incremental Datalog solver could handle them. As such, the current section also presents the required Datalog background.
Challenge 1: Expressions. We start with the typing relation (e : T ) of a very simple type system that only permits unit constants and their application. This type system is not particularly useful but helps us illustrate how to translate a simple type system to Datalog. typed(e,T ) :-?unit(e), !Unit(T ). typed(e,T ) :-?app(e, e 1 , e 2 ), typed(e 1 ,T 1 ), ?Unit(T 1 ), typed(e 2 ,T 2 ), ?Unit(T 2 ), !Unit(T ). ok(p) :-?main(p, e), typed(e,T ). A Datalog program consists of a sequence of rules, each of the form R(t 1 , . . . , t n ) :a 1 , . . . , a m . The rule head R(t 1 , . . . , t n ) declares tuple (t 1 , . . . , t n ) ∈ R if all atoms a 1 , . . . , a m in the rule body hold. Terms t are usually logical variables that are shared between the head and body of a rule. Atoms a query relations R(t 1 , . . . , t n ). This way, relations can depend on each other recursively. In this paper, we use Datalog enriched with algebraic data types in order to model expressions, types, contexts, etc. For each constructor c(x 1 , . . . , x k ) of an algebraic data type, we assume operations !c(y, x 1 , . . . , x k ) and ?c(y, x 1 , . . . , x k ) to construct and deconstruct algebraic data x.
Given this Datalog background, it should be easy to see that (e,T ) ∈ typed if and only if there is a derivation tree for (e : T ) according to the inference rules. We hope to incrementalize type checking (i.e., finding a derivation tree) by applying existing incremental Datalog solvers to the derived Datalog program. To this effect, it is important to know that incremental Datalog solvers evaluate Datalog rules bottom-up, inductively enumerating all derivable tuples. When the input changes, an incremental Datalog solver updates the relations by retracting those tuples no longer derivable and inserting the newly derivable tuples. Unfortunately, this strategy hinges on the Datalog relations being finite. However, our typing relation is infinite, because our example language contains infinitely many well-typed programs: typed = {(unit, Unit), ((unit unit), Unit), (((unit unit) unit), Unit), . . . } Dealing with an infinite language is a standard problem when using Datalog for static analysis. Even Datalog-based analysis systems without incrementalization such as Doop [Smaragdakis and Bravenboer 2010] require finite relations. Fortunately, there is a standard solution that we can employ here as well: Restrict the relations to only consider the user's current program. That is, rather than defining ?unit, ?app, and ?main inductively over all possible programs, we define them as sets of tuples that exactly reflect the user program. Since the user program is finite by construction, we can now evaluate typed bottom-up, enumerating the well-typed subset of the nodes in ?unit, ?app, and ?main. This strategy has been successfully employed in Datalog-based incremental analyzers before [Szabó et al. 2016], such that no further innovation is required for this first challenge. As an example we show how the program on the left is encoded in Datalog as you can see on the right: We use labels such as p and e1 in the Datalog encoding to reference nodes of the abstract syntax tree. The set of tuples ?app contains tuples that represent application nodes. Take for example the tuple (e1, e2, e5) where node e1 is an application node which has e2 and e5 as children. A Datalog solver will derive the following finite relations based on the Datalog rules above and the sets of tuples: Challenge 2: Types. The previous type system is not very useful because it only inhabits the Unit type. We extend this type system by allowing thunks and their application: typed(e,T ) :-?unit(e), !Unit(T ). typed(e,T ) :-?app(e, e 1 , e 2 ), typed(e 1 ,T e ), ?Fun(T e ,T 1 ,T ), ?Unit(T 1 ), typed(e 2 ,T 2 ), ?Unit(T 2 ). typed(e,T ) :-?lam(e, x,T 1 , e 1 ), ?Unit(T 1 ), typed(e 1 ,T 2 ), !Fun(T ,T 1 ,T 2 ). ok(p) :-?main(p, e), typed(e,T ).
Again, we must ask if these rules can be evaluated bottom-up by an incremental Datalog solver. And again this hinges on the Datalog relations being finite. If we assume like above that ?app, ?lam, etc. are constants and only enumerate the user's current program, then only finitely many expressions can occur in typed. Indeed, expressions are not the problem but types are. While the previous type system only considered a single type Unit, this type system associates thunk types of the form T ::= Unit | Unit → T to expressions. Notably, this domain is infinite and relation typed ⊆ e user × T could contain infinitely many tuples even if e user is finite. In truth, typed will only ever contain finitely many tuples. This is because of the functional dependency e T in typed, which means that column T of typed is uniquely determined by column e of typed. That is, if (e,T 1) ∈ typed and (e,T 2) ∈ typed, then T 1 = T 2 [Watt 2018, Chap. 11]. Our type system satisfies the functional dependency e T because it is algorithmic. Consequently, if typed only contains finitely many entries in column e, then typed can also only contain finitely many tuples in e × T . Therefore, typed is finite and incremental bottom-up evaluation succeeds [Ramakrishnan et al. 1987].
It is noteworthy that many (even non-incremental) Datalog solvers would reject the derived Datalog program because it synthesizes data at run time. However, our type system must generate function types !Fun(T ,T 1 ,T 2 ) of arbitrary size to match the nesting level of lambdas in the user's program. The good news is that a few cutting-edge incremental Datalog solvers like IncA [Szabó et al. 2018a] and DDlog [Ryzhyk and Budiu 2019] can handle the derived Datalog code. The bad news is that we must move beyond the cutting edge to support more interesting type systems.
Note that we use !bind in the lam case to extend the context and lookup in the var case to extract a binding from the context. The main program is checked in the !empty context. Unfortunately, our derived Datalog program is not computable in bottom-up style anymore and, thus, cannot be incrementalized by existing Datalog solvers. To see why, let us inspect the var rule in more detail. This rule declares a tuple (C, e,T ) ∈ typed whenever ?var(e, x) and lookup(C, x,T ) hold. As argued above, we can restrict e to range over the user's program only, so that only finitely many variable symbols have to be considered here. But unlike before, e does no longer uniquely determine T because the type also depends on the context C. Therefore, even a single variable x has infinitely many potential typing derivations: As we will show in Section 3, a different encoding of type systems in Datalog can solve this problem. Our solution works for algorithmic type systems and is based on the following observations: (1) Algorithmic type systems do not guess substitutions of metavariables, but require metavariables to be positively bound. In particular, when a judgment typed(C, e,T ) occurs as a premise, the context C is uniquely determined.
(2) Algorithmic type systems are syntax-directed and conduct a fold over the syntax tree. This means that each node in the syntax tree is visited at most once during typing.
Together, these observations entail that each expression is checked under a single, uniquely determined context. We exploit this to factor out the context from relation typed, adding a new relation context(e, C) that associates contexts to expressions. Both relations are finite now. In particular, each variable x in the syntax tree occurs in a unique context context(x, C) and therefore has a unique type typed(x,T ).
Challenge 4: Context propagation. By factoring out the context from relation typed, we obtained a Datalog program that is computable in bottom-up style. Thus, we can apply cutting-edge incremental Datalog solvers like IncA [Szabó et al. 2018a] and DDlog [Ryzhyk and Budiu 2019] to it. Unfortunately, this will yield unsatisfactory incremental performance. In general, an incremental algorithm yields good incremental performance if the size of a change correlates with the time it takes to process that change. Conversely, the update time should be largely independent of the size of the overall input. However, for our derived Datalog code, many small changes in the user program can require a large amount of reanalysis. This problem is due to context propagation.
Consider the following example program, where we use let as syntactic sugar: let id : Unit → Unit = λx:Unit. x in λy:Unit. λz:Unit. e 0 Expression e 0 will be checked in a typing context that binds id , y, and z. Now, if the type of id changes in any way, all previously propagated contexts have to be retracted and new contexts have to be propagated. Specifically, the tuples of relation context(e, C) become obsolete for all expressions e where id is in scope, even for expressions that do not actually refer to id . For declarations with a wide scope, such as top-level functions, this behavior will incur a significant incremental performance penalty. The problem is that the derived Datalog code propagates entire contexts rather than individual context bindings, and that it ignores whether a binding is being used. As we will show in Section 4, we can systematically transform the Datalog code to solve this problem. To do so, we will generate a new relation findBinding(x, e,T ) that finds the bound type of variable x occurring within expression e. This relation will walk the syntax tree in the opposite direction of context propagation until a binder for x is found. Since findBinding does not require a context, we will be able to drop relation context and rewrite the var rule as follows: typed(e,T ) :-?var(e, x), findBinding(x, e,T ).
That is, starting at the reference e, we find the bound type of x. With this change, no context propagation will be necessary anymore.
Challenge 5: Ill-typed terms. Static type systems restrict the syntactically well-formed terms and define a language of well-typed programs. A syntactically well-formed term is well-typed if there is a typing derivation for that term. This is a yes or no decision: in or out. For an algorithmic type system, as soon as any rule fails to satisfy a premise, the entire program is known to be ill-typed and typing can stop right there. However, aborting type checking early is unsatisfactory for Datalog-based incrementality and for programmer feedback.
For Datalog-based incrementality, aborting type checking is unsatisfactory since it prunes tuples from the typing relation unnecessarily. In particular, any typing that transitively depends on an ill-typed term will be dropped from the typing relation typed. For a simple example, consider a term using type ascription (e as T ). If e is ill-typed, e and all its ancestors will be dropped from typed because the type rules require subterms to be well-typed. However, notice how the type of (e as T ) really is independent of the well-typedness of e. We would like to retain (e,T ) ∈ typed, which also allows the ancestors to be checked as usual. As a developer makes changes in quick succession, alternating between a well-typed and an ill-typed program, a more stable typed relation means faster update times.
The second concern with aborting type checking at the first type error is that this is inconvenient in practice. Both compilers and programming editors usually try to report all type errors in the program. In Section 5, we show that the Datalog code can be systematically rewritten to collect all type errors and to avoid pruning the typing relation. To this end, we will generate another relation errors(e, err ) that associates type errors to expressions. A program p then is only well-typed if p ∈ ok and errors = ∅.
Problem Statement. The goal of this paper is to translate algorithmic type systems to Datalog to utilize state-of-the-art incremental Datalog solvers. The translation should be systematic, applicable to a wide range of type systems, and yield good incremental performance. In this section, we identified the following five challenges: Algorithmic Type Systems. In this paper, we assume type systems are given in algorithmic form. Specifically, challenges (C2) and (C3) require an algorithmic formulation. The word algorithmic means that the type system can be trivially translated into a recursive-descent algorithm, but the type system may still be defined using inference-style type rules. Most standard type checkers are naturally algorithmic: Type rules are syntax-directed and metavariables are positively bound. We therefore argue that requiring an algorithmic type system is a modest restriction.
To support our point, note that most textbooks introduce type systems in an algorithmic style, including Harper's Practical Foundations for Programming Languages [Harper 2016] and Pierce's Types and Programming Languages [Pierce 2002]. Hence, novice language designers learn about type systems by being introduced to their algorithmic formulation. Only complex type system features are sometimes given non-algorithmically and require a rewriting. However, the same rewriting is necessary for non-incremental implementations of those type checkers [Grewe et al. 2015], meaning we do not actually impose an additional requirement on type system designers.

TRANSFORMATION 1: CO-FUNCTIONAL DEPENDENCIES
Incremental Datalog solvers evaluate Datalog programs bottom-up. In the previous section, we explained why a naive translation of a type system to Datalog does not permit the application of bottom-up Datalog solvers (Challenge 3): Since contexts occur as a column in the typing relation typed, the typing relation has infinitely many tuples, as we illustrated for the var rule. Our solution to Challenge 3 is based on a property of algorithmic type systems that we discovered and named co-functional dependencies.

Co-Functional Dependencies
Co-functional dependencies express uniqueness relationships between columns of a relation, similar to functional dependencies. Intuitively, a functional dependency describes unique łoutputsž of a relation, whereas a co-functional dependency describes unique łinputsž of a relation. For example, the typing relation of the simply typed lambda calculus (typed ⊆ C × e × T ) has a functional dependency (C × e) T . That is, given C and e, type T is an łoutputž of typing that is uniquely determined by C × e. Our new observation is that the typing relation also has a co-functional dependency e co C. That is, given e, context C is an łinputž of typing that is uniquely determined by e and how typed is used. While the treatment of functional dependencies is standard in databases [Watt 2018, Chap. 11] and Datalog [Ramakrishnan et al. 1987], our notion of co-functional dependencies is novel to the best of our knowledge. Unfortunately, co-functional dependencies are harder to detect and utilize, since they depend on how a relation is being used.
The typing context C of the simply typed lambda calculus is an example of a co-functionally dependent column: Each expression is only checked under a single context. We do not know how to detect co-functional dependencies automatically, but instead rely on domain knowledge about algorithmic type systems. In general, all contextual information passed around in an algorithmic type system is uniquely determined for a syntax-tree node. This is because each syntax-tree node is visited at most once per relation (syntax-directedness), and the relevant context information is unique (no guessing of metavariables). We could in principle also allow multiple visits of the same syntax-tree node as long as relevant context information is identical in all visits. For example, this will allow us to support operator overloading with overlapping inference rules (Section 7).
In the remainder of this paper, we assume functional and co-functional dependencies are declared as part of a relation's signature. To this end, we introduce the following notation for signatures: describes the columns of relation R, its functional dependencies F , and its co-functional dependencies G. Functional and co-functional dependencies are defined based on column indices. For example, we can represent the typing relation of the simply typed lambda calculus by signature (typed : The functional dependency declares that columns 1 and 2 together uniquely determine column 3, that is, C ×e T . The co-functional dependency declares that column 2 also uniquely determines column 1, that is, e co C. Datalog relations annotated this way enable us to utilize co-functional dependencies.
Notation. We frequently need to denote sequences and subsequences in this paper. We write x or x 1 , . . . , x n for a sequence of x elements. Given a set of indices I , we write x I for the subsequence of x consisting of {x i | i ∈ I } and ordered by their index. We leniently write x, y and x I , y and x I , x J to concatenate sequences and sequence elements.

Utilizing Co-Functional Dependencies
A co-functional dependency c co c in relation R stipulates that column c of R is uniquely determined by some other columns c of R. This allows us to factor out c from R, since we can always use the other columns c to uniquely obtain c. However, the rules to obtain c from c are not obvious and depend on how R is being queried. This makes co-functional dependencies difficult to utilize.
We have developed a transformation of Datalog code that factors out co-functionally dependent columns c from their relation R. The key idea is to derive an auxiliary relation π R : c × c that has a (regular) functional dependency c c. Essentially, π R witnesses the contextual uniqueness of c by mapping c to c locally. We then rewrite R to drop column c and to query π R instead. Essentially, if (R(x, c, c) :a) is a rule of R, then (R ′ (x, c) :π R (c, c), a) will be a rule of the rewritten R ′ .
Note how we dropped column C from all rule heads and usages of typed. Instead, we introduced the query π typed (e, C) at the beginning of each typed rule to bind C. For the derived relation π typed : e × C, we generate one rule for each call of typed. Thus, there is no rule for unit because its rule does not call typed, but there are two rules for app. The derived rules reflect how the co-functionally dependent input C was constrained. Essentially, for each call of typed(C, e,T ) we copy the surrounding rule and replace the head with π typed (e, C): π typed (e 1 , C) :-?app(e, e 1 , e 2 ), typed(e 1 ,T e ), ?Fun(T e ,T 1 ,T ), typed(e 2 ,T 1 ), π typed (e, C). π typed (e 2 , C) :-?app(e, e 1 , e 2 ), typed(e 1 ,T e ), ?Fun(T e ,T 1 ,T ), typed(e 2 ,T 1 ), π typed (e, C).
Note how the derived relation finds the co-functional column C of an expression e 1 by querying itself recursively for parent node of e 1 . This way, the derived relation retraces the original context propagation. However, this initial version of π typed only yields a context for e if e is in typed, even though this does not influence which context is returned. To break this dependency, we drop all atoms from π typed that do not contribute to determining the co-functional column. We can also simplify typed, but we may only remove atoms that are infallible (!bind, !empty, π typed ) to preserve ill-typed terms. This yields the following minimal rule set with a clear division of labor: π typed propagates and extends the context, whereas typed does the checking and only mentions the context in the var rule. π typed (e 1 , C) :-?app(e, e 1 , e 2 ), π typed (e, C). π typed (e 2 , C) :-?app(e, e 1 , e 2 ), π typed (e, C). π typed (b, C ′ ) :-?lam(e, x,T 1 , b), !bind(C ′ , C, x,T 1 ), π typed (e, C). π typed (e, C) :-?main(p, e), !empty(C).
It is easy to show by induction that π typed satisfies the functional dependency e C. As we explained for Challenge 2 in Section 2, this is sufficient to ensure the finiteness of π typed . Hence, incremental Datalog solvers can apply their bottom-up evaluation strategy to this Datalog program.

Formalizing Transformation CoFunTrans
We formalize the transformation CoFunTrans that we described informally above. The transformation takes a Datalog program as input and rewrites it to utilize co-functional dependencies. The transformation operates in two steps. First, we revise the signatures of existing relations and add the signatures of derived relations π R . Second, we revise the rules of existing relations and add new rules for derived relations π R .
CoFunTrans signatures. Let Σ be the set of relational signatures of the input Datalog program. Then the rewritten Datalog program has signatures CoFunTransSigs(Σ) defined as follows: CoFunTrans-UpdateSig updates the signatures of existing relations R by dropping all columns codepCols that are co-functionally dependent . The updated signature of R only has columns J of types T J left. The functional dependencies F are updated accordingly and the co-functional dependencies G are dropped entirely. In particular, function deleteShift(F, codepCols) deletes codepCols from the functional dependencies in F and shifts the remaining indices to skip dropped columns. For example, (typed : Rule CoFunTrans-DeriveSig generates a separate signature π R,i for each co-functional dependency I co i of a relation R. Relation π R,i maps columns I of types T I to column i of type T i , as expressed by its functional dependency f . CoFunTrans rules. Let Σ be the set of relational signatures of the input Datalog program and let P be the set of rules of the input Datalog program. Then the rewritten Datalog program has rules CoFunTransRules(Σ, P) defined by the inference rules shown in Figure 2. Rule CoFunTrans-DropCodepArgs defines an auxiliary function ⌊a⌋ on atoms that removes cofunctionally dependent arguments from calls of R. We use this function in the other two rules.

CoFunTrans-DropCodepArgs
Rule CoFunTrans-UpdateRule updates the Datalog rules of existing relations R by making three changes. First, we remove co-functionally dependent columns from the rule head. Second, we insert queries against the newly derived relations π R,i into the body of the rule for each co-functionally dependent column i. Third, we remove co-functionally dependent arguments from calls to other relations in the rule body.
Rule CoFunTrans-DeriveRule generates Datalog rules for the new relations π R,i . Specifically, we generate one Datalog rule for each call of R and each co-functional dependency I co i of relation R. Suppose the call of R occurs in a rule of Q. We derive the new rule by changing the rule of Q in three ways. First, we exchange the rule head since we are only interested in learning how x I determines x i . Second, we adapt the rule body just like CoFunTrans-UpdateRule did: remove co-functionally dependent arguments and insert queries π Q ,j . This yields the body. Third, we slice the resulting (A ∪ Π) to only retain those that contribute to x i . The resulting Datalog program witnesses co-functional dependencies through the derived relations π R,i . Note that the transformation only preserves the semantics of the main relation (e.g. ok), but not the semantics of individual Datalog relations. This is intended as we wanted to restrict typed to become finite. Importantly, we only remove unnecessary tuples from typed such that the main relation is preserved: p ∈ ok if and only if p ∈ CoFunTrans (ok).
Correctness. We formulate precisely under which conditions the transformation is correct and preserves the semantics of the transformed type system. Note that we have not worked out a formal proof of correctness, but rather present the key invariants and properties that ensure correctness.
The formalization assumes a denotational semantics ⟦P⟧ Base for Datalog programs P [Alvarez-Picallo et al. 2019]. The denotational semantics takes a set of base facts Base as input (the extensional database in Datalog lingo) and computes the set of facts Deriv derived by P from Base (yielding the intensional database). Both Base and Deriv consist of ground tuples R(C, . . . , C), where R is a relation name and C are constants. In our work, the base facts describe the user program as we illustrated in Section 2.
Based on the denotational semantics we define the correctness theorem of CoFunTrans. Transformation CoFunTrans is correct because it leads to less derivable tuples, but all relevant tuples are still derivable. Hence, every program that is typeable with the original type system is typeable with the transformed type system. Without loss of generality, we assume there is a relation Main used as the entry point of type checking.
Theorem 1 (Correctness of CoFunTrans). Let Σ be the set of relational signatures of the input Datalog program, let P be the set of rules of the input Datalog program, and let Main be the entry point of the type system. For all base relations Base, Main(x) ∈ ⟦P⟧ Base if and only if Main(x) ∈ ⟦CoFunTransRules(Σ, P)⟧ Base .
To prove this theorem, we need to ensure that the derived π relations correctly capture co-functional dependencies I co i: It uniquely maps x I to x i . That is, we need to ensure that if the original relation R contains a tuple, the derived π relation contains a tuple representing a projection of the tuple according to the co-functional dependency. In addition, we need to ensure that the derived π relations actually describe functional dependencies to guarantee that Datalog bottom-up evaluation succeeds for the transformed Datalog program.
For all base relations Base, if R(x) ∈ ⟦P⟧ Base , then the following propositions hold: ( Lemma 1 is the key property of CoFunTrans required to prove correctness.

TRANSFORMATION 2: CONTEXT FUSION
Transformation CoFunTrans from the previous section makes a Datalog-encoded type system amenable to bottom-up evaluation. It does so by eliminating co-functional dependencies in favor of functional dependencies. For a type system, this means that class tables, typing contexts, and other contextual information is uniquely associated with each expression. While this enabled bottom-up evaluation, it also introduced a new problem: Even a slight change to contextual information will affect all expressions. This is the problem of context propagation we introduced as Challenge 4. Context propagation is problematic whenever the context consists of compound information (e.g., a typing context). When parts of the context are changed (e.g., the type of some variable), the entire context will regarded as changed. This is because incremental Datalog solvers only trace dependencies between relations and propagate inserted and deleted tuples, but they cannot trace changes to individual components of those tuples. Therefore, when the type of a variable changes, all typing contexts that contain that binding change, and thus all tuples that associate these contexts to expressions need updating.
In this section, we present a Datalog transformation that eliminates intermediate compound data. Specifically, we eliminate context information represented as immutable maps, which is produced by the !empty and the !bind constructors and consumed with lookup. Our rewriting can be regarded as a special case of deforestation [Wadler 1990] for immutable maps but for Datalog programs and with support for recursively defined relations. Note also that immutable maps can encode sets as Map[A, Unit] and lists as Map[Int, A], such that our rewriting supports many type system specifications. Nonetheless, our primary motivation was the elimination of intermediate typing contexts, which is why we call the transformation łcontext fusionž.

Context Fusion by Example
Consider again the Datalog rules for the simply typed lambda calculus, as produced by transformation CoFunTrans from the previous section. π typed (e 1 , C) :-?app(e, e 1 , e 2 ), π typed (e, C). π typed (e 2 , C) :-?app(e, e 1 , e 2 ), π typed (e, C). π typed (b, C ′ ) :-?lam(e, x,T 1 , b), !bind(C ′ , C, x,T 1 ), π typed (e, C). π typed (e, C) :-?main(p, e), !empty(C). Our goal is to eliminate the typing context produced by π typed and consumed by lookup in the var rule. Though we consider lookup to be a built-in operation, it can be defined in Datalog as follows: The first rule yields value v if map m starts with a binding for key k. The second rule continues lookup in the rest of the map m ′ if k differs from k ′ .
To eliminate the context, we want to fuse π typed and lookup. Specifically, since relation π typed has a functional dependency e C, it uniquely associates a context to an expression. Thus, instead of performing lookup on the context, can't we derive a specialized lookup relation that operates on the expression directly? Indeed, this is what our second transformation does.
We derive a specialized lookup relation φ typed : e × v × T that finds the binding of a variable v given an expression e. We find bindings by mimicking the rules of π typed , When a !bind occurs in π typed , we inline the definition of lookup to check if we have found the desired entry. For the simply typed lambda calculus we obtain the following rules: . . . . . . typed(e,T ) :-?var(e, x), φ typed (e, x,T ).
For applications, π typed propagated the context of the parent term e. Hence, φ typed continues its search for k in the parent term. For lambdas, π typed yielded an extended context !bind(C ′ , C, x,T 1 ). We inline the definition of lookup and hence obtain two φ typed rules. First, we yield T 1 if the bound variable x is the entry k we are looking for. Second, we continue searching in the parent term if x and k differ. For the main program, π typed yields the empty context !empty(C). Since lookup fails on the empty context, we do not add a rule to φ typed . Consequently, φ typed will fail (as it should) when we reached the root node and have not found a binding.

Formalizing Transformation CtxFusionTrans
We formalize the transformation CtxFusionTrans that we exemplified above. The transformation takes a Datalog program as input and rewrites it to derive and apply find relations φ R . We first derive the new signatures and then update and add rules to the Datalog program.
CtxFusionTrans signatures. Let Σ be the set of relational signatures of the input Datalog program. The rewritten Datalog program has signatures CtxFusionTransSigs(Σ) defined as follows: Rule CtxFusionTrans-DeriveSig generates a signature for the find relations φ R . We generate a separate find relation for each functional dependency I i where column i has a Map type. That is, whenever it is possible to uniquely determine a map from other columns I , we want to find bindings based on I . The find relation uniquely maps values of types T I together with a key of type K to a value of type V , as expressed by the functional dependency f .
Rule CtxFusionTrans-RetainSig merely retains all existing signatures. Usually, it is possible to drop relations that only produce a map since we won't need them after the transformation. For example, we dropped relation π typed in our example from above, using φ typed instead. However, our transformation does not account for this simple post-processing.
CtxFusionTrans rules. Let Σ be the set of relational signatures of the input Datalog program and let P be the set of rules of the input Datalog program. Then the rewritten Datalog program has rules CtxFusionTransRules(Σ, P) defined by the inference rules shown in Figure 3. In computing CtxFusionTransRules(Σ, P), we construct intermediate sets Step z (Σ, P) that contain rules after a z-fold unfolding of the !bind constructor. Note that the unfolding is bounded by the number of syntactic occurrences of !bind in the original rules. Rule CtxFusionTrans-Init derives the initial φ R,i rule for any R that has a functional dependency I i with column i being a Map. Given x I and k, the initial rule uses a 1 , . . . , a m to uniquely obtain x i and then perform a lookup on that. In the subsequent rules, we try to eliminate the invocation of lookup and with it the need for obtaining the map x i explicitly.

CtxFusionTrans-Init
Rules CtxFusionTrans-Unfold and CtxFusionTrans-Bound have the same premises. They check if lookup is invoked on an explicitly constructed map. To this end, we check if any of the atoms a 1 , . . . , a m is an invocation of !bind and if the !bind-constructed map M is used in lookup. We write a 1 , . . . , a m ⊢ x i = M to mean that x i and M unify to the same logic variable under a 1 , . . . , a m , which is decidable in Datalog. If so, we know that the lookup occurs on top of M. We can thus inline lookup. Rule CtxFusionTrans-Unfold captures the case where k k ′ and lookup thus must continue on the rest of the map M ′ . Since the resulting rule still contains lookup, we add the rule to Step z+1 (Σ, P) to allow further transformation. Rule CtxFusionTrans-Bound captures the case where k = k ′ , so that we can yield v = v ′ . Since CtxFusionTrans-Bound fully eliminated the lookup call, we add the resulting rule to the output of the transformation.
Rule CtxFusionTrans-Delegate checks if lookup is invoked on a context obtained from another relation. That is the case if any of the atoms a 1 , . . . , a m is a query Q(y) and the map x i corresponds to y j for some j. Now, if Q has a functional dependency J j and uniquely determines the map y j , then we can use the φ Q ,j relation we created in CtxFusionTrans-DeriveSig for Q. That is, we delegate the search in R and continue searching in Q, which may lead to a (mutually) recursively defined search relation.
Rules CtxFusionTrans-Replace and CtxFusionTrans-Retain propagate the original rules from P. Rule CtxFusionTrans-Replace applies to rules that contain a lookup on a map that is uniquely obtained from relation Q. We replace these lookups by the corresponding search φ Q ,j . Rule CtxFusionTrans-Retain copies over all other rules unchanged.
Note that rules can starve within Step z and never make it to CtxFusionTransRules. This is intended and accounts for the cases where the original lookup would have failed as well. In particular, a lookup on an empty map will not result in a CtxFusionTransRules rule.
Correctness. We formulate a correctness theorem for CtxFusionTrans. This transformation is an optimization and does not affect the derivable tuples in any way. Hence, every tuple that is derivable by the original type system is derivable by the transformed type system.
Theorem 2 (Correctness of CtxFusionTrans). Let Σ be the relational signatures of the input Datalog program, let P be the rules of the input Datalog program, and let (R :T 1 × . . . × T n | F, G) ∈ Σ. For all base relations Base, R(x) ∈ ⟦P⟧ Base if and only if R(x) ∈ ⟦CtxFusionTransRules(Σ, P)⟧ Base .
The only rewriting that changes existing relations is CtxFusionTrans-Replace, which replaces invocations of lookup with invocations of φ. To justify this rewriting, we need to ensure the derived φ relations are correct, that is, they resolve key k to the same value v as lookup. We formulate the following lemma which ensures we can actually replace lookup with the derived φ relations. It states that lookup will resolve key k to the same value v within context x j as the newly derived relation φ Q,j . Note that Q functionally determines the context x j based on x J which in turn will be source arguments of φ Q,j .
This characterizes under which conditions the correctness of CtxFusionTrans is ensured.

Example Revisited
We illustrate the step-wise application of CtxFusionTransRules to the relevant rules of the simply typed lambda calculus.
typed(e,T ) :π typed (e, C), ?var(e, x), φ typed (e, x,T ). A subsequent optimization of the derived rules will remove all invocations of π typed and !bind. This is supported by our implementation and will yield exactly those rules shown in Section 4.1.

Optimizing Search Relations φ R
Our transformation CtxFusionTrans successfully eliminated all intermediate contexts and introduced a bottom-up find function instead. As we will show in our empirical evaluation, the resulting Datalog code yields far superior incremental performance. However, there is one issue we need to take care of first: The derived find relations φ R enumerate all referable bindings, not just those required by actual references.
x Unit 2 x Unit 1 + 2 x Unit 3 x Unit 4 x Unit 3 + 4 x Unit (1 + 2) + (3 + 4) x Unit Consider the example term λx:Unit. (1 + 2) + (3 + 4), where we used additions and numeric literals for convenience. Although this program contains no variable references, φ typed contains all of the entries shown in the table on the right. That is, φ typed contains one entry for each variable and each expression where that variable is in scope. This does not scale very well and it is unneeded.
Indeed it is sufficient to consider variables that are being referenced in an expression. Fortunately, we can derive an optimized version of φ typed by restricting its entries. Specifically, we implemented a simple magic set transformation [Beeri and Ramakrishnan 1991] to derive a helper relation ρ R that restricts φ R to those tuples for which a lookup is needed. In particular, when φ R corresponds to variable lookup, ρ R corresponds to the free variables of an expression. We restrict φ R to those tuples that ρ R considers relevant: φ typed (e 1 , k, v) :ρ typed (e 1 , k), ?app(e, e 1 , e 2 ), φ typed (e, k, v). φ typed (e 2 , k, v) :ρ typed (e 2 , k), ?app(e, e 1 , e 2 ), φ typed (e, k, v).

TRANSFORMATION 3: COLLECTING ERRORS
The traditional formulation of type systems is focused on deciding if a term is well-typed or ill-typed: There either exists a typing derivation or not. However, applications of type systems need more detailed information, namely the reason(s) a typing derivation could not be constructed. In this section, we propose an alternative formulation of type systems that separates finding a term's type from reporting type errors. This allows us (i) to sometimes find a term's type even though there are type errors and (ii) to report multiple type errors for the same term. We present a Datalog transformation that automatically transforms a traditional type system into one with separate error collection. Our transformation is compatible with the previous two transformations from Sections 3 and 4, but it does not require them and can be used independently.

Collecting Errors by Example
We illustrate how our transformation works by considering the simply typed lambda calculus again. However, to showcase that our transformation can be used independently from the other two transformations, we start with the original type rules from Section 2: The construction of a typing derivation fails when premises are unsatisfiable. However, different premises have different purposes and require different error handling. Therefore, we categorize premises as follows: • ReportStuck is the set of relations whose stuckness should result in a type error. We only track the premises occurring in rules of ReportStuck relations. For our example, ReportStuck = {typed, ok}. • For every R ∈ ReportStuck, IgnoreStuck R is the set of relations that should be ignored when they occur as premises. We use IgnoreStuck for those constraints that merely help select the right type rule. For our example, IgnoreStuck typed = {?unit, ?app, ?lam, ?var} and IgnoreStuck ok = {?main}. • Some premises R(x) are known to be infallible and can be ignored during error handling. In our example, !Unity(T ) amongst others will never fail and thus cannot produce a type error.
Based on this categorization, we can systematically derive relations ε typed : C × e × Error and ε ok : p × Error that collect the errors that can occur during type checking: ε typed (C, e, err ) :-?app(e, e 1 , e 2 ), ε typed (C, e 1 , err ). There is no rule for unit because its first premise is in IgnoreStuck typed and its second premise is infallible. For app we obtain three rules. First, if there are type errors in e 1 , we propagate those. We stripped most other premises because they are irrelevant for the recursive call ε typed (C, e 1 , err ). Second, if the type T e of e 1 is not a function type (note the negation ¬ in front of ?Fun), we generate a new error. Third, we propagate the type errors of e 2 . A lam cannot introduce a new error and only propagate type errors from the lambda's body. For var we obtain a new type error when the lookup fails (again note the negation ¬).
Note that the collected type errors are not unique; an expression can have multiple errors. For example, both subterms of an app expression can propagate type errors. The derived ε R relations collect all type errors that occur in the program, which was one of our declared goals.
Our other goal was to find a type despite type errors when possible. To this end, we refine what it means for a term to be well-typed in our encoding: A term is well-typed if we can find its type and there is no type error for it. That is, rather than only requiring (C, e,T ) ∈ typed, we additionally require (C, e, err ) ε typed for any err . This allows us to retain tuples in typed even when an expression contains type errors. Our transformation exploits this to relax the rules of typed: Premises that merely perform a check are discarded. For example, our transformation removes the check on an app's argument e 2 and on the body of main. The other rules are unaffected:

Formalizing Transformation CollectErrorsTrans
We formalize the transformation CollectErrorsTrans that we exemplified above. The transformation takes a Datalog program as input and rewrites it to generate relations ε R and to relax existing relations. The transformation is parametric in the sets ReportStuck and IgnoreStuck R as described above. We first derive the new signatures and then update and add rules to the Datalog program.
CollectErrorsTrans signatures. Let Σ be the set of relational signatures of the input Datalog program. The rewritten Datalog program has signatures CollectErrorsTrans(Σ) defined as follows: The first transformation rule adds new signatures ε R for those relations R that are in ReportStuck.
The new relation has all columns of R except for those that are functionally dependent. For an algorithmic type system this means that the error relation does not track the computed type. In addition to the columns of R, the error relation ε R has a new column of type Error. A tuple (t 1 , . . . , t n , err ) ∈ ε R means that R is stuck for (t 1 , . . . , t n ). The second transformation rule retains the signatures of all existing relations.
CollectErrorsTrans rules. Let Σ be the set of relational signatures of the input Datalog program and let P be the set of rules of the input Datalog program. Then the rewritten Datalog program has rules CollectErrorsTransRules(Σ, P) defined by the inference rules seen in Figure 3.
Rule CollectErrorsTrans-Propagate generates a Datalog rule that propagates errors from subderivations upwards. Given the rule of a relation R ∈ ReportStuck, if R calls another relation Q ∈ ReportStuck, then we want to forward the errors of Q. Thus, we generate a rule for ε R that forwards error err obtained from ε Q . Since we dropped functionally dependent columns from error relations, we select the appropriate variables x J and y K to call ε R and ε Q respectively. Finally, we copy a slice of the other atoms A to the resulting rule, namely those that contribute to the call of (R(x) :a 1 , . . . , a k , Q(y), a k +2 , . . . , a m .) ∈ P A = {a 1 , . . . , a k , a k +2 , . . . , a m } R ∈ ReportStuck Q ∈ ReportStuck (R : ε Q . This slicing is important for correctness. For example, consider a type rule for binary addition e 1 + e 2 . Without slicing, we would get the following error rules amongst others: ε typed (C, e, err ) :-?add(e, e 1 , e 2 ), ε typed (C, e 1 , err ), ?Nat(T 1 ), typed(C, e 2 ,T 2 ), ?Nat(T 2 ). ε typed (C, e, err ) :-?add(e, e 1 , e 2 ), typed(C, e 1 ,T 1 ), ?Nat(T 1 ), ε typed (C, e 2 , err ), ?Nat(T 2 ).
These rules work fine if one of the operands is ill-typed. But if both operands are ill-typed at the same time, neither rule can fire because of the remaining typed constraint on the other operand. Slicing eliminates this problem by discarding those premises that do not help to discover the propagated error.
The second transformation rule CollectErrorsTrans-NewError generates error rules for the origin of a stuck premise. If a relation R ∈ ReportStuck calls another relation Q ReportStuck that is fallible and should not be ignored, then we derive a corresponding error rule. The derived error rule yields a new error description err if ¬Q(y), that is, the premise on Q fails. Like in the previous transformation rule, we use slicing to ensure the error rule can fire.
Transformation rule CollectErrorsTrans-RetainSliced carries out the relaxation of the original rules for R ∈ ReportStuck. Once again we use slicing, this time to drop premises a i that do not contribute to discovering the derivable tuples of R . However, the premises A that were ignored by the error rules may never be relaxed. Transformation rule CollectErrorsTrans-RetainNormal retains all other Datalog rules unchanged.
Correctness. We formulate a correctness theorem for transformation CollectErrorsTrans. This transformation relaxes existing relations and derives error relations to collect stuck derivations instead. That is, all previously derivable tuples are still derivable. In addition, if the original Datalog program will derive a tuple for a relation R marked to report type errors, then there will be no tuple in the corresponding error relation ε R of the transformed Datalog program.
Theorem 3 (Correctness of CollectErrorsTrans). Let Σ be the set of relational signatures of the input Datalog program and P be the set of rules of the input Datalog program. Let (R :T 1 × . . . ×T n | F, G) ∈ Σ and J = {1, . . . , n} \ {i | (I i) ∈ F }. For all base relations Base, R(x) ∈ ⟦P⟧ Base if and only if the two following properties hold: (1) R(x) ∈ ⟦CollectErrorsTransRules(Σ, P)⟧ Base .
To prove this theorem, we need to ensure the error relation ε R only contains errors for tuples that were previously underivable.

Optimizing Error Propagation
The transformation described above generates rules that propagate errors. In general, this propagation is necessary to ensure we recognize a term as ill-typed when a type error occurs in a subterm. But the propagation of errors also induces a performance overhead: If an error occurs deeply nested in a subterm, that error will be associated with the subterm and all its ancestors. Thus, when the programmer introduces or fixes a type error, the corresponding error propagation takes time. We found that for many type systems we can eliminate error propagation. If a type system visits all nodes of the syntax tree, an explicit propagation of errors toward the root is unnecessary. Instead, we can refine well-typedness once more and require all subterms to be free of type errors: p is well-typed if and only if p ∈ ok and (e, err ) ε ok for any subterm e of p and any err . With this definition it is sufficient to find the sources of errors, but it is not necessary to propagate them. We can easily adapt our transformation by removing rule CollectErrorsTrans-Propagate, such that error relations ε R are only filled according to CollectErrorsTrans-NewError. Moreover, the resulting error relations are perfectly suited for programming editors and compilers, which can extract type errors their origin.

IMPLEMENTATION: A TYPE-SYSTEM DSL COMPILED TO DATALOG
We have implemented a domain-specific language (DSL) for describing textbook-like type systems. In our DSL, the programmer can declare arbitrary judgments with mixfix syntax and annotate the sorts to describe the cofunctional and functional dependencies of the judgments. The actual annotations in the DSL are simpler than in the paper, but also slightly less expressive. These judgments can then be used to define type rules. The screenshot on the right shows part of a type system specification as an example of our DSL. We implemented the DSL as a metalanguage in the projectional language workbench MPS. 1 That is, our DSL can be used to define the type system of other languages defined with MPS. We developed a compiler for our DSL that generates Datalog code using the transformations described in this paper. We can target any Datalog dialect that allows Datalog rules to synthesize algebraic data (e.g., to produce function types). However, we will only obtain an incremental checker for those Datalog dialects that have an incremental solver. Specifically, we generate code conforming to the Datalog dialect of IncA [Szabó et al. 2018a[Szabó et al. , 2016, an incremental Datalog-based static analysis framework. Another Datalog dialect our approach can target is DDlog [Ryzhyk and Budiu 2019]. There are a few differences between the transformations in our implementation and the transformations described in the paper: • In our DSL, the premises of type rules are ordered and the judgments declare input-like and output-like columns. We use this information to reason about metavariable bindings. For example, we require metavariable C to be bound before using it in a premise C ⊢ e : T . • In this paper, we introduce the transformations acting on Datalog code, but our compiler actually transforms type system specifications described in our DSL. Only as a last step, the compiler will lower typing rules to the Datalog code. As such, the transformations can be understood to simplify data dependencies within typing rules, which is probably useful for any incrementalization attempt, but maybe even for parallelizing type checking. Additionally, we want to emphasize that the transformations presented in this paper can be useful when implementing type checkers that do not utilize Datalog solvers. The first transformation eliminates the propagation of typing contexts and turns it into a judgment that determines the typing context to consider on demand when a variable reference is encountered. This can enable more fine-grained dependency tracking that can be utilized in other approaches to implement type checkers, including parallelizing it. In combination with the second transformation we avoid the dependencies between intermediate typing context entirely. • Since we can reason about metavariable bindings in the implementation, slicing becomes easier. Where we used slice X (A) in the paper, our implementation can easily decide which atoms A are relevant. • As usual in the type systems literature, but unlike our Datalog encodings, the conclusions of type rules in our DSL express a few syntactic constraints. Usually, these are used to dispatch the current term to the appropriate type rule. By default, our implementation of CollectErrorsTrans uses the constraints found in the conclusion as IgnoreStuck, such that no explicit declaration of IgnoreStuck is required. • In addition to the transformations described in the paper, our implementation can also handle infinite relations with neither functional nor co-functional dependencies. For such relations, our implementation resolves to generating non-incremental Java code that can be invoked from within the Datalog rules. This is reasonable for embedding short yet intractable computations within a larger incremental computation. For example, this extension enabled us to support polymorphic types in our case studies.

CASE STUDIES
We conducted case studies to explore the expressivity of our DSL and of the underlying Datalog transformations. Using our DSL, we specified a range of type systems and compiled them to Datalog. In this section, we provide an overview of type system features we successfully encoded and discuss limitations.
Simple types. We encoded PCF, a simply typed lambda calculus with numeric literals, addition, if-zero, and fix. PCF extends our running example and the specification looks much the same. We also used PCF for benchmarking, which we discuss in Section 8.
Products and sums. To confirm that the DSL and Datalog transformations can handle types for compound data, we modeled product and sum types. The type rules in our DSL closely follow the rules described in Types and Programming Languages [Pierce 2002]. Our compiler translates the extended specification to incrementally executable Datalog code without difficulty. It is reassuring to see that our transformation rules are unchallenged by simple extensions.
Bi-directional type checking. Bi-directional type checking is a form of local type inference. The challenge of bi-directional type checking for our DSL is that there are two mutually recursive typing relations: one for checking and one for inferring types. Our transformations can handle this scenario since we never relied on the recursive structure of the typing relation, and since the underlying Datalog solver can compute mutually recursive Datalog relations. We can thus incrementalize bi-directional type systems.
Overloading. When we introduced co-functional dependencies, we argued that in an algorithmic type system all contextual information is co-functionally dependent on the syntax-tree node. This is because each syntax-tree node is visited at most once per relation (syntax-directedness), and the relevant context information must not be guessed to avoid backtracking. To explore if the type system necessarily has to be algorithmic, we modeled simple operator overloading. Specifically, we added floating-point numbers to PCF such that there are two type rules for the + operator: one for integers and one for floating-point numbers. This type system is not algorithmic, since we have to try out multiple type rules when encountering a + operator. Hence, the question arises whether the typing context is co-functionally dependent nonetheless, or if our transformations fail. As it turns out, overlapping type rules are not an issue for co-functional dependencies as long as all overlapping rules treat the contextual information uniformly. We believe that this usually is the case: The syntactic form governs the threading of contextual information, not the particular type rule applied.
Universal types. We extended PCF with universal types in the style of System F. The main challenge for incrementality and our transformations is the substitution function on types, that the type system uses to instantiate universal types. As a relation, type substitution takes the form tsubst :T × X × T × T for types T and type variables X . This relation is infinite and there are no co-functional dependencies. Therefore, our transformations cannot make this relation compatible with bottom-up evaluation and thus not incremental. In such cases, our implementation falls back to generating non-incremental Java code that is being invoked from within the incremental Datalog code. This is acceptable when only a small portion of the overall computation becomes non-incremental. For universal types, only type substitution is non-incremental, while tree traversal, variable lookups, type propagation, etc. are fully incremental. However, the size of types usually does not grow proportionally with the size of the AST, such that non-incremental type substitution does not endanger the incremental performance. Technically, our incremental Datalog solver selectively reruns non-incremental operations when any of their arguments changes.
Iso-recursive types. We can also support iso-recursive types as introduced in Types and Programming Languages [Pierce 2002]. The typing rules for the fold and unfold expressions depend on type substitution just like universal types. The extension of iso-recursive types does not violate the property of being an algorithmic type system. With this extension and the already supported sum, product and universal types, we can support an expressive functional programming languages type system.
Limitations. We are aware of a few limitations that we want to disclose. First, our DSL currently does not provide support for handling lists, which makes it difficult to encode type system features such as records, variants, or functions with multiple parameters. This is a DSL limitation, not a limitation of our approach of generating incremental Datalog programs. Second, since type substitution is difficult to incrementalize (see universal types), unification is difficult to incrementalize. Therefore, it is not clear if type systems with Hindley-Milner type inference can be supported by our approach. Third, as of right now our approach does not support dependent types. In order to support dependent types our approach needs to be extended such that it can translate operational semantics to Datalog. As a first experiment we were able to encode an interpreter for PCF in the Datalog dialect IncA which enables us to incrementalize operational semantics. Hence, it is possible to describe an type checker supporting dependent types in Datalog. Lastly, we investigated if our approach can support languages with nominal subtyping. Like type substitution, subtyping is an infinite relation without co-functional dependencies, and we must resolve to generating non-incremental Java code. However, nominal subtyping is not self-contained and requires access to the class table of the program in order to decide C <: D. This induces additional constraints on when to rerun a subtype check, which we cannot currently trace.

PERFORMANCE EVALUATION
We present a preliminary performance evaluation of our approach using a type checker for PCF and synthesized subject programs. Our goal is to assess the incremental performance of our approach, and to examine that impact of our transformation steps on the performance. We compare to a non-incremental recursive descent type checker written in Java.
We synthesize two PCF programs Star and Chain that have intricate dependencies and challenge our incremental approach. Star consists of n functions all calling f 0 . Chain consists of n functions each calling f n−1 . These programs allow us to introduce changes with global effect on type checking. Star: Chain: in 1 + f n (1) We generate small IDE-style program changes (as opposed to larger commit-style changes) for our evaluation. Our changes are local and only affect a single subterm. We change the program by deleting and inserting tuples into the sets of tuples that describe the program, but only those that are directly affected by the change. The incremental Datalog solver will make sure to propagate those deletions and insertions as to update all derived tuples. To stress-test our approach, we always apply changes to f 0 , which all other functions (transitively) depend on. We consider the following 6 kind of changes and their inverse undo changes: • Num: Increment the value of a numeric literal by 1.
• Ref : Change a variable reference to an unbound name.
• Param: Change the parameter name of a lambda abstraction.
• Anno: Change the type annotation of a lambda abstraction.
• Lambda: Insert a lambda abstraction in the body of an existing lambda abstraction.
• AddApp: Change an addition to an application while retaining the original operands.
Note that, except for Num, all of the above changes will result in an ill-typed program. We believe this realistically reflects programming sessions, where a developer changes one piece at a time.
We consider 4 type checker implementations: • B: baseline type checker, non-incremental, written as a recursive Java function.
For the measurements, we synthesize subject programs Star and Chain with n = 200. We apply each change and its undo 40 times after warmup. We measure the initial analysis time and the time Results. Figure 4 shows a summary of our measurement results. First, let us discuss the performance of the final transformation stage T1+T2+T3 that our DSL uses and compare it to the non-incremental baseline type checker. We observe that the incremental update times are really fast; they are at most several tens of milliseconds, which is exactly what we expect from a type checker running in an IDE. The initialization time is at most a second, which we consider acceptable, as this is a one-time cost. The run time of the baseline analysis is also fast. This is not surprising because our subject programs are small. However, incrementalization brings significant performance gains most of the time compared to the baseline version. For example, for Num, Ref, and Param changes we see multiple orders of magnitude speedups. We also see slowdowns in certain cases: For the Star program the Anno, Lambda, and AddApp changes induce an order of magnitude slowdown. This is due to the global effect these changes have on the program, which our incremental analysis has to retrace. But even in these cases, the incremental running times are still much faster than the initial run of our analysis. In future work, we will try to speed up the initial analysis run, which should improve the performance for changes with global effect.
Let us now examine the effect of our transformations on the performance. For CtxFusionTrans (T2), the Chain program is interesting because it requires a long threading of typing contexts. When we change the type of f 0 (changes Param and Anno), all threaded contexts become invalid. However, for changes Lambda and AddApp we can observe a negative effect of CtxFusionTrans. This is because those changes eliminate the binding of f 0 altogether, since its definition becomes ill-typed. Transformation CollectErrorsTrans (T3) recovers these losses. Indeed, CollectErrorsTrans (T3) induces a significant speedup most of the time. This is because error collection makes the entire typeOf relation more resilient to changes. That is, the type checker can endure ill-typed terms and reuse the tuples in the relation more frequently. As it turns out, this separation of type inference and error collection is key to fast incremental type checking.
Given that incrementalization comes with extensive caching, we also benchmarked the memory overhead of our type checkers. We found that on average the memory overhead is around 10 MB, which is a negligible value compared to the 2 GB memory consumption of the IDE itself.
To summarize, we find that the incremental performance of our type checker is suitable for applications in IDEs. We often achieve order-of-magnitude speedups compared to the non-incremental baseline analysis. We pay the price for this with occasional slowdowns in update times and longer initialization time. The memory overhead of our approach is negligible for the synthesized programs.

RELATED WORK
IncA [Szabó et al. 2016] is an incremental static analysis framework based on Datalog. We use IncA in our work as the incremental evaluation engine for the Datalog code we generate. Specifically, we show how to systematically construct type checkers that can then be automatically incrementalized by IncA. IncA has been shown previously to deliver fast incremental updates for a range of program analyses: FindBugs-style linting, control-flow analysis [Szabó et al. 2016], data-flow analyses [Szabó et al. 2018a], and overload resolution [Szabó et al. 2018b]. This paper is the first to generate IncA code from high-level specifications.
Typol [Despeyroux 1984] translates inference rules to Prolog. In contrast to Datalog, Prolog is a Turing-complete language and supports infinite relations that are explored on-demand through top-down evaluation. The same holds for other works such as [Farka et al. 2018;Franceschini et al. 2016] which compile to first-order Horn clauses where infinte relations are allowed. Thus, we face the more difficult challenges of translating inference rules into a style that permits the bottom-up evaluation of logic programs. Attali et al. [1992] implemented an incremental evaluator for Typol programs. However, for fast incremental update times, the context is not allowed to change. If the context changes in any way, type checking has to be started from scratch for the affected expressions. In contrast, we derive a Datalog program that is resilient to such changes. Wachsmuth et al. [2013] propose a task engine for incremental name and type analysis. Tasks tend to be small and inter-dependent, encoding fine-grained dependencies. When a file changes, they (re)generate tasks for the entire file. Task evaluation relies on a cache of previous task results, only recomputing tasks that are new. If a change affects a task, its cache entry is invalidated and the task reevaluated. The task engine then triggers the reevaluation of all transitively dependent tasks. In contrast to this specialized approach, we rely on a generic incremental compilation target, namely Datalog. The transformations we presented in this paper enable us to handle type systems based on standard typing rules, whereas the task engine requires language-specific rules for task generation.  introduce a co-contextual formulation of type checking. Similar to our approach, co-contextual type checking eliminates context propagation. However, while we synthesize a find relation to lookup bindings as needed, co-contextual type checkers propagate lookup constraints when encountering a variable. This makes co-contextual type checkers compositional, allowing subderivations to be reused even when context information changes. The caveat of cocontextual type checking is that incremental performance heavily relies on constraints being locally solved in the subderivations, which often is not the case [Kuci et al. 2017]. In our solution, we use Datalog's dependency tracking instead of trying to fit dependencies into a compositional structure.
The work on incremental type checking for the programming language B [Meertens 1983] decorates the syntax tree with the type requirements known for a specific node. When changing a node in the syntax tree, the decorated node is deleted which is followed by inserting the newly decorated node while reusing the decorated children of the deleted node. This technique only works because B does not support type declarations for variables but infers the type by discovering type requirements based on the usage of the variable. Hence, the type system of B does not require top-down context propagation, which we support by utilizing co-functional dependencies. As our case studies indicate, our approach is applicable to many type systems. Busi et al. [2019] propose to incrementalize type checking by deriving type rules that utilize memoization. This allows the reuse of parts of the typing derivation when code changes occur. However, as soon as any part of the context or the expression is changed, the entire subderivation has to be reconstructed. Our approach uses much more fine-grained dependency tracking. In particular, our second transformation enables us to track individual bindings rather than entire contexts, which our evaluation confirmed to be essential for incremental type checking.
Datafun [Arntzenius and Krishnaswami 2020] is a higher-order functional language that incorporates Datalog's semi-naive bottom-up evaluation. While Datafun does not aim for incrementality, it would be interesting to see if our transformations can expand the expressivity of Datafun. Specifically, it would be interesting to demonstrate that the bottom-up computable Datalog code we generate indeed is admitted by Datafun's type system. Their type system enforces monotonicity constraints that our Datalog solver relies on, too.
The transformation we presented in Section 3 has a strong resemblance with magic set transformations [Beeri and Ramakrishnan 1991], which are well-known in the Datalog community. Like our transformation, a magic set transformation rewrites a Datalog program to eliminate the derivation of irrelevant (unquerried) tuples. Traditionally, magic set transformations are used as an optimization that may filter some or all irrelevant tuples, and usually the original Datalog program is already computable (has finite relations). In contrast, we start with an incomputable Datalog program (infinite relations). Therefore, we developed a specialized transformation that exploits the new concept of co-functional dependencies. Our specialized transformation allows us to guarantee all irrelevant tuples are eliminated and that the typing relation becomes finite. Additionally, our transformation can exploit co-functional dependencies to avoid the generation of additional auxiliary relations that traditional magic set transformations would require.
Deforestation [Wadler 1990] is a technique to avoid intermediate immutable data structures that are produced and immediately consumed. The context fusion transformation of Section 4 follows the same idea. Instead of constructing intermediate maps (e.g. typing contexts) and letting the built-in lookup relation consume them, we directly perform lookup on the data that functionally determines the map that is passed to lookup. The consumer is fixed (lookup) in our approach, but every relation that functionally determines a map is viable as a producer. Our technique is applicable to recursive Datalog programs while deforestation is an optimization technique for functional programs.

CONCLUSION
We proposed a novel approach to systematically deriving incremental type checkers based on textbook-style type rules. Our solution is divided into three different transformations. The first transformation utilizes co-functional dependencies to translate type rules to Datalog such that bottom-up evaluation succeeds. The second transformation eliminate dependencies on compound data such as typing contexts to achieve more efficient incremental performance. And the third transformation separates the error collection from the type rules, which is interesting even outside of this work. While our transformations primarily tackle issues with incremental name bindings and type errors, we showcased that our transformations effectively support a wide range of type system features such as sum and product types, overloading, universal types, iso-recursive types, and bi-directional type checking. Further, we performed a preliminary performance evaluation to demonstrate that the derived type checkers indeed achieve fast incremental update times.