Abstract

Typed Clojure is an optional type system for the Clojure programming language that aims to type check idiomatic Clojure code. This dissertation presents the design of Typed Clojure, formalizes Typed Clojure’s underlying theory, studies its effectiveness in real-world code bases, and proposes several extensions to help address its shortcomings.

I develop a formal model of Typed Clojure that includes key features like hash-maps, multimethods, Java interoperability, and occurrence typing, and prove the model type sound. Then, I demonstrate that Typed Clojure’s design is useful and corresponds to actual usage patterns with an empirical study of real-world Typed Clojure usage in over 19,000 lines of code. This experience also revealed several usability shortcomings in Typed Clojure.

First, the top-level annotation burden needed to port untyped code is prohibitively high. We present an automatic annotator for Typed Clojure to ease this burden, using runtime observations to synthesize heterogeneous, recursive type annotations. We evaluate our experience using the annotator by porting several open-source projects.

Second, pre-expanding macros before type checking makes type checking brittle. We describe and implement a new analyzer for Clojure code that can provide the foundation of an alternative approach where the user provides custom type rules for macros.

Third, too many local functions require annotations. We present a hybrid approach of symbolic execution and type checking that helps check some common higher-order Clojure idioms.

Acknowledgements

I first touched down in Bloomington ready to start my graduate career—that is, until my puzzled cab driver Juannita informed me with a gasp we were in Bloomington, Illinois. She kindly agreed to drive me to IU, a 12-hour roundtrip—a humbling start to graduate school. The next day, reconnecting with Dan Friedman and the inspirational Will Byrd came full circle. Thanks Jason Hemann, Cam & Rebecca Swords, Jaime Guerrero, and Tori Vollmer for helping me find my feet.

Since then, Andrew Kent and I have done most things together, like deciphering set-theoretic types, floating down a Eugene river, weekly Zelda gaming, and dissertating. Andrew and his delightful family took me under their wing—thanks Carrie, Charlotte, Harrison, Sydney, and Dwight.

Thanks to my donators, talk attendees, and users, including Chas Emerick, Brandon Bloom, David Nolen, Ghadi Shayban, Nicola Mometto, Devin Walters, Reid McKenzie, Nathan Sorenson, Eric Normand, Craig Andera, Jim Duey, Kyle Kingsbury, Colin Fleming, Paula Gearon, Nikko Patten, and Claire Alvis who were very encouraging. CircleCI enabled discussion of Typed Clojure “in practice,” and their post-mortem summarized my frustrations with Typed Clojure.

Sam taught me how (and when) to turn my implementations into research. He has been supportive, trusting, and always game to clarify my bizarre ideas. Mike Vollmer helped brainstorm the annotator; I’m grateful for Mike’s presense and support. I fondly remember our conversations, nagivating Mumbai together, and bad-movie nights. The annotator took shape at weekly meetings—thanks Matteo Cimini, Rajan Walia, Spenser Bauman, Jeremy Siek, Mike Vitousek, Deyaaeldeen Almahallawi, Caner Derici, Sarah Spall, and David Christiansen for your attention and suggestions.

Symbolic closures were the result of many conversations. Andre Kuhlenschmidt’s interest in them during my final PL Wonks talk helped me through the last weeks before my defense. Thanks to Wonks regulars Ryan Scott, Kyle Carter, Vikraman Choudhury, Matthew Heimerdinger, Paulette Koronkevich, Aaron Hsu, Praveen Narayanan, and Chaitanya Koparkar for your engagement.

Thanks to my committee Ryan, Larry, and Ken for your feedback. I found Ryan’s compilers course and Larry’s logic course invigorating, and I’m grateful to Ken for always asking the right questions.

Thanks to my friends and family, especially Mum, Dad, and Aaron. Having a partner with experience in Computer Science research has been wonderful, and my wife Marcela Poffald is my greatest advocate. Her feedback has improved and clarified my work, and her continuous requests to be referred to as “Mrs. Typed Clojure” with a matching cap never fail to make me blush.

Contents

Chapter 1
Introduction

1.1 My Thesis

Typed Clojure is a sound and practical optional type system for Clojure.

1.2 Structure of this Dissertation

This document progresses in several parts that support my thesis statement.

Part I motivates and presents the design of Typed Clojure. It addresses both parts of my thesis statement.

• Typed Clojure is sound I formalize Typed Clojure, including its characteristic features like hash-maps, multimethods, and Java interoperability, and prove the model type sound.
• Typed Clojure is practical I present an empirical study of real-world Typed Clojure usage in over 19,000 lines of code, showing its features correspond to actual usage patterns.

The results and industry feedback of this work inspired three distinct research directions to help improve the experience of using Typed Clojure.

• Part II presents a solution to lower the annotation burden in real-world Typed Clojure programs. I formalize and implement a tool to automatically annotate types for top-level user and library definitions, and empirically study the manual changes needed for the generated annotations to pass type checking.
• Part III describes the design and implementation of a new code analyzer for Clojure, in service of enabling user-provided type rules for Clojure macros to help make type checking complex macro usages more robust.
• Part IV motivates and describes symbolic closure types, a technique that enhances type checking with symbolic execution, that helps check some common Clojure idioms via a compatible extension of Typed Clojure’s original design.

Finally, Part V presents the related work and future directions for each part.

1.3 Previously Published Work

Part I has been published:

• Ambrose Bonnaire-Sergeant, Rowan Davies, and Sam Tobin-Hochstadt. Practical Optional Types for Clojure. In Proceedings of the 25th European Symposium on Programming, 2016. (ESOP ’16)

Part II is in submission:

• Ambrose Bonnaire-Sergeant, and Sam Tobin-Hochstadt. Squash the work: A Workflow for Typing Untyped Programs that use Ad-Hoc Data Structures. In Submission

Part I
Practical Optional Types for Clojure

Chapter 2
Abstract

Typed Clojure is an optional type system for Clojure, a dynamic language in the Lisp family that targets the JVM. Typed Clojure enables Clojure programmers to gain greater confidence in the correctness of their code via static type checking while remaining in the Clojure world, and has acquired significant adoption in the Clojure community. Typed Clojure repurposes Typed Racket’s occurrence typing, an approach to statically reasoning about predicate tests, and also includes several new type system features to handle existing Clojure idioms.

