2 2. Overview of Typed Scheme The goal of the Typed Scheme project is to develop an explicit type system that easily accommodates a conventional Scheme programming style. Ideally, programming in Typed Scheme should feel like programming in PLT Scheme, except for
2 2. Overview of Typed Scheme The goal of the Typed Scheme project is to develop an explicit type system that easily accommodates a conventional Scheme programming style. Ideally, programming in Typed Scheme should feel like programming in PLT Scheme, except for typed function and structure signatures plus type definitions. Few other changes should be required when going from a Scheme program to a Typed Scheme program. Furthermore, the addition of types should require a relatively small effort, compared to the original program. This requires that macros, both those used and defined in the typed program, must be supported as much as possible. Supporting this style of programming demands a significant rethinking of type systems. Scheme programmers reason about their programs, but not with any conventional type system in mind. They superimpose on their untyped syntax whatever type (or analysis) discipline is convenient. No existing type system could cover all of these varieties of reasoning. Consider the following function defintion: 1 ;; data definition: a Complex is either ;; - a Number or ;; - (cons Number Number) ;; Complex Number (define (creal x) (cond [(number? x) x] [else (car x)])) As the informal data definition states, complex numbers are represented as either a single number, or a pair of numbers (cons). The definition illustrates several key elements of the way that Scheme programmers reason about their programs: ad-hoc type specifications, true union types, and predicates for type testing. No datatype specification is needed to introduce a sum type on which the function operates. Instead there is just an informal data definition and contract (Felleisen et al. 2001), which gives a name to a set of pre-existing data, without introducing new constructors. Further, the function does not use pattern matching to dispatch on the union type. All it uses is a predicate that distinguishes the two cases: the first cond clause, which deals with x as a number and the second one, which treats it as a pair. Here is the corresponding Typed Scheme code: 2 (define-type-alias Cplx ( S Number (cons Number Number))) (define: (creal [x : Cplx]) : Number (cond [(number? x) x] [else (car x)])) This version explicates both aspects of our informal reasoning. The type Cplx is an abbreviation for the true union intended by the programmer; naturally, it is unnecessary to introduce type abbreviations like this one. Furthermore, the body of creal is not modified at all; Typed Scheme type-checks each branch of the conditional appropriately. In short, only minimal type annotations are required to obtain a typed version of the original code, in which the informal, unchecked comments become statically-checked design elements. More complex reasoning about the flow of values in Scheme programs is also accomodated in our design: (foldl scene+rectangle empty-scene (filter rectangle? list-of-shapes)) 1 Standards-conforming Scheme implementations provide a complex number datatype directly. This example serves only expository purposes. 2 In this paper, we typeset Typed Scheme code in a manner that differs slightly from what programmers enter into an editor. This code selects all the rectangles from a list of shapes, and then adds them one by one to an initially-empty scene, perhaps being prepared for rendering to the screen. Even though the initial listof-shapes may contain shapes that are not rectangles, those are removed by the filter function. The resulting list contains only rectangles, and is an appropriate argument to scene+rectangle. This example demonstrates a different mode of reasoning than the first; here, the Scheme programmer uses polymorphism and the argument-dependent invariants of filter to ensure correctness. No changes to this code are required for it to typecheck in Typed Scheme. The type system is able to accommodate both modes of reasoning the programmer uses with polymorphic functions and occurrence typing. In contrast, a more conventional type system would require the use of an intermediate data structure, such as an option type, to ensure conformance. 2.1 Other Type System Features In order to support Scheme idioms and programming styles, Typed Scheme supports a number of type system features that have been studied previously, but rarely found in a single, full-fledged implementation. Specifically, Typed Scheme supports true union types (Pierce 1991), as seen above. It also provides first-class polymorphic functions, known as impredicative polymorphism, a feature of the Glasgow Haskell Compiler (Vyt