Practical Optional Types for Clojure
Ambrose Bonnaire-Sergeant, Rowan Davies, Sam Tobin-Hochstadt
TL;DR
Typed Clojure introduces an optional static type system for Clojure, enhancing code correctness and safety while supporting common idioms and Java interoperability, with formal guarantees and real-world adoption.
Contribution
It extends Typed Racket's occurrence typing to Clojure, incorporating features for multimethods, Java interop, and heterogeneous dictionaries, with formal soundness proof.
Findings
Formal model and soundness proof of Typed Clojure's type system.
Widespread adoption in industry and open-source projects.
Quantitative analysis of type feature usage in large codebases.
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 paper, 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…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Software Engineering Research · Software Testing and Debugging Techniques
11institutetext: Indiana University; Omnia Team, Commonwealth Bank of Australia* {abonnair,samth}@indiana.edu, [email protected]
Practical Optional Types for Clojure
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 paper, 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.
1 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 [19] and Flow [11] for JavaScript, Hack [10] for PHP, and mypy [15] for Python among the optional systems, and Typed Racket [23], Reticulated Python [25], and Gradualtalk [1] among gradually-typed systems.111We use “gradual typing” for systems like Typed Racket with sound interoperation between typed and untyped code; Typed Clojure or TypeScript which don’t enforce type invariants we describe as “optionally typed”.
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 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.
Our main contributions are as follows:
We motivate and describe Typed Clojure, an optional type system for Clojure that understands existing Clojure idioms. 2. 2.
We present a sound formal model for three crucial type system features: multi-methods, Java interoperability, and heterogenous maps. 3. 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 paper begins with an example-driven presentation of the main type system features in Section 2. We then incrementally present a core calculus for Typed Clojure covering all of these features together in Section 3 and prove type soundness (Section 4). We then present an empirical analysis of significant code bases written in core.typed—the full implementation of Typed Clojure—in Section 5. Finally, we discuss related work and conclude.
2 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,222Full examples: https://github.com/typedclojure/esop16 before studying the core features in detail in Section 3.
2.1 Clojure
Clojure [13] 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.
2.2 Typed Clojure
A simple one-argument function greet is annotated with ann to take and return strings.
(typed ann greet [Str -> Str] typed)
(defn greet [n] (invoke str "Hello, " n "!" invoke))
(invoke greet "Grace" invoke) ;=> "Hello, Grace!" :- Str
Providing nil (exactly Java’s null) is a static type error—nil is not a string.
(invoke greet nil invoke) ; Type Error: Expected Str, given nil
Unions
To allow nil, we use ad-hoc unions (nil and false are logically false).
(typed ann greet-nil [(U nil Str) -> Str] typed)
(defn greet-nil [n] (invoke str "Hello" (when n (invoke str ", " n invoke)) "!" invoke))
(invoke greet-nil "Donald" invoke) ;=> "Hello, Donald!" :- Str
(invoke greet-nil nil invoke) ;=> "Hello!" :- Str
Typed Clojure prevents well-typed code from dereferencing nil.
Flow analysis
Occurrence typing [24] models type-based control flow. In greetings, a branch ensures repeat is never passed nil.
(typed ann greetings [Str (U nil Int) -> Str] typed)
(defn greetings [n i]
(invoke str "Hello, " (when i (invoke apply str (invoke repeat i "hello, " invoke) invoke)) n "!" invoke))
(invoke greetings "Donald" 2 invoke) ;=> "Hello, hello, hello, Donald!" :- Str
(invoke greetings "Grace" nil invoke) ;=> "Hello, Grace!" :- Str
Removing the branch is a static type error—repeat cannot be passed nil.
(typed ann greetings-bad [Str (U nil Int) -> Str] typed)
(defn greetings-bad [n i] ; Expected Int, given (U nil Int)
(invoke str "Hello, " (invoke apply str (invoke repeat i "hello, " invoke) invoke) n "!" invoke))
2.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
(interop .getParent (interop new File "a/b" interop) interop) ;=> "a" :- (U nil Str)
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.
(fn [f] (interop .getParent f interop)) ; Type Error: Unresolved interop: getParent
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
(typed ann parent [(U nil File) -> (U nil Str)] typed)
(defn parent [f] (if f (interop .getParent f interop) nil))
The conditional guards from dereferencing nil, and—as before—removing it is a static type error, as typed code could possibly dereference nil.
(defn parent-bad-in [f :- (U nil File)]
(interop .getParent f interop)) ; Type Error: Cannot call instance method on nil.
Typed Clojure rejects programs that assume methods cannot return nil.
(defn parent-bad-out [f :- File] :- Str
(interop .getParent f interop)) ; Type Error: Expected Str, given (U nil Str).
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.333http://docs.oracle.com/javase/specs/jls/se7/html/jls-15.html#jls-15.9.4
Example 3
(invoke parent (interop new File s interop) invoke)
2.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
(typed ann hi [Kw -> Str] typed) ; multimethod type
(defmulti hi identity) ; dispatch function identity
(defmethod hi :en [_] "hello") ; method for :en
(defmethod hi :fr [_] "bonjour") ; method for :fr
(defmethod hi :default [_] "um...") ; default method
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.
(invoke map hi [vec :en :fr :bocce vec] invoke) ;=> (list "hello" "bonjour" "um..." list)
For example, (invoke hi :en invoke) evaluates to "hello"—it executes the :en method because (invoke = (invoke identity :en invoke) :en invoke) is true and (invoke = (invoke identity :en invoke) :fr invoke) 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 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.
(invoke isa? :en :en invoke) ;=> true
(invoke isa? String Object invoke) ;=> true
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, the call (invoke pname "STAINS/JELLY" invoke) picks the String method because (invoke isa? String String invoke) is true, and (invoke isa? String File invoke) is not.
2.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
(def breakfast {map :en "waffles" :fr "croissants" map})
(invoke :en breakfast invoke) ;=> "waffles" :- Str
(invoke :bocce breakfast invoke) ;=> nil :- nil
HMap types describe the most common usages of keyword-keyed maps.
breakfast ; :- (HMap :mandatory {:en Str, :fr Str}, :complete? true)
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, with '{:en Str :fr Str} abbreviating (HMap :mandatory {:en Str, :fr Str}).
Example 6
(typed ann lunch '{:en Str :fr Str} typed)
(def lunch {map :en "muffin" :fr "baguette" map})
(invoke :bocce lunch invoke) ;=> nil :- Any ; less accurate type
HMaps in practice
The next example is extracted from a production system at CircleCI, a company with a large production Typed Clojure system (Section 5.2 presents a case study and empirical result from this code base).
Example 7
(*typed defalias RawKeyPair ; extra keys disallowed
(HMap :mandatory {:pub RawKey, :priv RawKey},
:complete? **t**rue) typed*)
(*typed defalias EncKeyPair ; extra keys disallowed
(HMap :mandatory {:pub RawKey, :enc-priv EncKey}, :complete? true) typed*)
(typed ann enc-keypair [RawKeyPair -> EncKeyPair] typed)
(defn enc-keypair [kp]
(invoke assoc (invoke dissoc kp :priv invoke) :enc-priv (invoke encrypt (invoke :priv kp invoke) invoke) invoke))
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.
(defn enc-keypair-bad [kp] ; Type error: :priv disallowed
(invoke assoc kp :enc-priv (invoke encrypt (invoke :priv kp invoke) invoke) invoke))
2.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.
(*typed defalias Order "A meal order, tracking dessert quantities."
(U '{:Meal ':lunch, :desserts Int} '{:Meal ':dinner :desserts Int}
'{:Meal ':combo :meal1 Order :meal2 Order}) typed*)
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.
Example 8
(typed ann desserts [Order -> Int] typed)
(defmulti desserts :Meal) ; dispatch on :Meal entry
(defmethod desserts :lunch [o] (invoke :desserts o invoke))
(defmethod desserts :dinner [o] (invoke :desserts o invoke))
(defmethod desserts :combo [o]
(invoke + (invoke desserts (invoke :meal1 o invoke) invoke) (invoke desserts (invoke :meal2 o invoke) invoke) invoke))
(*invoke desserts {*map :Meal :combo, :meal1 {map :Meal :lunch :desserts 1 map},
:meal2 {***m**ap :Meal :dinner :desserts 2 **m**ap*} **m**ap*} invoke*) ;=> 3
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.
Example 9
(typed ann desserts' [Order -> Int] typed)
(defmulti desserts'
(fn [o :- Order] (invoke class (invoke :desserts o invoke) invoke)))
(defmethod desserts' Long [o]
;o :- (U '{:Meal (U ':dinner ':lunch), :desserts Int}
; '{:Meal ':combo, :desserts Int, :meal1 Order, :meal2 Order})
(invoke :desserts o invoke))
(defmethod desserts' nil [o]
; o :- '{:Meal ':combo, :meal1 Order, :meal2 Order}
(invoke + (invoke desserts' (invoke :meal1 o invoke) invoke) (invoke desserts' (invoke :meal2 o invoke) invoke) invoke))
In the Long method, Typed Clojure learns that its argument is at least of type '{:desserts Long}—since (invoke isa? (invoke class (invoke :desserts o invoke) invoke) Long invoke) 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, (invoke isa? (invoke class (invoke :desserts o invoke) invoke) nil invoke) must be true—which implies (invoke class (invoke :desserts o invoke) invoke) 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
(U '{:desserts nil} (HMap :absent-keys #{:desserts}))
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.
3 A Formal Model of
After demonstrating the core features of Typed Clojure, we link them together in a formal model called . 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.
3.1 Core type system
We start with a review of occurrence typing [24], the foundation of .
Expressions
Syntax is given in Figure 2. Expressions include variables , values , 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 , , class literals , keywords , integers , constants , and strings . Lexical closures close value environments —which map bindings to values—over functions.
Types
Types or include the top type \mathop{\hbox{\bf\top\/}}\nolimits, untagged unions (\mathop{\hbox{\bf\bigcup\/}}\nolimits\ \overrightarrow{\tau}), singletons , and class instances . We abbreviate the classes to , to , to , to , and to . We also abbreviate the types (\mathop{\hbox{\bf\bigcup\/}}\nolimits) to \mathop{\hbox{\bf\bot\/}}\nolimits, () to , () to , and () to . The difference between the types () and is subtle. The former is inhabited by class literals like and the result of —the latter by instances of classes, like a keyword literal , an instance of the type . Function types contain latent (terminology from [17]) propositions , object , and return type , which may refer to the function argument . 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 has object ; has object ; and has the empty object since it is unimportant in our system. Figure 2 gives the syntax for objects —non-empty objects \pathelem{} combine of a root variable and a path , which consists of a possibly-empty sequence of path elements () applied right-to-left from the root variable. We use two path elements—class and —representing the results of calling class and looking up a keyword , 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.
[TABLE]
Occurrence typing instead pairs logical formulas, that can reason about arbitrary non-empty objects, with a proof system. The logical statement says variable is of type .
[TABLE]
In T0-Local, appeals to the proof system to solve for .
We further extend logical statements to propositional logic. Figure 2 describes the syntax for propositions , consisting of positive and negative type propositions about non-empty objects— and respectively—the latter pronounced “the object \pathelem{} is not of type ”. The other propositions are standard logical connectives: implications, conjunctions, disjunctions, and the trivial () and impossible () propositions. The full proof system judgement says proposition environment proves proposition .
Each expression is associated with two propositions—when expression is in test position like , the type system extracts ’s ‘then’ and ‘else’ proposition to check and respectively. For example, in we learn variable is true in via ’s ‘then’ proposition {\overline{\mathop{\hbox{\bf(\cup\ \mathop{\hbox{\bf nil/}}\nolimits\ \mathop{\hbox{\bf false/}}\nolimits)\/}}\nolimits{}}}_{o}, and that is false in via ’s ‘else’ proposition {\mathop{\hbox{\bf(\cup\ \mathop{\hbox{\bf nil/}}\nolimits\ \mathop{\hbox{\bf false/}}\nolimits)\/}}\nolimits{}}_{o}.
To illustrate, recall Example 2.6. The parameter is of type , written as a proposition. In the method, we know is , based on multimethod dispatch rules. This is written , pronounced “the path of variable is of type ()”.
To attain the type of , we must solve for in , under proposition environment which deduces to be a meal. The logical system combines pieces of type information to deduce more accurate types for lexical bindings—this is explained in Section 3.6.
Typing judgment
We formalize our system following Tobin-Hochstadt and Felleisen [24]. The typing judgment says expression rewrites to , which is of type in the proposition environment , with ‘then’ proposition , ‘else’ proposition and object .
We write to mean for some , and , and abbreviate self rewriting judgements to .
Typing rules
The core typing rules are given as Figure 3. We introduce the interesting rules with the complement number predicate as a running example.
[TABLE]
The lambda rule T-Abs introduces = {\mathop{\hbox{\bf\top\/}}\nolimits}_{d} to check the body. With = {\mathop{\hbox{\bf\top\/}}\nolimits}_{d}, T-If first checks the test = via the T-App rule, with three steps.
First, in T-App the operator = n? is checked with T-Const, which uses (Figure 7, dynamic semantics in the supplemental material) to type constants. n? is a predicate over numbers, and class returns its argument’s class.
Resuming , in T-App the operand = is checked with T-Local as
[TABLE]
which encodes the type, proposition, and object information about variables. The proposition {\overline{\mathop{\hbox{\bf(\cup\ \mathop{\hbox{\bf nil/}}\nolimits\ \mathop{\hbox{\bf false/}}\nolimits)\/}}\nolimits}}_{d} says “it is not the case that variable is of type \mathop{\hbox{\bf(\cup\ \mathop{\hbox{\bf nil/}}\nolimits\ \mathop{\hbox{\bf false/}}\nolimits)\/}}\nolimits”; {\mathop{\hbox{\bf(\cup\ \mathop{\hbox{\bf nil/}}\nolimits\ \mathop{\hbox{\bf false/}}\nolimits)\/}}\nolimits}_{d} says “ is of type \mathop{\hbox{\bf(\cup\ \mathop{\hbox{\bf nil/}}\nolimits\ \mathop{\hbox{\bf false/}}\nolimits)\/}}\nolimits”.
Finally, the T-App rule substitutes the operand’s object for the parameter in the latent type, propositions, and object. The proposition says “ is of type ”; says “it is not the case that is of type ”. The object is the symbolic representation of what the expression evaluates to.
[TABLE]
To demonstrate, the ‘then’ proposition—in T-App —substitutes the latent ‘then’ proposition of with , giving = .
To check the branches of , T-If introduces = to check = , and = to check = . 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.
[TABLE]
Finally T-Abs assigns a type to the overall function:
[TABLE]
Subtyping
Figure 4 presents subtyping as a reflexive and transitive relation with top type \mathop{\hbox{\bf\top\/}}\nolimits. Singleton types are instances of their respective classes—boolean singleton types are of type , class literals are instances of and keywords are instances of . Instances of classes are subtypes of . Function types are subtypes of . All types except for are subtypes of , so \mathop{\hbox{\bf\top\/}}\nolimits is similar to (\mathop{\hbox{\bf\bigcup\/}}\nolimits\ \mathop{\hbox{\bf nil\/}}\nolimits\ \mathop{\hbox{\bf Object\/}}\nolimits). 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 in a big-step style using an environment, following [24]. We include both errors and a value, which is provably ruled out by the type system. The main judgment is which states that evaluates to answer in environment . We chose to omit the core rules (included in supplemental material) however a notable difference is is a false value, which affects the semantics of (Figure 5).
3.2 Java Interoperability
We present Java interoperability in a restricted setting without class inheritance, overloading or Java Generics. We extend the syntax in Figure 6 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 and method calls .
In Example 2.3, (interop .getParent (interop new File "a/b" interop) interop) translates to
[TABLE]
But both the constructor and method are unresolved. We introduce non-reflective expressions for specifying exact Java overloads.
[TABLE]
From the left, the one-argument constructor for takes a , and the method of takes zero arguments and returns a .
We now walk through this conversion.
Constructors
First we check and convert to . The T-New typing rule checks and rewrites constructors. To check we first resolve the constructor overload in the class table—there is at most one to simplify presentation. With = , we convert to a nilable type the argument with = (\mathop{\hbox{\bf\bigcup\/}}\nolimits\ \mathop{\hbox{\bf nil\/}}\nolimits\ \mathop{\hbox{\bf S\/}}\nolimits) and type check against . Typed Clojure defaults to allowing non-nilable arguments, but this can be overridden, so we model the more general case. The return Java type is converted to a non-nil Typed Clojure type = 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 , or . Finally, the constructor rewrites to .
Methods
Next we convert to the non-reflective expression . The T-Method rule for unresolved methods checks . We verify the target type = is non-nil by T-New. The overload is chosen from the class table based on = —there is at most one. The nilable return type = (\mathop{\hbox{\bf\bigcup\/}}\nolimits\ \mathop{\hbox{\bf nil\/}}\nolimits\ \mathop{\hbox{\bf S\/}}\nolimits) is given, and the entire expression rewrites to expression 5.
The T-Field rule (Figure 6) is like T-Method, but without arguments.
The evaluation rules B-Field, B-New and B-Method (Figure 6) simply evaluate their arguments and call the relevant JVM operation, which we do not model—Section 4 states our exact assumptions. There are no evaluation rules for reflective Java interoperability, since there are no typing rules that rewrite to reflective calls.
3.3 Multimethod preliminaries:
We now consider the operation, a core part of the multimethod dispatch mechanism. Recalling the examples in Section 2.4, is a subclassing test for classes, but otherwise is an equality test. The T-IsA rule uses (Figure 8), a metafunction which produces the propositions for expressions.
To demonstrate the first case, the expression ( ) is true if is a keyword, otherwise false. When checked with T-IsA, the object of the left subexpression = \classpe{} (which starts with the class path element) and the type of the right subexpression = () (a singleton class type) together trigger the first case , giving propositions that correspond to our informal description = .
The second case captures the simple equality mode for non-class singleton types. For example, the expression ( ) produces true when evaluates to , otherwise it produces false. Using T-IsA, it has the propositions = since = and = (). The side condition on the second case ensures we are in equality mode—if can possibly be a class in ( ), uses its conservative default case, since if is a class literal, subclassing mode could be triggered. Capture-avoiding substitution of objects 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 is given by B-IsA (Figure 8). explicitly handles classes in the second case.
3.4 Multimethods
Figure 8 presents immutable multimethods without default methods to ease presentation. Figure 9 translates the mutable Example 2.4 to .
To check , we note creates a multimethod with interface type , and dispatch function of type , producing a value of type ( ). The T-DefMulti typing rule checks the dispatch function, and verifies both the interface and dispatch type’s domain agree. Our example checks with = , interface type = , dispatch function type = , and overall type .
Next, we show how to check . The expression () creates a new multimethod that extends multimethod ’s dispatch table, mapping dispatch value to method . The T-DefMulti typing rule checks is a multimethod with dispatch function type , 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 being of type with = (from below the arrow on the right argument of the previous type) and = (). Then = from (see Section 3.3). Since = , we check the method body with . Finally from the interface type , we know = = , and = , which also agrees with the method body, above. Notice the overall type of a is the same as its first subexpression .
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 8.
Semantics
Multimethod definition semantics are also given in Figure 8. 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 is applied to the argument to obtain the dispatch value . Based on , the metafunction (Figure 8) extracts a method from the method table and applies it to the original argument for the final result.
3.5 Precise Types for Heterogeneous maps
Figure 10 presents heterogeneous map types. The type () contains , a map of present entries (mapping keywords to types), , a set of keyword keys that are known to be absent and tag which is either (“complete”) if the map is fully specified by , and (“partial”) if there are unknown entries. The partially specified map of lunch in Example 2.5 is written () (abbreviated ). The type of the fully specified map breakfast in Example 2.5 elides the absent entries, written () (abbreviated ). To ease presentation, if an HMap has completeness tag then is elided and implicitly contains all keywords not in the domain of —dissociating keys is not modelled, so the set of absent entries otherwise never grows. Keys cannot be both present and absent.
The metavariable 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 operations on the empty map. We restrict lookup and extension to keyword keys.
How to check
A mandatory lookup is checked by T-GetHMap.
[TABLE]
The result type is , and the return object is \keype{\makekw{en}}. The object is a symbolic representation for a keyword lookup of in . The substitution for handles the case where is empty.
[TABLE]
An absent lookup is checked by T-GetHMapAbsent.
[TABLE]
The result type is —since is fully specified—with return object \keype{\makekw{bocce}}.
A lookup that is not present or absent is checked by T-GetHMapPartialDefault.
[TABLE]
The result type is \mathop{\hbox{\bf\top\/}}\nolimits—since has an unknown entry—with return object \keype{\makekw{bocce}}. Notice propositions are erased once they enter a HMap type.
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.
[TABLE]
The result type is , and the return object is \keype{\makekw{en}}. However, lookups of on (\mathop{\hbox{\bf\bigcup\/}}\nolimits\ \mathop{\hbox{\bf Bf\/}}\nolimits\mathop{\hbox{\bf Lu\/}}\nolimits) maps are unsupported. This restriction still allows us to check many of the examples in Section 2—in particular we can check Example 2.6, as is in common with both HMaps, but cannot check Example 2.6 because a meal lacks a entry. Adding a rule to handle Example 2.6 is otherwise straightforward.
Extending a map with T-AssocHMap preserves its completeness.
[TABLE]
The result type is , a complete map. T-AssocHMap also enforces to prevent badly formed types.
Subtyping
Subtyping for HMaps designate as a common supertype for all HMaps. S-HMap says that HMaps are subtypes if they agree on , 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 and are straightforward.
3.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:
[TABLE]
It says under , if object \pathelemp{} is of type , and an extension \pathelem{}\pathelemp{} is of possibly-negative type , then (, , ) is \pathelemp{}’s type under .
Recall Example 2.6. Solving uses L-Update, where = and = [].
[TABLE]
Since is a union of HMaps, we structurally recur on the first case of (Figure 12), which preserves . Each initial recursion hits the first HMap case, since there is some such that and accepts partial maps .
To demonstrate, meals are handled by the first HMap case and update to () where = (, , ) and = . updates to \mathop{\hbox{\bf\bot\/}}\nolimits via the penultimate case, because ((), ()) = \mathop{\hbox{\bf\bot\/}}\nolimits by the first case. The same happens to meals, leaving just the HMap.
In Example 2.6, updates the argument in the method. This recurs twice for each meal to handle the class path element.
We describe the other cases. The first class case updates to if class returns (). The second case detects contradictions in absent keys. The third case updates unknown entries to be mapped to or absent. The fourth case updates unknown entries to be present when they do not overlap with .
4 Metatheory
We prove type soundness following Tobin-Hochstadt and Felleisen [24]. Our model is extended to include errors and a value, and we prove well-typed programs do not go wrong; this is therefore a stronger theorem than proved by Tobin-Hochstadt and Felleisen [24]. Errors behave like Java exceptions—they can be thrown and propagate “upwards” in the evaluation rules ( 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 (other assumptions given in the supplemental material).
{assumption}
[ ] If and is consistent with then either
- •
which is consistent with ,
- •
, or
- •
is undefined.
For the purposes of our soundness proof, we require that all values are consistent. Consistency (defined in the supplemental material) 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 , and . Proofs are deferred to the supplemental material.
Lemma 1
If , , , and then either
- •
* and all of the following hold:*
either = or , 2. 2.
either and or and , 3. 3.
* for some , and , and* 4. 4.
, or
- •
.
Theorem 4.1 (Type soundness)
If and then for some , and .
5 Experience
Typed Clojure is implemented as core.typed [2], which has seen wide usage.
5.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 [22], 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 [14].
5.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 13).
feeds2imap
feeds2imap444https://github.com/frenchy64/feeds2imap.clj 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 [7] 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 [8], maintaining 87 namespaces and 19,000 lines of code, an experience we summarise in Section 5.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 2.6. 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.
5.3 Further challenges
After a 2 year trial, the second case study decided to disabled type checking [9]. 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 13, 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 [9] contains more details.
6 Related Work
Multimethods
[20] and collaborators present a sequence of systems [4, 5, 20] with statically-typed multimethods and modular type checking. In contrast to Typed Clojure, in these system methods declare the types of arguments that they expect which corresponds to exclusively using class as the dispatch function in Typed Clojure. However, Typed Clojure does not attempt to rule out failed dispatches.
Record Types
Row polymorphism [26, 3, 12], used in systems such as the OCaml object system, provides many of the features of HMap types, but defined using universally-quantified row variables. HMaps in Typed Clojure are instead designed to be used with subtyping, but nonetheless provide similar expressiveness, including the ability to require presence and absence of certain keys.
Dependent JavaScript [6] can track similar invariants as HMaps with types for JS objects. They must deal with mutable objects, they feature refinement types and strong updates to the heap to track changes to objects.
TeJaS [16], another type system for JavaScript, also supports similar HMaps, with the ability to record the presence and absence of entries, but lacks a compositional flow-checking approach like occurrence typing.
Typed Lua [18] has table types which track entries in a mutable Lua table. Typed Lua changes the dynamic semantics of Lua to accommodate mutability: Typed Lua raises a runtime error for lookups on missing keys—HMaps consider lookups on missing keys normal.
Java Interoperability in Statically Typed Languages
Scala [21] has nullable references for compatibility with Java. Programmers must manually check for null as in Java to avoid null-pointer exceptions.
Other optional and gradual type systems
Several other gradual type systems have been developed for existing dynamically-typed languages. Reticulated Python [25] is an experimental gradually typed system for Python, implemented as a source-to-source translation that inserts dynamic checks at language boundaries and supporting Python’s first-class object system. Clojure’s nominal classes avoids the need to support first-class object system in Typed Clojure, however HMaps offer an alternative to the structural objects offered by Reticulated. Similarly, Gradualtalk [1] offers gradual typing for Smalltalk, with nominal classes.
Optional types have been adopted in industry, including Hack [10], and Flow [11] and TypeScript [19], two extensions of JavaScript. These systems support limited forms of occurrence typing, and do not include the other features we present.
7 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.
The reference list from the paper itself. Each links out to its DOI / PubMed record.
- 1[1] Allende, E., Callau, O., Fabry, J., Tanter, É., Denker, M.: Gradual typing for Smalltalk. Science of Computer Programming 96, 52–69 (2014)
- 2[2] Bonnaire-Sergeant, A., contributors: core.typed, https://github.com/clojure/core.typed
- 3[3] Cardelli, L., Mitchell, J.C.: Operations on records. In: Mathematical Structures in Computer Science. pp. 3–48 (1991)
- 4[4] Chambers, C.: Object-oriented multi-methods in Cecil. In: Proc. ECOOP (1992)
- 5[5] Chambers, C., Leavens, G.T.: Typechecking and modules for multi-methods. In: Proc. OOPSLA (1994)
- 6[6] Chugh, R., Herman, D., Jhala, R.: Dependent types for Java Script. In: Proc. OOPSLA (2012)
- 7[7] Circle CI: Circle CI, https://circleci.com
- 8[8] Circle CI: Why we’re supporting Typed Clojure, and you should too! (September 2013), http://blog.circleci.com/supporting-typed-clojure/