In this part, we describe Typed Clojure and present these type system extensions, focusing on three features widely used in Clojure. First, multimethods provide extensible operations, and their Clojure semantics turns out to have a surprising synergy with the underlying occurrence typing framework. Second, Java interoperability is central to Clojure’s mission but introduces challenges such as ubiquitous null; Typed Clojure handles Java interoperability while ensuring the absence of null-pointer exceptions in typed programs. Third, Clojure programmers idiomatically use immutable dictionaries for data structures; Typed Clojure handles this with multiple forms of heterogeneous dictionary types.

We provide a formal model of the Typed Clojure type system incorporating these and other features, with a proof of soundness. Additionally, Typed Clojure is now in use by numerous corporations and developers working with Clojure, and we present a quantitative analysis on the use of type system features in two substantial code bases.

Chapter 3
Background: Clojure with static typing

The popularity of dynamically-typed languages in software development, combined with a recognition that types often improve programmer productivity, software reliability, and performance, has led to the recent development of a wide variety of optional and gradual type systems aimed at checking existing programs written in existing languages. These include TypeScript [77] and Flow [31] for JavaScript, Hack [35] for PHP, and mypy [52] for Python among the optional systems, and Typed Racket [76], Reticulated Python [78], and Gradualtalk [1] among gradually-typed systems.¹

One key lesson of these systems, indeed a lesson known to early developers of optional type systems such as Strongtalk, is that type systems for existing languages must be designed to work with the features and idioms of the target language. Often this takes the form of a core language, be it of functions or classes and objects, together with extensions to handle distinctive language features.

We synthesize these lessons to present Typed Clojure, an optional type system for Clojure. Clojure is a dynamically typed language in the Lisp family—built on the Java Virtual Machine (JVM)—which has recently gained popularity as an alternative JVM language. It offers the flexibility of a Lisp dialect, including macros, emphasizes a functional style via immutable data structures, and provides interoperability with existing Java code, allowing programmers to use existing Java libraries without leaving Clojure. Since its initial release in 2007, Clojure has been widely adopted for “backend” development in places where its support for parallelism, functional programming, and Lisp-influenced abstraction is desired on the JVM. As a result, there is an extensive base of existing untyped programs whose developers can benefit from Typed Clojure, an experience we discuss in this paper.

Since Clojure is a language in the Lisp family, we apply the lessons of Typed Racket, an existing gradual type system for Racket, to the core of Typed Clojure, consisting of an extended λ-calculus over a variety of base types shared between all Lisp systems. Furthermore, Typed Racket’s occurrence typing has proved necessary for type checking realistic Clojure programs.

However, Clojure goes beyond Racket in many ways, requiring several new type system features which we detail in this paper. Most significantly, Clojure supports, and Clojure developers use, multimethods to structure their code in extensible fashion. Furthermore, since Clojure is an untyped language, dispatch within multimethods is determined by application of dynamic predicates to argument values. Fortunately, the dynamic dispatch used by multimethods has surprising symmetry with the conditional dispatch handled by occurrence typing. Typed Clojure is therefore able to effectively handle complex and highly dynamic dispatch as present in existing Clojure programs.

But multimethods are not the only Clojure feature crucial to type checking existing programs. As a language built on the Java Virtual Machine, Clojure provides flexible and transparent access to existing Java libraries, and Clojure/Java interoperation is found in almost every significant Clojure code base. Typed Clojure therefore builds in an understanding of the Java type system and handles interoperation appropriately. Notably, null is a distinct type in Typed Clojure, designed to automatically rule out null-pointer exceptions.

An example of these features is given in Figure 3.1. Here, the pname multimethod dispatches on the class of the argument—for Strings, the first method implementation is called, for Files, the second. The String method calls a File constructor, returning a non-nil File instance—the getName method on File requires a non-nil target, returning a nilable type.

Finally, flexible, high-performance immutable dictionaries are the most common Clojure data structure. Simply treating them as uniformly-typed key-value mappings would be insufficient for existing programs and programming styles. Instead, Typed Clojure provides a flexible heterogenous map type, in which specific entries can be specified.

While these features may seem disparate, they are unified in important ways. First, they leverage the type system mechanisms inherited from Typed Racket—multimethods when using dispatch via predicates, Java interoperation for handling null tests, and heterogenous maps using union types and reasoning about subcomponents of data. Second, they are crucial features for handling Clojure code in practice. Typed Clojure’s use in real Clojure deployments would not be possible without effective handling of these three Clojure features.

3.1 Contributions

Our main contributions are as follows:

1.

We motivate and describe Typed Clojure, an optional type system for Clojure that understands existing Clojure idioms.

2.

We present a sound formal model for three crucial type system features: multi-methods, Java interoperability, and heterogenous maps.

3.

We evaluate the use of Typed Clojure features on existing Typed Clojure code, including both open source and in-house systems.

The remainder of this part begins with an example-driven presentation of the main type system features in Section 4. We then incrementally present a core calculus for Typed Clojure covering all of these features together in Section 5 and prove type soundness (Section 6). We then present an empirical analysis of significant code bases written in core.typed—the full implementation of Typed Clojure—in Section 7. Finally, we discuss related work and conclude.

Chapter 4
Overview of Typed Clojure

We now begin a tour of the central features of Typed Clojure, beginning with Clojure itself. Our presentation uses the full Typed Clojure system to illustrate key type system ideas,¹ before studying the core features in detail in Section 5.

4.1 Clojure

Clojure [44] is a Lisp that runs on the Java Virtual Machine with support for concurrent programming and immutable data structures in a mostly-functional style. Clojure provides easy interoperation with existing Java libraries, with Java values being like any other Clojure value. However, this smooth interoperability comes at the cost of pervasive null, which leads to the possibility of null pointer exceptions—a drawback we address in Typed Clojure.

4.2 Typed Clojure

A simple one-argument function greet is annotated with ann to take and return strings.

Providing nil (exactly Java’s null) is a static type error—nil is not a string.

Unions To allow nil, we use ad-hoc unions (nil and false are logically false).

Typed Clojure prevents well-typed code from dereferencing nil.

Flow analysis Occurrence typing [75] models type-based control flow. In greetings, a branch ensures repeat is never passed nil.

Removing the branch is a static type error—repeat cannot be passed nil.

4.3 Java interoperability

Clojure can interact with Java constructors, methods, and fields. This program calls the getParent on a constructed File instance, returning a nullable string.

