Programmers reason about their programs using a wide variety of formal and informal methods. Programmers in untyped languages such as Scheme or Erlang are able to use any such method to reason about the type behavior of their programs. Our type system for Scheme accommodates common reasoning methods by assigning variable occurrences a subtype of their declared type based on the predicates prior to the occurrence, a discipline dubbed occurrence typing. It thus enables programmers to enrich existing Scheme code with types, while requiring few changes to the code itself. Three years of practical experience has revealed serious shortcomings of our type system. In particular, it relied on a system of ad-hoc rules to relate combinations of predicates, it could not reason about subcomponents of data structures, and it could not follow sophisticated reasoning about the relationship among predicate tests, all of which are used in existing code. In this paper, we reformulate occurrence typing to eliminate these shortcomings. The new formulation derives propositional logic formulas that hold when an expression evaluates to true or false, respectively. A simple proof system is then used to determine types of variable occurrences from these propositions. Our implementation of this revised occurrence type system thus copes with many more untyped programming idioms than the original system.  Keywords Type systems, Untyped languages, Logic Developing programs in a typed language helps programmers avoid mistakes. It also forces them to provide some documentation, and it establishes some protective abstraction barriers. As such, the type system imposes a discipline on the programming process. Nevertheless, numerous programmers continue to choose untyped scripting languages for their work, including many who work in a functional style. When someone eventually decides that explicitly stated type information reduces maintenance cost, they face a * This research was partially supported by grants from the US NSF and a donation from the Mozilla Foundation. Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. To copy otherwise, to republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. ICFP'10, September 27-29, 2010, Baltimore, Maryland, USA. Copyright c 2010 ACM 978-1-60558-794-3/10/09. . . $10.00 dilemma. To address this situation, we need to develop typed sister languages for untyped languages. With those, programmers can enrich existing programs with type declarations as needed while maintaining smooth interoperability. A type system for an existing untyped language must accommodate the existing programming idioms in order to keep the cost of type enrichment low. Otherwise, type enrichment requires changes to code, which may introduce new mistakes. Put positively, the ideal typed sister language requires nothing but the addition of type specifications to function headers, structure definitions, etc. Our experience shows that programming idioms in untyped functional languages rest on a combination of traditional typebased reasoning with reasoning about control flow. In particular, conditionals and data-type predicates are used to establish the nature of variables' values, and based on this flow-sensitive reasoning, programmers use variables at more specific types than expected. Put differently, the programmer determines the type of each variable occurrence based on the predicates that flow-dominate it. Multiple researchers over the decades have discovered this insight. In his paper on the static analysis of untyped programs, Reynolds [1968] notes that such reasoning is necessary, stating that in future systems, "some account should be taken of the premises in conditional expressions." In his work on TYPED LISP, Cartwright [1976, §5] describes having to abandon the policy of rejecting typeincorrect programs because the variables in conditionals had overly broad types. Similarly, in their paper on translating Scheme to ML, Henglein and Rehof [1995] state "type testing predicates aggravate the loss of static type information since they are typically used to steer the control flow in a program in such a fashion that execution depends on which type tag an object has at run-time." We exploited this insight for the development of Typed Scheme, a typed sister language for Racket (formerly PLT Scheme) [TobinHochstadt and Felleisen 2008]. Its type system combines several preexisting elements-"true" recursive union types, subtyping, polymorphism-with the novel idea of occurrence typing, 1 a type discipline for exploiting the use of data-type predicates in the test expression of conditionals. Thus, if a test uses (number? x), the type system uses the type Number for x in the then branch and the declared type of x, minus Number, otherwise. Three years of extensive use have revealed several shortcomings in our original design. One significant problem concerns control flow governed by logical combinations (e.g., and, or, not) of predicate tests. Another is that the type system cannot track uses of predicates applied to structure selectors such as car. This lack of expressiveness in the type system is due to fundamental limitations. First, our original system does not consider asymmetries between the then and else branches of conditionals. For example, when the expression (and (number? x) (> x 100)) is true, the type system should know that x is a number, but x might or 1 Komondoor et al. [2005] independently coined the term "occurrence typing" in the context of providing an advanced type system for COBOL. might not be a number when the expression is false, since it might be 97 or "Hello". Second, the type system does not appropriately distinguish between selector expressions such as (car x) and predicate expressions such as (number? x). Third, the treatment of combinations of tests relies on an ad-hoc collection of rules. In this paper, we present a new and simple framework for occurrence typing that eliminates all three problems via an increase in expressive power. The key innovation is to turn control flow predicates into formulas in propositional logic for reasoning about the types of variables. The atomic propositions include statements that a particular variable has a particular type, replacing the previous collection of special cases with textbook rules of logical inference. This new design allows the type system to reason about combinations of predicates: (cond [(and (number? (node-left x)) (string? (node-right y))) ;; known: (node-right y) is a string, (node-left x) is a number . Now the programmer and the revised type system both determine that since (number? (node-left x)) is true in the second clause, (string? (node-right y)) must be false, and thus, (node-right y) is not a string. Using propositional logic to reason about predicates handles this and many other similar situations. Beyond the new type system, this paper contributes: • a full-fledged implementation of the calculus, now known as Typed Racket, addressing the full complexities of the functional core of Racket, such as mutable data and multiple arguments; • an empirical study of the usefulness of our extensions; and • a novel model-theoretic proof technique for type soundness. The paper begins with a brief review of the essence of occurrence typing with an emphasis on programming idioms that our original system cannot typecheck. We then describe the new system in a semi-formal manner. In the three following sections, we describe the system formally: first the core system of occurrence typing, then several extensions demonstrating the expressiveness of the system, and third the proof of soundness. These sections are followed by a description of our implementation strategy and empirical measures of its usefulness on existing code. Finally, we discuss related work and conclude.
Typed Racket's occurrence typing narrows the type of unions based on control dominating type tests, and its latent predicates lift the results of tests across higher-order functions REF .
Logical types for untyped languages
ICFP '10
Computer Science