Source-linked AI summary
The Design and Implementation of Typed Scheme: From Scripts to Programs
Sam Tobin-Hochstadt, Matthias Felleisen
TL;DR
Untyped scripts become difficult to maintain because programmers must recover lost design information when changing them. The paper presents Typed Scheme, whose occurrence-typing-based system is formalized and proved sound, implemented with several complementary type features, and evaluated through examples and existing-code experiments. The authors report that typing thousands of lines of Scheme appears feasible, while dynamic enforcement and complex macros remain limitations.
Problem
Untyped scripting languages lack explicit type annotations, making programmers recover design information when modifying growing programs.
Method
Typed Scheme combines occurrence typing with true unions, subtyping, recursive types, polymorphism, local inference, and predicate-based refinement types.
Results
Experiments on existing Scheme code are described as promising and suggest that converting untyped scripts into well-typed programs is feasible.
Takeaways & Limitations
Occurrence typing supports static verification of arbitrary property checking while accommodating Scheme programming idioms with minimal code changes.
Takeaways & Limitations
Some types cannot yet be dynamically enforced, and code using the most complex PLT Scheme macros cannot be typechecked.
Abstract
from arXiv · showhide
When scripts in untyped languages grow into large programs, maintaining them becomes difficult. A lack of explicit type annotations in typical scripting languages forces programmers to must (re)discover critical pieces of design information every time they wish to change a program. This analysis step both slows down the maintenance process and may even introduce mistakes due to the violation of undiscovered invariants. This paper presents Typed Scheme, an explicitly typed extension of PLT Scheme, an untyped scripting language. Its type system is based on the novel notion of occurrence typing, which we formalize and mechanically prove sound. The implementation of Typed Scheme additionally borrows elements from a range of approaches, including recursive types, true unions and subtyping, plus polymorphism combined with a modicum of local inference. The formulation of occurrence typing naturally leads to a simple and expressive version of predicates to describe refinement types. A Typed Scheme program can use these refinement types to keep track of arbitrary classes of values via the type system. Further, we show how the Typed Scheme type system, in conjunction with simple recursive types, is able to encode refinements of existing datatypes, thus expressing both proposed variations of refinement types.
1 Type Refactoring: From Scripts to Programs
Typed Scheme addresses the maintenance and migration challenges of growing untyped Scheme programs by combining explicit typing with mechanisms suited to Scheme programming idioms. Its formal system is proved sound, implemented for PLT Scheme, and preliminarily evaluated on thousands of lines of untyped code.
- Untyped scripts lose design information, forcing programmers to recover it when changing code and making long-term maintenance difficult.
- Typed Scheme is an explicitly typed version of PLT Scheme designed to support scripts, libraries, and large operating-system-like programs.PLT Scheme was chosen partly because it is widely used as a scripting language and has a large existing codebase.
- Occurrence typing is combined with subtyping, recursive types, polymorphism, and limited inference to accommodate idiomatic PLT Scheme code.
- Predicates such as even? can define lightweight refinement types for subsets of existing types without implication or inclusion checking.
- A formal model of occurrence typing is proved type-sound, and preliminary experience adding types to thousands of lines suggests migration is feasible.
2 Overview of Typed Scheme
Typed Scheme adapts typing to Scheme’s flow-oriented and idiomatic programming style through occurrence typing, unions, polymorphism, recursive types, and predicate-based refinements. Examples show that common code can typecheck with minimal changes, while complex macros and subtle invariants remain boundaries.
- Scheme programmers use ad-hoc specifications, true unions, and predicates rather than declared sum types and pattern matching.
- Typed Scheme represents informal unions explicitly while preserving the original function body, requiring only minimal annotations.
- Occurrence typing assigns branch-specific types, allowing original Scheme code to typecheck without changes or intermediate option types.
- Refinement types describe subsets of conventional types, and Typed Scheme represents them using simple Scheme predicates.
- Typed Scheme combines true unions, first-class polymorphism, explicit recursive types, and PLT Scheme-compatible base types.
- Typed Scheme gives precise types to S-expressions and fixed-length lists through explicit cons-cell and recursive-type representations.
- Some invariants, such as those embedded in unstructured XML S-expressions, are too subtle for the type system and remain in untyped code.
- Macro expansion handles almost all simple macros and many complex ones, but the largest macros with their own invariants do not scale to this approach.
3 Two Examples of Refinements
Typed Scheme uses predicate-based refinements to verify validated inputs and recursive types to encode structured subsets of data. The examples demonstrate both practical security-oriented checking and expressive encodings of restricted grammars.
- Form validation: Predicate-based refinement types statically verify that only validated strings are passed to a database, addressing SQL injection risks from unsanitized input.
- Form validation: A Typed Scheme predicate becomes a refinement type through declare-refinement, changing its type to recognize acceptable values.
- Form validation: The query function accepts a string refined by sql-safe? and returns a list of results, while the refinement remains usable as a String.
- Form validation: Sanitize returns a sql-safe? refinement and checks the predicate after escaping, while only sql-safe? enters the trusted computing base.
- Restricted grammars: Recursive types encode IntList and its NonEmpty subset, with NonEmpty established as a subtype of IntList.
- Restricted grammars: Typed Scheme encodes partitioned CPS terms by distinguishing user-value and continuation variables and defining recursive term categories.
- Restricted grammars: The resulting CPS types are subtypes of the general term type, allowing typeful compiler functions to interoperate with functions accepting arbitrary terms.
4 A Formal Model of Typed Scheme
The λTS calculus models occurrence typing with unions, subtyping, predicates, and conditional refinement, then establishes its preservation, progress, and soundness properties.
- 4 A Formal Model of Typed Scheme: λTS formalizes occurrence typing alongside true unions and subtyping, while separating proof-only rules from the implementation-facing typing rules.The calculus models the primary novel feature and supports a mechanically verified soundness result.
- 4.1 Syntax and Operational Semantics: Expressions include values, variables, applications, and conditionals; types include top, functions, base types, and finite unions.Function types carry latent predicates, while evaluation contexts specify reduction positions.
- 4.1 Syntax and Operational Semantics: Auxiliary environment operations restrict or remove types using predicate information, while combpred combines the effects of conditional tests and branches.These operations support the type-environment changes required by conditional typing.
- 4.2 Preliminaries: Occurrence typing assigns distinct types to variable occurrences according to control flow, allowing a union such as Number ∪ Boolean to split across conditional branches.Predicate information can propagate through programmer-defined functions via latent predicate annotations.
- 4.3 Typing Rules: Scheme-style conditionals accept tests of any type and use visible predicates to refine the environments checked for the then and else branches.A variable test is treated as non-false in the then branch and false in the else branch.
- 4.4 Proof-Technical Typing Rules: The proof-technical extension handles reduced terms whose unreachable branches are ill-typed under the primary rules, using visible false predicates to disregard those branches.This addresses intermediate terms needed for a Wright–Felleisen-style soundness proof.
- 4.4 Proof-Technical Typing Rules: The calculus proves progress and soundness: a closed well-typed term is either a value or can reduce, and otherwise reduces forever or to a suitably typed value.The soundness theorem applies to terms typed with the primary rules and a base result type.
5 Formalizing Refinements
Typed Scheme extends the calculus with built-in-function refinements, integrates them into subtyping and typing, and preserves soundness by erasing refinements to ordinary types. The extension expresses parity-based constraints while retaining ordinary use of refined values.
- 5 Formalizing Refinements: Refinement types use the constructor (R c τ), where a built-in function c defines a refinement over argument type τ.The implemented system infers τ from c's type.
- 5 Formalizing Refinements: Refinement subtyping adds an environment of permitted built-ins and makes each refinement a subtype of its underlying type.The judgement becomes ∆⊢r τ1 <: τ2, and ∆⊢r (R c τ) <: τ follows from the new rule.
- 5 Formalizing Refinements: The typing judgement is extended with the refinement environment, but no additional typing rules are required for refined expressions.Expressions of type (R c τ) can still be used as τ, so standard arithmetic applies to even and odd numbers.
- 5 Formalizing Refinements: The constants even? and odd? support functions that apply an even-consuming function exactly when a number is even.The example tests even? n and otherwise returns n.
- 5.1 Soundness: Refinement types add no further error prevention under the calculus's existing soundness semantics, and this remains true even if errors such as division by zero are added.The paper therefore changes the proof strategy rather than claiming stronger operational exclusion.
- 5.1 Soundness: Erasure maps every refinement (R c τ) to τ and extends to terms, predicates, environments, judgements, and primitive semantics.The erased program is intended to remain typeable and reduce appropriately.
- 5.1 Soundness: The erased-term typing lemma establishes that a refinement-typed term remains typable after erasure, enabling combination with preservation and progress.These lemmas provide the bridge to the extended soundness theorem.
- 5.1 Soundness: For closed terms with base or refined-base result types, soundness guarantees divergence or reduction to a value whose erased type and predicate satisfy the required relations.The theorem uses erased subtyping and erased visible-predicate relations.
6 From λTS To Typed Scheme
Typed Scheme extends the λTS core into a practical language that supports Scheme idioms, polymorphism, recursive types, local inference, and refinement-oriented predicates. Its examples show that occurrence typing and inference can preserve useful types without requiring extensive annotations.
- Type-system extensions: Typed Scheme integrates occurrence typing with polymorphism, recursive types, subtyping, and local inference for Scheme-style programming.The implementation extends the λTS core with features intended to accommodate idiomatic Scheme code.
- Polymorphism and inference: Polymorphic map explicitly quantifies over type variables, while recursive calls infer appropriate instantiations without type applications.The body remains identical to the untyped definition, including its recursive call.
- Recursive types: Recursive types represent regular S-expression structures, and Typed Scheme automatically folds and unfolds their instances.Binary trees over cons cells are presented as an example using an explicit recursive type alias.
- Local inference: Local inference handles non-recursive bindings and omitted polymorphic type arguments, although subtyping can make inference fail.When inference fails, programmers must sometimes annotate arguments or functions; in practice, such annotations are rarely needed.
- Scheme integration: Typed Scheme adapts major Scheme constructs, including structures, multiple values, and typed-module interoperability, while automatically guarding typed exports with contracts.A limitation is that macros defined in typed modules cannot currently be imported into an untyped context.
- Refinement and predicates: Predicates such as number? refine existing types, allowing filtering a mixed list to produce a value typed as (Listof Number).The type of filter carries the predicate’s latent predicate information into the resulting element type.
7 Implementation
Typed Scheme is implemented as a macro-based layer over PLT Scheme, integrating type checking with expansion and preserving module interoperability. The implementation has low overhead for purely typed execution, but contracts and complex macros remain important limitations.
- Implementation strategy: Typed Scheme is implemented as a full-featured language layer over PLT Scheme using its macro system.The implementation includes the standard library and was distributed with PLT Scheme.
- Expansion and checking: Type checking is integrated with macro expansion by redefining #%module-begin and reporting ill-typed modules at expansion time.The macro implementation expands programs before type checking, reducing the remaining language to PLT Scheme core forms.
- Modules: Persistent reified type environments allow separately expanded modules to recreate the information needed for cross-module type checking.Identifier keys preserve module-origin information and support standard PLT Scheme tools.
- Performance: The typechecker is slower than macro expansion alone but typechecks even large files in a few seconds after substantial optimization.Interning type representations enables constant-time type comparison and reduces memory use.
- Performance: Contract overhead can be substantial and may change asymptotic complexity, but it occurs only across typed-untyped boundaries; selected DrScheme code showed no measurable slowdown.Purely typed programs incur no runtime overhead beyond loading library code, so typed code executes at full speed.
- Limitations: The implementation cannot dynamically enforce some types, including variable-arity polymorphism and some mutable-data contracts.More types may become dynamically enforceable as the PLT Scheme contract system gains corresponding support.
- Limitations: Typed Scheme cannot typecheck code using the most complex PLT Scheme macros, including the unit and class systems.These macros maintain invariants that would require substantially more type-system complexity or special handling.
8 Practical Experience
Typed Scheme was tested by porting educational code, libraries, and sizable applications, generally requiring annotations and targeted changes to preserve or check invariants. The experiments suggest that converting existing PLT Scheme programs is feasible, though some external-data invariants remained outside the type system.
- Educational code: Educational code usually required only function-header type declarations, but some S-expression invariants could not be expressed.This limitation appeared in both textbook programs and undergraduate course solutions.
- Evaluation scope: The evaluation covered educational programs, data-structure libraries, a 2,700-line game, and a 500-line checkbook script.The game comprised 10 modules and included 500 lines of unit tests.
- Applications: A complex game function required changes confined to its header, while local variable types were inferred from definition bodies.The added header included parameter and multiple-return-value annotations.
- Applications: The game’s external XML-format invariant was unchecked and unspecified, so its handling moved to an untyped module of fewer than 50 lines accessed through require/typed.The typed portion therefore relied on a typed–untyped module boundary for this data.
- Applications: The checkbook script added input-format checks and maintained a data-structure typing invariant by construction rather than after-the-fact mutation.The authors regarded the typechecker-mandated change as an improvement despite the program’s prior successful use.
9 Related Work
Related work positions Typed Scheme between soft typing, gradual typing, flow analysis, and refinement-type systems. Its distinguishing approach combines explicit annotations with occurrence-sensitive reasoning and predicate-based refinements that avoid theorem-prover-based implication checking.
- Soft typing: Soft typing aims to infer types without declarations and avoid preventing programs from running, but its systems can be complex, brittle, and difficult to explain.Reported problems include very large inferred types and major type changes after small syntactic edits.
- Soft typing: Typed Scheme’s evaluation suggests that explicit annotations and rejecting programs can pinpoint errors more clearly than conservative soft-typing systems.The authors also report that programmers can convert entire modules with few declarations and function-header annotations.
- Occurrence typing: Occurrence typing generalizes predicate-based case analysis beyond simple typecase constructs, supporting existing Scheme code that was not written with typecase.Its motivation is connected to Scheme programmers’ combination of flow-oriented and type-based reasoning.
- Gradual and integrated typing: Typed Scheme supports integration of typed and untyped code while running as a PLT Scheme library, unlike related Ruby work requiring a new interpreter.The comparison also notes that the Ruby system lacked a published soundness theorem at the time described.
- Refinement types: Its predicate-style refinements use in-language predicates, permit any computable set as a refinement, and do not decide implication between predicates.This design avoids depending on a theorem prover.
10 Conclusion
The paper concludes that Typed Scheme demonstrates a feasible migration path from untyped scripts to typed programs by accommodating the idioms of PLT Scheme. Its occurrence-typing design supports refinement checking, and the implementation and experiments provide an initial evaluation of that approach.
- Conclusion: The paper presents migration from untyped to typed languages as an important problem and demonstrates an approach based on accommodating scripting-language idioms.The conclusion frames this as one successful approach rather than a universal solution.
- Conclusion: Occurrence typing assigns distinct subtypes to parameter occurrences according to control flow and enables static verification of arbitrary property checking.The design combines this idea with previously studied type-system features and supports a simple, expressive refinement form.
- Implementation: Typed Scheme was implemented and distributed as a PLT Scheme package with core type-system features and integration support for the surrounding system.The package includes the interoperation features needed to work with the rest of PLT Scheme.
- Evaluation: The authors regard the section 8 experiments as illustrative of existing code and consider their success a good predictor for future experiments.They planned further library ports and deeper study of occurrence typing.