Example 1

Typed Clojure can integrate with the Clojure compiler to avoid expensive reflective calls like getParent, however if a specific overload cannot be found based on the surrounding static context, a type error is thrown.

Function arguments default to Any, which is similar to a union of all types. Ascribing a parameter type allows Typed Clojure to find a specific method.

Example 2

The conditional guards from dereferencing nil, and—as before—removing it is a static type error, as typed code could possibly dereference nil.

Typed Clojure rejects programs that assume methods cannot return nil.

Method targets can never be nil. Typed Clojure also prevents passing nil as Java method or constructor arguments by default—this restriction can be adjusted per method.

In contrast, JVM invariants guarantee constructors return non-null.²

Example 3

4.4 Multimethods

Multimethods are a kind of extensible function—combining a dispatch function with one or more methods—widely used to define Clojure operations.

Value-based dispatch This simple multimethod takes a keyword (Kw) and says hello in different languages.

Example 4

When invoked, the arguments are first supplied to the dispatch function—identity—yielding a dispatch value. A method is then chosen based on the dispatch value, to which the arguments are then passed to return a value.

For example, (hi :en) evaluates to "hello"—it executes the :en method because

• (= (identity :en):en) is true and
• (= (identity :en):fr) is false.

Dispatching based on literal values enables certain forms of method definition, but this is only part of the story for multimethod dispatch.

Class-based dispatch For class values, multimethods can choose methods based on subclassing relationships. Recall the multimethod from Figure 3.1. The dispatch function class dictates whether the String or File method is chosen. The multimethod dispatch rules use isa?, a hybrid predicate which is both a subclassing check for classes and an equality check for other values.

The current dispatch value and—in turn—each method’s associated dispatch value is supplied to isa?. If exactly one method returns true, it is chosen. For example, (pname "STAINS/JELLY") picks the String method because (isa? String String) is true, and (isa? String File) is not.

4.5 Heterogeneous hash-maps

The most common way to represent compound data in Clojure are immutable hash-maps, typicially with keyword keys. Keywords double as functions that look themselves up in a map, or return nil if absent.

Example 5

HMap types describe the most common usages of keyword-keyed maps.

This says :en and :fr are known entries mapped to strings, and the map is fully specified—that is, no other entries exist—by :complete? being true. HMap types default to partial specification. '{:en Str :fr Str} abbreviates: (HMap :mandatory :en Str, :fr Str).

Example 6

HMaps in practice The next example is extracted from a production system at CircleCI, a company with a large production Typed Clojure system (Section 7.2 presents a case study and empirical result from this code base).

As EncKeyPair is fully specified, we remove extra keys like :priv via dissoc, which returns a new map that is the first argument without the entry named by the second argument. Notice removing dissoc causes a type error.

4.6 HMaps and multimethods, joined at the hip

HMaps and multimethods are the primary ways for representing and dispatching on data respectively, and so are intrinsically linked. As type system designers, we must search for a compositional approach that can anticipate any combination of these features.

Thankfully, occurrence typing, originally designed for reasoning about if tests, provides the compositional approach we need. By extending the system with a handful of rules based on HMaps and other functions, we can automatically cover both easy cases and those that compose rules in arbitrary ways.

Futhermore, this approach extends to multimethod dispatch by reusing occurrence typing’s approach to conditionals and encoding a small number of rules to handle the isa?-based dispatch. In practice, conditional-based control flow typing extends to multimethod dispatch, and vice-versa.

We first demonstrate a very common, simple dispatch style, then move on to deeper structural dispatching where occurrence typing’s compositionality shines.

HMaps and unions Partially specified HMap’s with a common dispatch key combine naturally with ad-hoc unions. An Order is one of three kinds of HMaps.

The :Meal entry is common to each HMap, always mapped to a known keyword singleton type. It’s natural to dispatch on the class of an instance—it’s similarly natural to dispatch on a known entry like :Meal.

The :combo method is verified to only structurally recur on Orders. This is achieved because we learn the argument o must be of type '{:Meal ':combo} since (isa? (:Meal o):combo) is true. Combining this with the fact that o is an Order eliminates possibility of :lunch and :dinner orders, simplifying o to '{:Meal ':combo :meal1 Order :meal2 Order} which contains appropriate arguments for both recursive calls.

Nested dispatch A more exotic dispatch mechanism for desserts might be on the class of the :desserts key. If the result is a number, then we know the :desserts key is a number, otherwise the input is a :combo meal. We have already seen dispatch on class and on keywords in isolation—occurrence typing automatically understands control flow that combines its simple building blocks.

The first method has dispatch value Long, a subtype of Int, and the second method has nil, the sentinel value for a failed map lookup. In practice, :lunch and :dinner meals will dispatch to the Long method, but Typed Clojure infers a slightly more general type due to the definition of :combo meals.

In the Long method, Typed Clojure learns that its argument is at least of type '{:desserts Long}, since (isa? (class (:desserts o))Long) must be true. Here the :desserts entry must be present and mapped to a Long—even in a :combo meal, which does not specify :desserts as present or absent.

In the nil method, (isa? (class (:desserts o))nil) must be true—which implies (class (:desserts o)) is nil. Since lookups on missing keys return nil, either

• o maps the :desserts entry to nil, like the value {:desserts nil}, or
• o is missing a :desserts entry.

We can express this type with the :absent-keys HMap option

This eliminates non-:combo meals since their '{:desserts Int} type does not agree with this new information (because :desserts is neither nil or absent).

From multiple to arbitrary dispatch Clojure multimethod dispatch, and Typed Clojure’s handling of it, goes even further, supporting dispatch on multiple arguments via vectors. Dispatch on multiple arguments is beyond the scope of this paper, but the same intuition applies—adding support for multiple dispatch admits arbitrary combinations and nestings of it and previous dispatch rules.

Chapter 5
A Formal Model of λTC

After demonstrating the core features of Typed Clojure, we link them together in a formal model called λTC. Building on occurrence typing, we incrementally add each novel feature of Typed Clojure to the formalism, interleaving presentation of syntax, typing rules, operational semantics, and subtyping.

5.1 Core type system

We start with a review of occurrence typing [75], the foundation of λTC.

Expressions Syntax is given in Figure 5.1. Expressions e include variables x, values v, applications, abstractions, conditionals, and let expressions. All binding forms introduce fresh variables—a subtle but important point since our type environments are not simply dictionaries. Values include booleans b, nil, class literals C, keywords k, integers n, constants c, and strings s. Lexical closures [ρ,λxτ.e]c close value environments ρ—which map bindings to values—over functions.

Types Types σ or τ include the top type ⊤, untagged unions (⋃  ), singletons (Vall), and class instances C. We abbreviate the classes Boolean to B, Keyword to K, Nat to N, String to S, and File to F. We also abbreviate the types (⋃ ) to ⊥, (Val nil) to nil, (Val true) to true, and (Val false) to false. The difference between the types (ValC) and C is subtle. The former is inhabited by class literals like K and the result of (class :a)—the latter by instances of classes, like a keyword literal :a, an instance of the type K. Function types x:στ contain latent (terminology from [55]) propositions ψ, object o, and return type τ, which may refer to the function argument x. They are instantiated with the actual object of the argument in applications.

Objects Each expression is associated with a symbolic representation called an object. For example, variable m has object m; (class(:lunch m)) has object class(key:lunch(m)); and 42 has the empty object ∅ since it is unimportant in our system. Figure 5.1 gives the syntax for objects o—non-empty objects π(x) combine of a root variable x and a path π, which consists of a possibly-empty sequence of path elements (pe) applied right-to-left from the root variable. We use two path elements—class and key k—representing the results of calling class and looking up a keyword k, respectively.

Propositions with a logical system In standard type systems, association lists often track the types of variables, like in LC-Let and LC-Local.

Occurrence typing instead pairs logical formulas, that can reason about arbitrary non-empty objects, with a proof system. The logical statement σx says variable x is of type σ.

We further extend logical statements to propositional logic. Figure 5.1 describes the syntax for propositions ψ, consisting of positive and negative type propositions about non-empty objects—τπ(x) and τπ(x) respectively—the latter pronounced “the object π(x) is not of type τ”. The other propositions are standard logical connectives: implications, conjunctions, disjunctions, and the trivial (tt) and impossible (ff) propositions. The full proof system judgement Γ ⊢ ψ says proposition environment Γ proves proposition ψ.

Each expression is associated with two propositions—when expression e1 is in test position like (if e1 e2 e3), the type system extracts e1’s ‘then’ and ‘else’ proposition to check e2 and e3 respectively. For example, in (if o e2 e3) we learn variable o is true in e2 via o’s ‘then’ proposition (∪ nil false)o, and that o is false in e3 via o’s ‘else’ proposition (∪ nil false)o.

To illustrate, recall Example 8. The parameter o is of type Order, written Ordero as a proposition. In the :combo method, we know (:Meal o) is :combo, based on multimethod dispatch rules. This is written (Val :combo)key : Meal(o), pronounced “the :Meal path of variable o is of type (Val :combo)”.

To attain the type of o, we must solve for τ in Γ ⊢ τo, under proposition environment Γ = Ordero,(Val :combo)key : Meal(o) which deduces τ to be a :combo meal. The logical system combines pieces of type information to deduce more accurate types for lexical bindings—this is explained in Section 5.6.

Typing judgment We formalize our system following Tobin-Hochstadt and Felleisen [75]. The typing judgment Γ ⊢ e ⇒ e′ : τ ; ψ+|ψ− ; o says expression e rewrites to e′, which is of type τ in the proposition environment Γ, with ‘then’ proposition ψ+, ‘else’ proposition ψ− and object o. For ease of presentation, we omit e′ when it is easily inferred.

We write Γ ⊢ e ⇒ e′ : τ to mean Γ ⊢ e ⇒ e′ : τ ; ψ′+|ψ′− ; o′ for some ψ′+, ψ′ − and o′.

Typing rules The core typing rules are given as Figure 5.2. We introduce the interesting rules with the complement number predicate as a running example.

(5.1)

The lambda rule T-Abs introduces σx = ⊤d to check the body. With Γ = ⊤d, T-If first checks the test e1 = (n? d) via the T-App rule, with three steps.

First, in T-App the operator e = n? is checked with T-Const, which uses δτ (Figure 5.6, dynamic semantics in the supplemental material) to type constants. n? is a predicate over numbers, and class returns its argument’s class.

Resuming (n? d), in T-App the operand e′ = d is checked with T-Local as

(5.2)

which encodes the type, proposition, and object information about variables. The proposition (∪ nil false)d says “it is not the case that variable d is of type (∪ nil false)”; (∪ nil false)d says “d is of type (∪ nil false)”.

Finally, the T-App rule substitutes the operand’s object o′ for the parameter x in the latent type, propositions, and object. The proposition Nd says “d is of type N”; Nd says “it is not the case that d is of type N”. The object d is the symbolic representation of what the expression d evaluates to.

(5.3)

To demonstrate, the ‘then’ proposition—in T-App ψ+[o′∕x]—substitutes the latent ‘then’ proposition of δτ(n?) with d, giving Nx[d∕x] = Nd.

To check the branches of (if (n? d) false true), T-If introduces ψ1+ = Nd to check e2 = false, and ψ1− = Nd to check e3 = true. The branches are first checked with T-False and T-True respectively, the T-Subsume premises Γ,ψ+ ⊢ ψ′+ and Γ,ψ− ⊢ ψ′− allow us to pick compatible propositions for both branches.

Finally T-Abs assigns a type to the overall function:

Subtyping Figure 5.3 presents subtyping as a reflexive and transitive relation with top type ⊤. Singleton types are instances of their respective classes—boolean singleton types are of type B, class literals are instances of Class and keywords are instances of K. Instances of classes C are subtypes of Object. Function types are subtypes of Fn. All types except for nil are subtypes of Object, so ⊤ is similar to (⋃  nil Object). Function subtyping is contravariant left of the arrow—latent propositions, object and result type are covariant. Subtyping for untagged unions is standard.

Operational semantics We define the dynamic semantics for λTC in a big-step style using an environment, following [75]. We include both errors and a wrong value, which is provably ruled out by the type system. The main judgment is ρ ⊢ e ⇓ α which states that e evaluates to answer α in environment ρ. We chose to omit the core rules (included in supplemental material) however a notable difference is nil is a false value, which affects the semantics of if (Figure 5.4).

5.2 Java Interoperability

We present Java interoperability in a restricted setting without class inheritance, overloading or Java Generics. We extend the syntax in Figure 5.5 with Java field lookups and calls to methods and constructors. To prevent ambiguity between zero-argument methods and fields, we use Clojure’s primitive “dot” syntax: field accesses are written (. e fld) and method calls (. e (mth)). In Example 1, (.getParent (new File "a/b")) translates to

(5.4)

But both the constructor and method are unresolved. We introduce non-reflective expressions for specifying exact Java overloads.

(5.5)

From the left, the one-argument constructor for F takes a S, and the getParent method of F takes zero arguments and returns a S.

We now walk through this conversion.

Constructors First we check and convert (new F“a∕b”) to (new[S] F “a∕b”). The T-New typing rule checks and rewrites constructors. To check (new F“a∕b”) we first resolve the constructor overload in the class table—there is at most one to simplify presentation. With C1 = S, we convert to a nilable type the argument with τ1 = (⋃  nil S) and type check “a∕b” against τ1. Typed Clojure defaults to allowing non-nilable arguments, but this can be overridden, so we model the more general case. The return Java type F is converted to a non-nil Typed Clojure type τ = F for the return type, and the propositions say constructors can never be false—constructors can never produce the internal boolean value that Clojure uses for false, or nil. Finally, the constructor rewrites to (new[S] F “a∕b”).

Methods Next we convert (. (new[S] F “a∕b”) (getParent)) to the non-reflective expression (. (new[S] F “a∕b”) (getParentF [[],S])). The T-Method rule for unresolved methods checks:

(. (new[S] F “a∕b”) (getParent)).

We verify the target type σ = F is non-nil by T-New. The overload is chosen from the class table based on C1 = F—there is at most one. The nilable return type τ = (⋃  nil S) is given, and the entire expression rewrites to expression 5.5.

The T-Field rule (Figure 5.5) is like T-Method, but without arguments.

The evaluation rules B-Field, B-New and B-Method (Figure 5.5) simply evaluate their arguments and call the relevant JVM operation, which we do not model—Section 6 states our exact assumptions. There are no evaluation rules for reflective Java interoperability, since there are no typing rules that rewrite to reflective calls.

5.3 Multimethod preliminaries: isa?

We now consider the isa? operation, a core part of the multimethod dispatch mechanism. Recalling the examples in Section 4.4, isa? is a subclassing test for classes, but otherwise is an equality test. The T-IsA rule uses IsAProps (Figure 5.7), a metafunction which produces the propositions for isa? expressions.

To demonstrate the first IsAProps case, the expression (isa? (class x) K) is true if x is a keyword, otherwise false. When checked with T-IsA, the object of the left subexpression o = class(x) (which starts with the class path element) and the type of the right subexpression τ = (ValK) (a singleton class type) together trigger the first IsAProps case IsAProps(class(x),(ValK)) = Kx|Kx, giving propositions that correspond to our informal description ψ+|ψ− = Kx|Kx.

The second IsAProps case captures the simple equality mode for non-class singleton types. For example, the expression (isa? x :en) produces true when x evaluates to :en, otherwise it produces false. Using T-IsA, it has the propositions ψ +|ψ− = IsAProps(x,(Val :en)) = (Val :en)x|(Val :en)x since o = x and τ = (Val :en). The side condition on the second IsAProps case ensures we are in equality mode—if x can possibly be a class in (isa? x Object), IsAProps uses its conservative default case, since if x is a class literal, subclassing mode could be triggered. Capture-avoiding substitution of objects [o∕x] used in this case erases propositions that would otherwise have ∅ substituted in for their objects—it is defined in the appendix.

The operational behavior of isa? is given by B-IsA (Figure 5.7). IsA explicitly handles classes in the second case.

5.4 Multimethods

Figure 5.7 presents immutable multimethods without default methods to ease presentation. Figure 5.8 translates the mutable Example 4 to λTC.

To check (defmulti x:KS λxK.x), we note (defmulti σ e) creates a multimethod with interface type σ, and dispatch function e of type ^, producing a value of type (Multi σ ^). The T-DefMulti typing rule checks the dispatch function, and verifies both the interface and dispatch type’s domain agree. Our example checks with τ = K, interface type σ = x:KS, dispatch function type ^ = x:K K, and overall type (Multix:KS x:K K).

Next, we show how to check (defmethod hi₀ :en λxK.“hello”). The expression (defmethod em ev ef) creates a new multimethod that extends multimethod em’s dispatch table, mapping dispatch value ev to method ef. The T-DefMulti typing rule checks em is a multimethod with dispatch function type τd, then calculates the extra information we know based on the current dispatch value ψ′′+, which is assumed when checking the method body. Our example checks with em being of type (Multix:KS x:K K) with o′ = x (from below the arrow on the right argument of the previous type) and τv = (Val :en). Then ψ′′+ = (Val :en)x from IsAProps(x,(Val :en)) = (Val :en)x|(Val :en)x (see Section 5.3). Since τ = K, we check the method body with

It is worth noting the lack of special typing rules for overlapping methods—each method is checked independently based on local type information.

Subtyping Multimethods are functions, via S-PMultiFn, which says a multimethod can be upcast to its interface type. Multimethod call sites are then handled by T-App via T-Subsume. Other rules are given in Figure 5.7.

Semantics Multimethod definition semantics are also given in Figure 5.7. B-DefMulti creates a multimethod with the given dispatch function and an empty dispatch table. B-DefMethod produces a new multimethod with an extended dispatch table.

The overall dispatch mechanism is summarised by B-BetaMulti. First the dispatch function vd is applied to the argument v′ to obtain the dispatch value ve. Based on ve, the GM metafunction (Figure 5.7) extracts a method vf from the method table t and applies it to the original argument for the final result.

5.5 Precise Types for Heterogeneous maps

Figure 5.9 presents heterogeneous map types. The type (HMapE M A) contains M, a map of present entries (mapping keywords to types), A, a set of keyword keys that are known to be absent and tag E which is either C (“complete”) if the map is fully specified by M, and P (“partial”) if there are unknown entries. The partially specified map of lunch in Example 6 is written (HMapP{(Val :en) S,(Val :fr) S} {}) (abbreviated Lu). The type of the fully specified map breakfast in Example 5 elides the absent entries, written (HMapC{(Val :en) S,(Val :fr) S}) (abbreviated Bf). To ease presentation, if an HMap has completeness tag C then A is elided and implicitly contains all keywords not in the domain of M—dissociating keys is not modelled, so the set of absent entries otherwise never grows. Keys cannot be both present and absent.

The metavariable m ranges over the runtime value of maps {}, usually written {}. We only provide syntax for the empty map literal, however when convenient we abbreviate non-empty map literals to be a series of assoc operations on the empty map. We restrict lookup and extension to keyword keys.

How to check A mandatory lookup is checked by T-GetHMap.

An absent lookup is checked by T-GetHMapAbsent.

A lookup that is not present or absent is checked by T-GetHMapPartialDefault.

For presentational reasons, lookups on unions of HMaps are only supported in T-GetHMap and each element of the union must contain the relevant key.

Extending a map with T-AssocHMap preserves its completeness.

Subtyping Subtyping for HMaps designate Map as a common supertype for all HMaps. S-HMap says that HMaps are subtypes if they agree on E, agree on mandatory entries with subtyping and at least cover the absent keys of the supertype. Complete maps are subtypes of partial maps as long as they agree on the mandatory entries of the partial map via subtyping (S-HMapP).

The semantics for get and assoc are straightforward.

5.6 Proof system

The occurrence typing proof system uses standard propositional logic, except for where nested information is combined. This is handled by L-Update:

It says under Γ, if object π′(x) is of type τ, and an extension π(π′(x)) is of possibly-negative type ν, then update (τ, ν, π) is π′(x)’s type under Γ.

Recall Example 8. Solving Ordero,(Val :combo)key : Meal(o) ⊢ τo uses L-Update, where π = 𝜖 and π′ = [key:Meal].

To demonstrate, :lunch meals are handled by the first HMap case and update to

In Example 9, Γ ⊢ update(Order,Long,[class,key:desserts])o updates the argument in the Long method. This recurs twice for each meal to handle the class path element.

We describe the other update cases. The first class case updates to C if class returns (ValC). The second keyk case detects contradictions in absent keys. The third keyk case updates unknown entries to be mapped to τ or absent. The fourth key k case updates unknown entries to be present when they do not overlap with nil.

Chapter 6
Metatheory

We prove type soundness following Tobin-Hochstadt and Felleisen [75]. Our model is extended to include errors err and a wrong value, and we prove well-typed programs do not go wrong; this is therefore a stronger theorem than proved by Tobin-Hochstadt and Felleisen [75]. Errors behave like Java exceptions—they can be thrown and propagate “upwards” in the evaluation rules (err rules are deferred to the appendix).

Rather than modeling Java’s dynamic semantics, a task of daunting complexity, we instead make our assumptions about Java explicit. We concede that method and constructor calls may diverge or error, but assume they can never go wrong.

For readability we define logical truth in Clojure.

For the purposes of our soundness proof, we require that all values are consistent. Consistency states that the types of closures are well-scoped—they do not claim propositions about variables hidden in their closures.

We can now state our main lemma and soundness theorem. The metavariable α ranges over v, err and wrong. Proofs are deferred to the supplemental material.

Chapter 7
Experience

Typed Clojure is implemented as core.typed [7], which has seen wide usage.

7.1 Implementation

core.typed provides preliminary integration with the Clojure compilation pipeline, primarily to resolve Java interoperability.

The core.typed implementation extends this paper in several key areas to handle checking real Clojure code, including an implementation of Typed Racket’s variable-arity polymorphism [74], and support for other Clojure idioms like datatypes and protocols. There is no integration with Java Generics, so only Java 1.4-style erased types are “trusted” by core.typed. Casts are needed to recover the discarded information, which—for collections—are then tracked via Clojure’s universal sequence interface [42].

7.2 Evaluation

Throughout this paper, we have focused on three interrelated type system features: heterogeneous maps, Java interoperability, and multimethods. Our hypothesis is that these features are widely used in existing Clojure programs in interconnecting ways, and that handling them as we have done is required to type check realistic Clojure programs.

To evaluate this hypothesis, we analyzed two existing core.typed code bases, one from the open-source community, and one from a company that uses core.typed in production. For our data gathering, we instrumented the core.typed type checker to record how often various features were used (summarized in Figure 7.1).

feeds2imap feeds2imap¹ is an open source library written in Typed Clojure. It provides an RSS reader using the javax.mail framework.

Of 11 typed namespaces containing 825 lines of code, there are 32 Java interactions. The majority are method calls, consisting of 20 (62%) instance methods and 5 (16%) static methods. The rest consists of 1 (3%) static field access, and 6 (19%) constructor calls—there are no instance field accesses.

There are 27 lookup operations on HMap types, of which 20 (74%) resolve to mandatory entries, 6 (22%) to optional entries, and 1 (4%) is an unresolved lookup. No lookups involved fully specified maps.

From 93 def expressions in typed code, 52 (56%) are checked, with a rate of 1 Java interaction for 1.6 checked top-level definitions, and 1 HMap lookup to 1.9 checked top-level definitions. That leaves 41 (44%) unchecked vars, mainly due to partially complete porting to Typed Clojure, but in some cases due to unannotated third-party libraries.

No typed multimethods are defined or used. Of 18 total type aliases, 7 (39%) contained one HMap type, and none contained unions of HMaps—on further inspection there was no HMap entry used to dictate control flow, often handled by multimethods. This is unusual in our experience, and is perhaps explained by feeds2imap mainly wrapping existing javax.mail functionality.

CircleCI CircleCI [19] provides continuous integration services built with a mixture of open- and closed-source software. Typed Clojure was used at CircleCI in production systems for two years [21], maintaining 87 namespaces and 19,000 lines of code, an experience we summarise in Section 7.3.

The CircleCI code base contains 11 checked multimethods. All 11 dispatch functions are on a HMap key containing a keyword, in a similar style to Example 8. Correspondingly, all 89 methods are associated with a keyword dispatch value. The argument type was in all cases a single HMap type, however, rather than a union type. In our experience from porting other libraries, this is unusual.

Of 328 lookup operations on HMaps, 208 (64%) resolve to mandatory keys, 70 (21%) to optional keys, 20 (6%) to absent keys, and 30 (9%) lookups are unresolved. Of 95 total type aliases defined with defalias, 62 (65%) involved one or more HMap types. Out of 105 Java interactions, 26 (25%) are static methods, 36 (34%) are instance methods, 38 (36%) are constructors, and 5 (5%) are static fields. 35 methods are overriden to return non-nil, and 1 method overridden to accept nil—suggesting that core.typed disallowing nil as a method argument by default is justified.

Of 464 checked top-level definitions (which consists of 57 defmethod calls and 407 def expressions), 1 HMap lookup occurs per 1.4 top-level definitions, and 1 Java interaction occurs every 4.4 top-level definitions.

From 1834 def expressions in typed code, only 407 (22%) were checked. That leaves 1427 (78%) which have unchecked definitions, either by an explicit :no-check annotation or tc-ignore to suppress type checking, or the warn-on-unannotated-vars option, which skips def expressions that lack expected types via ann. From a brief investigation, reasons include unannotated third-party libraries, work-in-progress conversions to Typed Clojure, unsupported Clojure idioms, and hard-to-check code.

Lessons Based on our empirical survey, HMaps and Java interoperability support are vital features used on average more than once per typed function. Multimethods are less common in our case studies. The CircleCI code base contains only 26 multimethods total in 55,000 lines of mixed untyped-typed Clojure code, a low number in our experience.

7.3 Further challenges

After a 2 year trial, the second case study decided to disabled type checking [20]. They were supportive of the fundamental ideas presented in this paper, but primarily cited issues with the checker implementation in practice and would reconsider type checking if they were resolved. This is also supported by Figure 7.1, where 78% of def expressions are unchecked.

Performance Rechecking files with transitive dependencies is expensive since all dependencies must be rechecked. We conjecture caching type state will significantly improve re-checking performance, though preserving static soundness in the context of arbitrary code reloading is a largely unexplored area.

Library annotations Annotations for external code are rarely available, so a large part of the untyped-typed porting process is reverse engineering libraries.

Unsupported idioms While the current set of features is vital to checking Clojure code, there is still much work to do. For example, common Clojure functions are often too polymorphic for the current implementation or theory to account for. The post-mortem [20] contains more details.

Chapter 8
Conclusion

Optional type systems must be designed with close attention to the language that they are intended to work for. We have therefore designed Typed Clojure, an optionally-typed version of Clojure, with a type system that works with a wide variety of distinctive Clojure idioms and features. Although based on the foundation of Typed Racket’s occurrence typing approach, Typed Clojure both extends the fundamental control-flow based reasoning as well as applying it to handle seemingly unrelated features such as multi-methods. In addition, Typed Clojure supports crucial features such as heterogeneous maps and Java interoperability while integrating these features into the core type system. Not only are each of these features important in isolation to Clojure and Typed Clojure programmers, but they must fit together smoothly to ensure that existing untyped programs are easy to convert to Typed Clojure.

The result is a sound, expressive, and useful type system which, as implemented in core.typed with appropriate extensions, is suitable for typechecking a significant amount of existing Clojure programs. As a result, Typed Clojure is already successful: it is used in the Clojure community among both enthusiasts and professional programmers.

Our empirical analysis of existing Typed Clojure programs bears out our design choices. Multimethods, Java interoperation, and heterogeneous maps are indeed common in both Clojure and Typed Clojure, meaning that our type system must accommodate them. Furthermore, they are commonly used together, and the features of each are mutually reinforcing. Additionally, the choice to make Java’s null explicit in the type system is validated by the many Typed Clojure programs that specify non-nullable types.

However, there is much more that Typed Clojure can provide. Most significantly, Typed Clojure currently does not provide gradual typing—interaction between typed and untyped code is unchecked and thus unsound. We hope to explore the possibilities of using existing mechanisms for contracts and proxies in Java and Clojure to enable sound gradual typing for Clojure.

Additionally, the Clojure compiler is unable to use Typed Clojure’s wealth of static information to optimize programs. Addressing this requires not only enabling sound gradual typing, but also integrating Typed Clojure into the Clojure tool so that its information can be communicated to the compiler.

Finally, our case study, evaluation, and broader experience indicate that Clojure programmers still find themselves unable to use Typed Clojure on some of their programs for lack of expressiveness. This requires continued effort to analyze and understand the features and idioms and develop new type checking approaches.

Part II
Automatic Annotations for Typed Clojure

Chapter 9
Abstract

We present a semi-automated workflow for porting untyped programs to annotation-driven optional type systems. Unlike previous work, we infer useful types for recursive heterogeneous entities that have “ad-hoc” representations as plain data structures like maps, vectors, and sequences.

Our workflow starts by using dynamic analysis to collect samples from program execution via test suites or examples. Then, initial type annotations are inferred by combining observations across different parts of the program. Finally, the programmer uses the type system as a feedback loop to tweak the provided annotations until they type check.

Since inferring perfect annotations is usually undecidable and dynamic analysis is necessarily incomplete, the key to our approach is generating close-enough annotations that are easy to manipulate to their final form by following static type error messages. We explain our philosophy behind achieving this along with a formal model of the automated stages of our workflow, featuring maps as the primary “ad-hoc” data representation.

We report on using our workflow to convert real untyped Clojure programs to type check with Typed Clojure, which both feature extensive support for ad-hoc data representations. First, we visually inspect the initial annotations for conformance to our philosophy. Second, we quantify the kinds of manual changes needed to amend them. Third, we verify the initial annotations are meaningfully underprecise by enforcing them at runtime.

We find that the kinds of changes needed are usually straightforward operations on the initial annotations, leading to a substantial reduction in the effort required to port such programs.

Chapter 10
Introduction

Consider the exercise of counting binary tree nodes using JavaScript. With a class-based tree representation, we naturally add a method to each kind of node like so.

An alternative “ad-hoc” representation uses plain JavaScript Objects with explicit tags, which is less extensible but simpler. Then, the method becomes a recursive function that explicitly takes a tree as input.

Now, consider the problem of inferring type annotations for these programs. The class-based representation is idiomatic to popular dynamic languages like JavaScript and Python, and so many existing solutions support it. For example, TypeWiz [72] uses dynamic analysis to generate the following TypeScript annotations from the above example execution of nodes.

The intuition behind inferring such a type is straightforward. For example, an instance of Leaf was observed in Node’s left field, and so the nominal type Leaf is used for its annotation.

The second “ad-hoc” style of programming seems peculiar in JavaScript, Python, and, indeed, object-oriented style in general. Correspondingly, existing state-of-the-art automatic annotation tools are not designed to support them. There are several ways to trivially handle such cases. Some enumerate the tree representation “verbatim” in a union, like TypeWiz [72].

Others “discard” most (or all) structure, like Typette [38] and PyType [33] for Python.

Each annotation is clearly insufficient to meaningfully check both the function definition and valid usages. To show a desirable annotation for the “ad-hoc” program, we port it to Clojure [44], where it enjoys full support from the built-in runtime verification library clojure.spec and primary optional type system Typed Clojure [8].

Making this style viable requires a harmony of language features, in particular to support programming with functions and immutable values, but none of which comes at the expense of object-orientation. Clojure is hosted on the Java Virtual Machine and has full interoperability with Java objects and classes—even Clojure’s core design embraces object-orientation by exposing a collection of Java interfaces to create new kinds of data structures. The {k v ...} syntax creates a persistent and immutable Hash Array Mapped Trie [5], which can be efficiently manipulated by dozens of built-in functions. The leading colon syntax like :op creates an interned keyword, which are ideal for map keys for their fast equality checks, and also look themselves up in maps when used as functions (e.g., (:op t) is like JavaScript’s t.op). Multimethods regain the extensibility we lost when abandoning methods, like the following.

On the type system side, Typed Clojure supports a variety of heterogeneous types, in particular for maps, along with occurrence typing [75] to follow local control flow. Many key features come together to represent our “ad-hoc” binary tree as the following type.

The defalias form introduces an equi-recursive type alias Tree, U a union type, '{:kw Type ...} for heterogeneous keyword map types, and ':node for keyword singleton types. With the following function annotation, Typed Clojure can intelligently type check the definition and usages of nodes.

This (manually written) Typed Clojure annotation involving Tree is significantly different from TypeWiz’s “verbatim” annotation for nodes. First, it is recursive, and so supports trees of arbitrary depth (TypeWiz’s annotation supports trees of height < 3). Second, it uses singleton types ':leaf and ':node to distinguish each case (TypeWiz upcasts "leaf" and "node" to string). Third, the tree type is factored out under a name to enhance readability and reusability. On the other end of the spectrum, the “discarding” annotations of Typette and PyType are too imprecise to use meaningfully (they include trees of arbitrary depth, but also many other values).

The challenge we overcome in this research is to automatically generate annotations like Typed Clojure’s Tree, in such a way that the ease of manual amendment is only mildly reduced by unresolvable ambiguities and incomplete data collection.

Chapter 11
Overview

We demonstrate our approach by synthesizing a Typed Clojure annotation for nodes. The following presentation is somewhat loose to keep from being bogged down by details—interested readers may follow the pointers to subsequent sections where they are made precise.

We use dynamic analysis to observe the execution of functions, so we give an explicit test suite for nodes.

The first step is the instrumentation phase (formalized in Section 12.1), which monitors the inputs and outputs of nodes by redefining it to use the track function like so (where <nodes-body> begins the case expression of the original nodes definition):

The track function (given later in Figure 12.2) takes a value to track and a path that represents its origin, and returns an instrumented value along with recording some runtime samples about the value. A path is represented as a vector of path elements, and describes the source of the value in question. For example, (track 3 ['nodes :rng]) returns 3 and records the sample ['nodes :rng] : Int which says “Int was recorded at nodes’s range.” Running our test suite nodes-test with an instrumented nodes results in more samples like this, most which use the path element {:key :kw} which represents a map lookup on the :kw entry.

• ['nodes :dom {:key :op}] : ':leaf
• ['nodes :dom {:key :op}] : ':node
• ['nodes :dom {:key :val}] : ?
• ['nodes :dom {:key :left}] : ?
• ['nodes :dom {:key :right}] : ?
• ['nodes :dom {:key :left}{:key :op}] : ':leaf
• ['nodes :dom {:key :right}{:key :op}] : ':leaf
• ['nodes :dom {:key :left}{:key :val}] : Int
• ['nodes :dom {:key :right}{:key :val}] : Int
• ['nodes :rng] : Int

Now, our task is to transform these samples into a readable and useful annotation. This is the function of the inference phase (formalized in Section 12.2), which is split into three passes: first it generates a naive type from samples, then it combines types that occur syntactically near eachother (“squash locally”), and then aggressively across different function annotations (“squash globally”).

The initial naive type generated from these samples resembles TypeWiz’s “verbatim” annotation given in Chapter 10, except the ? placeholder represents incomplete information about a path (this process is formalized as toEnv in Figure 12.3).

Next, the two “squashing” phases. The intuition behind both are based on seeing types as directed graphs, where vertices are type aliases, and an edge connects two vertices u and v if u is mentioned in v’s type.

Local squashing (squashLocal in Figure 12.4) constructs such a graph by creating type aliases from map types using a post-order traversal of the original types. In this example, the previous annotations become:

As a graph, this becomes the left-most graph below. The dotted edge from op-leaf2 to op-leaf1 signifies that they are to be merged, based on the similar structure of the types they point to.

After several merges (reading the graphs left-to-right), local squashing results in the following:

All three duplications of the ':leaf type in the naive annotation have been consolidated into their own name, with the ? placeholder for the :val entry being absorbed into Int.

Now, the global squashing phase (squashGlobal in Figure 12.5) proceeds similarly, except the notion of a vertex is expanded to also include unions of map types, calculated, again, with a post-order traversal of the types giving:

This creates op-leaf-node, giving the left-most graph below.

Now, type aliases are merged based on overlapping sets of top-level keysets and likely tags. Since op-leaf and op-leaf-node refer to maps with identical keysets (:op and :val) and whose likely tags agree (the :op entry is probably a tag, and they are both ':leaf), they are merged and all occurrences of op-leaf are renamed to op-leaf-node, creating a mutually recursive type between the remaining aliases in the middle graph:

In the right-most graph, the aliases op-node and op-leaf-node are merged for similar reasons:

All that remains is to choose a recognizable name for the alias. Since all its top-level types seem to use the :op entry for tags, we choose the name Op and output the final annotation:

The rest of the porting workflow involves the programmer repeatedly type checking their code and gradually tweaking the generated annotations until they type check. It turns out that this annotation immediately type checks the definition of nodes and all its valid usages, so we turn to a more complicated function visit-leaf to demonstrate a typical scenario.