The component-by-component migration of a program from untyped to typed can trigger unintended performance degradations. When such a degradation occurs, typing well-chosen components can lessen the cost of type enforcement, while typing poorly chosen components can exacerbate it. This article examines whether off-the-shelf profiling tools deliver information that is an effective guide for navigating these migration choices in Typed Racket. Using the rational-programmer method, the article tests this hypothesis with an experiment that involves tens of thousands of performance-debugging scenarios, two different profiler types, and 23 strategies that convert profiler output to migration choices. The most effective strategy relies on a boundary profiler to identify the costliest inter-component boundary and then adds deeply enforced types to both sides. When the output of this profiler fails to identify a boundary, the strategy takes a random migration step—similar to the way many computational approaches resort temporarily to random choices to avoid getting stuck. The strategy completely eliminates the cost of run-time type checks in more than half of the scenarios if at most two performance degradations are tolerable along the way.

Abstract Actor languages realize concurrency via message passing, which most of the time is easy to use. Empirical code inspection provides evidence, however, that on occasion, programmers wish to have an actor share some of its state with others. The dataspace model adds a tightly controlled state-exchange mechanism, dubbed dataspace, to the actor model for just this purpose. Experience with dataspaces suggests that this form of sharing calls for linguistic constructs that allow programmers to state temporal aspects of actor conversations. In response, this paper presents the facet notation: its theory, its type system, its behavioral type system, and some first experiences with an implementation.

Software contracts empower programmers to describe functional properties of components. When it comes to constraining effects, though, the literature offers only one-off solutions for various effects. It lacks a universal principle. This paper presents the design of an effectful contract system in the context of effect handlers. A key metatheorem shows that contracts cannot unduly interfere with a program’s execution. An implementation of this design, along with an evaluation of its generality, demonstrates that the theory can guide practice.

Abstract Behavioral software contracts allow programmers to strengthen the obligations and promises that they express with conventional types. They lack expressive power, though, when it comes to invariants that hold across several function calls. Trace contracts narrow this expressiveness gap. A trace contract is a predicate over the sequence of values that flow through function calls and returns. This paper presents a principled design, an implementation, and an evaluation of trace contracts.

Sound migratory typing envisions a safe and smooth refactoring of untyped code bases to typed ones. However, the cost of enforcing safety with run-time checks is often prohibitively high, thus performance regressions are a likely occurrence. Additional types can often recover performance, but choosing the right components to type is difficult because of the exponential size of the migratory typing lattice. In principal though, migration could be guided by off-the-shelf profiling tools. To examine this hypothesis, this paper follows the rational programmer method and reports on the results of an experiment on tens of thousands of performance-debugging scenarios via seventeen strategies for turning profiler output into an actionable next step. The most effective strategy is the use of deep types to eliminate the most costly boundaries between typed and untyped components; this strategy succeeds in more than 50% of scenarios if two performance degradations are tolerable along the way.

Equipping an existing programming language with a gradual type system requires two major steps. The first and most visible one in academia is to add a notation for types and a type checking apparatus. The second, highly practical one is to provide a type veneer for the large number of existing untyped libraries; doing so enables typed components to import pieces of functionality and get their uses type-checked, without any changes to the libraries. When programmers create such typed veneers for libraries, they make mistakes that persist and cause trouble. The question is whether the academically investigated run-time checks for gradual type systems assist programmers with debugging such mistakes. This paper provides a first, surprising answer to this question via a rational-programmer investigation: run-time checks alone are typically less helpful than the safety checks of the underlying language. Combining Natural run-time checks with blame, however, provides significantly superior debugging hints.

The literature presents many strategies for enforcing the integrity of types when typed code interacts with untyped code. This article presents a uniform evaluation framework that characterizes the differences among some major existing semantics for typed–untyped interaction. Type system designers can use this framework to analyze the guarantees of their own dynamic semantics.

Programming language theoreticians develop blame assignment systems and prove blame theorems for gradually typed programming languages. Practical implementations of gradual typing almost completely ignore the idea of blame assignment. This contrast raises the question whether blame provides any value to the working programmer and poses the challenge of how to evaluate the effectiveness of blame assignment strategies. This paper contributes (1) the first evaluation method for blame assignment strategies and (2) the results from applying it to three different semantics for gradual typing. These results cast doubt on the theoretical effectiveness of blame in gradual typing. In most scenarios, strategies with imprecise blame assignment are as helpful to a rationally acting programmer as strategies with provably correct blame.

Abstract Actors collaborate via message exchanges to reach a common goal. Experience has shown, however, that pure message-based communication is limiting and forces developers to use design patterns. The recently introduced dataspace actor model borrows ideas from the tuple space realm. It offers a tightly controlled, shared storage facility for groups of actors. In this model, actors assert facts that they wish to share and interests in such assertions. The dataspace notifies interested parties of changes to the set of assertions that they are interested in. Although it is straightforward to add the dataspace model to untyped languages, adding a typed interface is both necessary and challenging. Without restrictions on exchanged data, a faulty actor may propagate erroneous data through a malformed assertion, causing an otherwise well-behaved actor to crash—violating the key principle of failure isolation. A properly designed type system can prevent this scenario and rule out other kinds of uncooperative actors. This paper presents the first structural type system for the dataspace model of actors; it does not address the question of behavioral types for assertion-oriented protocols.

Many programming problems call for turning geometrical thoughts into code: tables, hierarchical structures, nests of objects, trees, forests, graphs, and so on. Linear text does not do justice to such thoughts. But, it has been the dominant programming medium for the past and will remain so for the foreseeable future. This paper proposes a novel mechanism for conveniently extending textual programming languages with problem-specific visual syntax. It argues the necessity of this language feature, demonstrates the feasibility with a robust prototype, and sketches a design plan for adapting the idea to other languages.

Macros provide a powerful means of extending languages. They have proven useful in both general-purpose and domain-specific programming contexts. This paper presents an architecture for implementing macro-extensible DSLs on top of macro-extensible host languages. The macro expanders of these DSLs inherit the syntax system, hygienic expansion, and more from the host. They transform the extensible DSL syntax into a DSL core language. This arrangement has several important consequences. It becomes straightforward to integrate the syntax of various DSLs and the host language when their expanders share these inherited components. Also, a DSL compiler may be designed around a fixed core language, even for an extensible DSL. Finally, macros empower programmers to safely grow DSLs on their own and tailor them to their needs.

Abstract A sound gradual type system ensures that untyped components of a program can never break the guarantees of statically typed components. This assurance relies on runtime checks, which in turn impose performance overhead in proportion to the frequency and nature of interaction between typed and untyped components. The literature on gradual typing lacks rigorous descriptions of methods for measuring the performance of gradual type systems. This gap has consequences for the implementors of gradual type systems and developers who use such systems. Without systematic evaluation of mixed-typed programs, implementors cannot precisely determine how improvements to a gradual type system affect performance. Developers cannot predict whether adding types to part of a program will significantly degrade (or improve) its performance. This paper presents the first method for evaluating the performance of sound gradual type systems. The method quantifies both the absolute performance of a gradual type system and the relative performance of two implementations of the same gradual type system. To validate the method, the paper reports on its application to 20 programs and 3 implementations of Typed Racket.

In the context of gradual typing, type soundness guarantees the safety of typed code. When untyped code fails to respect types, a runtime check finds the discrepancy. As for untyped code, type soundness makes no promises; it does not protect untyped code from mistakes in type specifications and unwarranted blame. To address the asymmetry, this paper adapts complete monitoring from the contract world to gradual typing. Complete monitoring strengthens plain soundness into a guarantee that catches problems with faulty type specifications. Furthermore, a semantics that satisfies complete monitoring can easily pinpoint the conflict between a type specification and a value. For gradual typing systems that fail complete monitoring, the technical framework provides a source-of-truth to assess the quality of blame.

While high-level languages come with significant readability and maintainability benefits, their performance remains difficult to predict. For example, programmers may unknowingly use language features inappropriately, which cause their programs to run slower than expected. To address this issue, we introduce feature-specific profiling , a technique that reports performance costs in terms of linguistic constructs. Feature-specific profilers help programmers find expensive uses of specific features of their language. We describe the architecture of a profiler that implements our approach, explain prototypes of the profiler for two languages with different characteristics and implementation strategies, and provide empirical evidence for the approach’s general usefulness as a performance debugging tool.

The literature on gradual typing presents three fundamentally different ways of thinking about the integrity of programs that combine statically typed and dynamically typed code. This paper presents a uniform semantic framework that explains all three approaches, illustrates how each approach affects a developer's work, and adds a systematic performance comparison for a single implementation platform.

The Racket doctrine tells developers to narrow the gap between the terminology of a problem domain and general programming constructs by creating languages instead of just plain programs. This pearl illustrates this point with the creation of a relatively simple domain-specific language for editing videos. To produce the video proceedings of a conference, for example, video professionals traditionally use "non-linear" GUI editors to manually edit each talk, despite the repetitive nature of the process. As it turns out, video editing naturally splits the work into a declarative phase and an imperative rendering phase at the end. Hence it is natural to create a functional-declarative language for the first phase, which reduces a lot of manual labor. This user-facing DSL utilizes a second, internal DSL to implement the second phase, which is an interface to a general, low-level C library. Finally, we inject type checking into our language via another DSL that supports programming in the language of type formalisms. In short, the development of the video editing language cleanly demonstrates how the Racket doctrine naturally leads to the creation of language hierarchies, analogous to the hierarchies of modules found in conventional functional languages.

Contracts feel misunderstood, especially those with a higher-order soul. While software engineers appreciate contracts as tools for articulating the interface between components, functional programmers desperately search for their types and meaning, completely forgetting about their pragmatics.

Programmers have come to embrace dynamically-typed languages for prototyping and delivering large and complex systems. When it comes to maintaining and evolving these systems, the lack of explicit static typing becomes a bottleneck. In response, researchers have explored the idea of gradually-typed programming languages which allow the incremental addition of type annotations to software written in one of these untyped languages. Some of these new, hybrid languages insert run-time checks at the boundary between typed and untyped code to establish type soundness for the overall system. With sound gradual typing, programmers can rely on the language implementation to provide meaningful error messages when type invariants are violated. While most research on sound gradual typing remains theoretical, the few emerging implementations suffer from performance overheads due to these checks. None of the publications on this topic comes with a comprehensive performance evaluation. Worse, a few report disastrous numbers. In response, this paper proposes a method for evaluating the performance of gradually-typed programming languages. The method hinges on exploring the space of partial conversions from untyped to typed. For each benchmark, the performance of the different versions is reported in a synthetic metric that associates runtime overhead to conversion effort. The paper reports on the results of applying the method to Typed Racket, a mature implementation of sound gradual typing, using a suite of real-world programs of various sizes and complexities. Based on these results the paper concludes that, given the current state of implementation technologies, sound gradual typing faces significant challenges. Conversely, it raises the question of how implementations could reduce the overheads associated with soundness and how tools could be used to steer programmers clear from pathological cases.

Over the past 20 years, programmers have embraced dynamically-typed programming languages. By now, they have also come to realize that programs in these languages lack reliable type information for software engineering purposes. Gradual typing addresses this problem; it empowers programmers to annotate an existing system with sound type information on a piecemeal basis. This paper presents an implementation of a gradual type system for a full-featured class-based language as well as a novel performance evaluation framework for gradual typing.

Many educators have tried to leverage computing or programming to help improve students' achievement in mathematics. However, several hopes of performance gains---particularly in algebra---have come up short. In part, these efforts fail to align the computing and mathematical concepts at the level of detail typically required to achieve transfer of learning. This paper describes Bootstrap, an early-programming curriculum that is designed to teach key algebra topics as students build their own videogames. We discuss the curriculum, explain how it aligns with algebra, and present initial data showing student performance gains on standard algebra problems after completing Bootstrap.

While many programmers appreciate the benefits of lazy programming at an abstract level, determining which parts of a concrete program to evaluate lazily poses a significant challenge for most of them. Over the past thirty years, experts have published numerous papers on the problem, but developing this level of expertise requires a significant amount of experience.

Many languages support behavioral software contracts so that programmers can describe a component's obligations and promises via logical assertions in its interface. The contract system monitors program execution, checks whether the assertions hold, and, if not, blames the guilty component. Pinning down the violator gets the debugging process started in the right direction. Quality contracts impose a serious run-time cost, however, and programmers therefore compromise in many ways. Some turn off contracts for deployment, but then contracts and code quickly get out of sync during maintenance. Others test contracts randomly or probabilistically. In all cases, programmers have to cope with lack of blame information when the program eventually fails.

First-class classes enable programmers to abstract over patterns in the class hierarchy and to experiment with new forms of object-oriented programming such as mixins and traits. This increase in expressive power calls for tools to control the complexity of the software architecture. A contract system is one possible tool that has seen much use in object-oriented programming languages, but existing contract systems cannot cope with first-class classes. On the one hand, the typical contract language deals only with plain values such as numbers, while classes are higher-order values. On the other hand, contract specifications are usually contained within class definitions, while classes as values call for a separate contract language. This article presents the design and implementation of a contract system for first-class classes as well as a two-pronged evaluation. The first one states and proves a “blame correctness” theorem for a model of our language. The theorem shows that when the contract system assigns blame to a component for a contract violation, the component is indeed responsible for providing the nonconforming value. The second part, consisting of benchmarks and case studies, demonstrates the need for the rich contract language and validates that our implementation approach is performant with respect to time.

Optimizing compilers map programs in high-level languages to high-performance target language code. To most programmers, such a compiler constitutes an impenetrable black box whose inner workings are beyond their understanding. Since programmers often must understand the workings of their compilers to achieve their desired performance goals, they typically resort to various forms of reverse engineering, such as examining compiled code or intermediate forms. Instead, optimizing compilers should engage programmers in a dialog. This paper introduces one such possible form of dialog: optimization coaching. An optimization coach watches while a program is compiled, analyzes the results, generates suggestions for enabling further compiler optimization in the source program, and presents a suitable synthesis of its results to the programmer. We present an evaluation based on case studies, which illustrate how an optimization coach can help programmers achieve optimizations resulting in substantial performance improvements.

Dynamic type-checking and object-oriented programming often go hand-in-hand; scripting languages such as Python, Ruby, and JavaScript all embrace object-oriented (OO) programming. When scripts written in such languages grow and evolve into large programs, the lack of a static type discipline reduces maintainability. A programmer may thus wish to migrate parts of such scripts to a sister language with a static type system. Unfortunately, existing type systems neither support the flexible OO composition mechanisms found in scripting languages nor accommodate sound interoperation with untyped code. In this paper, we present the design of a gradual typing system that supports sound interaction between statically- and dynamically-typed units of class-based code. The type system uses row polymorphism for classes and thus supports mixin-based OO composition. To protect migration of mixins from typed to untyped components, the system employs a novel form of contracts that partially seal classes. The design comes with a theorem that guarantees the soundness of the type system even in the presence of untyped components.

Formal models serve in many roles in the programming language community. In its primary role, a model communicates the idea of a language design; the architecture of a language tool; or the essence of a program analysis. No matter which role it plays, however, a faulty model doesn't serve its purpose.

With this issue of the Journal of Functional Programming , we transition to a new leadership. Xavier Leroy, who has faithfully served as co-Editor in Chief since 2007, is stepping down. After a short apprenticeship over the past year, Benjamin Pierce is taking his place.

In the world of Racket, software systems consist of inter-operating components in different programming languages. A component's implementation language may provide the full functionality of Racket, or it may support a small domain-specific notation. Naturally, Racketeers construct languages as Racket components and compose them to create new languages. This talk will present the ideas behind Racket: language-specific components, the composition of components, and, most importantly, the rich support for building languages.

Programming language design benefits from constructs for extending the syntax and semantics of a host language. While C's string-based macros empower programmers to introduce notational shorthands, the parser-level macros of Lisp encourage experimentation with domain-specific languages. The Scheme programming language improves on Lisp with macros that respect lexical scope.

Behavioral software contracts supplement interface information with logical assertions. A rigorous enforcement of contracts provides useful feedback to developers if it signals contract violations as soon as they occur and if it assigns blame to violators with preciseexplanations. Correct blame assignment gets programmers started with the debugging process and can significantly decrease the time needed to discover and fix bugs.

Behavioral software contracts have become a popular mechanism for specifying and ensuring logical claims about a program's flow of values. While contracts for first-order functions come with a natural interpretation and are well understood, the various incarnations of higher-order contracts adopt, implicitly or explicitly, different views concerning the meaning of contract satisfaction. In this article, we define various notions of contract satisfaction in terms of observational equivalence and compare them with each other and notions in the literature. Specifically, we introduce a small model language with higher-order contracts and use it to formalize different notions of contract satisfaction. Each of them demands that the contract parties satisfy certain observational equivalences.

First-class classes add expressive power to class-based object-oriented languages. Most importantly, programmers can abstract over common scenarios with first-class classes. When it comes to behavioral software contracts, however, first-class classes pose significant challenges. In this paper, we present the first contract system for a programming language with first-class classes. The design has been implemented for Racket, which supports first-class classes and which implements mixins and traits as syntactic sugar. We expect that our experience also applies to languages with native mixins and/or traits.

Existing macro systems force programmers to make a choice between clarity of specification and robustness. If they choose clarity, they must forgo validating significant parts of the specification and thus produce low-quality language extensions. If they choose robustness, they must write in a style that mingles the implementation with the specification and therefore obscures the latter.

In 1995, my team and I decided to create an outreach project that would use our research on functional programming to change the K-12 computer science curriculum. We had two different goals in mind. On the one hand, our curriculum should rely on mathematics to teach programming, and it d exploit programming to teach mathematics. All students - not just those who major in computer science - should benefit. On the other hand, our course should demonstrate that introductory programming can focus on program design, not just a specific syntax. We also wished to create a smooth path from a design-oriented introductory course all the way to courses on large software projects.

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.

Behavioral software contracts express properties concerning the flow of values across component (modules, classes, etc) interfaces. These properties are often beyond the reach of theorem provers and are therefore monitored at run-time. When the monitor discovers a contract violation, it raises an exception that simultaneously pinpoints the contract violator and explains the nature of the violation.

Functional programming languages ought to play a central role in mathematics education for middle schools (age range: 10-14). After all, functional programming is a form of algebra and programming is a creative activity about problem solving. Introducing it into mathematics courses would make pre-algebra course come alive. If input and output were invisible, students could implement fun simulations, animations, and even interactive and distributed games all while using nothing more than plain mathematics. We have implemented this vision with a simple framework for purely functional I/O. Using this framework, students design, implement, and test plain mathematical functions over numbers, booleans, string, and images. Then the framework wires them up to devices and performs all the translation from external information to internal data (and vice versa)--just like every other operating system. Once middle school students are hooked on this form of programming, our curriculum provides a smooth path for them from pre-algebra to freshman courses in college on object-oriented design and theorem proving.

Many recent research projects focus on language support for behavioral software contracts, that is, assertions that govern the boundaries between software building blocks such as procedures, classes, or modules. Contracts primarily help locate bugs in programs, but they also tend to affect the performance of the program, especially as they become complex.

ACL2, a Common Lisp-based language for programming and theorem proving, has enjoyed industrial success despite lacking modern language features such as a module system. In previous work, we equipped ACL2 with modules, interfaces, and explicit linking and measured our system with a series of experiments. One experiment revealed a serious lack of expressivity; the interfaces cannot describe the induction schemes necessary to reason about exported functions with nontrivial patterns of recursion.

Eighteen years ago Richard Bird joined the editorial team of the Journal of Functional Programming . As Richard mentions in his recollections (Bird, 2006), the founding editors of the Journal , Simon Peyton Jones and Philip Wadler, had asked him to contribute a regular column to be called Functional Pearls , roughly modeled on the Programming Pearls that Jon Bentley had run for the Communications of the ACM in the 1980s. Richard agreed to the suggestion, but only under the proviso that he would seek other contributors to the column.

When scripts in untyped languages grow into large programs, maintaining them becomes difficult. A lack of types in typical scripting languages means that programmers 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.

Over the past two decades, Scheme macros have evolved into a powerful API for the compiler front-end. Like Lisp macros, their predecessors, Scheme macros expand source programs into a small core language; unlike Lisp systems, Scheme macro expanders preserve many desirable properties, including lexical scope and source location. Using such macros, Scheme programmers now routinely develop the ultimate abstraction: embedded domain-specific programming languages.

Operators for delimiting control and for capturing composable continuations litter the landscape of theoretical programming language research. Numerous papers explain their advantages, how the operators explain each other (or don't), and other aspects of the operators' existence. Production programming languages, however, do not support these operators, partly because their relationship to existing and demonstrably useful constructs - such as exceptions and dynamic binding - remains relatively unexplored.

In PLT Scheme, programs consist of modules with contracts. The latter describe the inputs and outputs of functions and objects via predicates. A run-time system enforces these predicates; if a predicate fails, the enforcer raises an exception that blames a specific module with an explanation of the fault.In this paper, we show how to use such module contracts to turn set-based analysis into a fully modular parameterized analysis. Using this analysis, a static debugger can indicate for any given contract check whether the corresponding predicate is always satisfied, partially satisfied, or (potentially) completely violated. The static debugger can also predict the source of potential errors, i.e., it is sound with respect to the blame assignment of the contract system.

Implementing first-class continuations can pose a challenge if the target machine makes no provisions for accessing and re-installing the run-time stack. In this paper, we present a novel translation that overcomes this problem. In the first half of the paper, we introduce a theoretical model that shows how to eliminate the capture and the use of first-class continuations in the presence of a generalized stack inspection mechanism. The second half of the paper explains how to translate this model into practice in two different contexts. First, we reformulate the servlet interaction language in the PLT Web server, which heavily relies on first-class continuations. Using our technique, servlet programs can be run directly under the control of non-cooperative web servers such as Apache. Second, we show how to use our new technique to copy and reconstitute the stack on MSIL.Net using exception handlers. This establishes that Scheme's first-class continuations can exist on non-cooperative virtual machines.

In 1996, Gil and Lorenz proposed programming language constructs for specifying environmental acquisition in addition to inheritance acquisition for objects. They noticed that in many programs, objects are arranged in containment hierarchies and need to obtain information from their container objects. Therefore, if languages allowed programmers to specify such relationships directly, type systems and run-time environments could enforce the invariants that make these programming patterns work.In this paper, we present a formal version of environmental acquisition for class-based languages. Specifically, we introduce an extension of the ClassicJava model with constructs for environmental acquisition of fields and methods, a type system for the model, a reduction semantics, and a type soundness proof. We also discuss how to scale the model to a full-scale Java-like programming language.

Financial companies, engineering firms and even scientists create increasingly larger spreadsheets and spreadsheet programs. The creators of large spreadsheets make errors and must track them down. One common class of errors concerns unit errors, because spreadsheets often employ formulas with physical or monetary units. In this paper, we describe XeLda, our tool for unit checking Excel spreadsheets. The tool highlights cells if their formulas process values with incorrect units and if derived units clash with unit annotations. In addition, it draws arrows to the sources of the formulas for debugging. The tool is sensitive to many of the intricacies of Excel spreadsheets including tables, matrices, and even circular references. Using XeLda, we have detected errors in some published scientific spreadsheets.

Twenty years ago Abelson and Sussman's Structure and Interpretation of Computer Programs radically changed the intellectual landscape of introductory computing courses. Instead of teaching some currently fashionable programming language, it employed Scheme and functional programming to teach important ideas. Introductory courses based on the book showed up around the world and made Scheme and functional programming popular. Unfortunately, these courses quickly disappeared again due to shortcomings of the book and the whimsies of Scheme. Worse, the experiment left people with a bad impression of Scheme and functional programming in general. In this pearl, we propose an alternative role for functional programming in the first-year curriculum. Specifically, we present a framework for discussing the first-year curriculum and, based on it, the design rationale for our book and course, dubbed How to Design Programs . The approach emphasizes the systematic design of programs. Experience shows that it works extremely well as a preparation for a course on object-oriented programming.

Security folklore holds that a security mechanism based on stack inspection is incompatible with a global tail call optimization policy; that an implementation of such a language must allocate memory for a source-code tail call, and a program that uses only tail calls (and no other memory-allocating construct) may nevertheless exhaust the available memory. In this article, we prove this widely held belief wrong. We exhibit an abstract machine for a language with security stack inspection whose space consumption function is equivalent to that of the canonical tail call optimizing abstract machine. Our machine is surprisingly simple and suggests that tail calls are as easy to implement in a security setting as they are in a conventional one.

Education matters. The lack of education on functional programming languages and techniques is visible on a daily basis. Our students, co-workers, friends, and colleagues just don't know enough about these ideas and therefore often fail to implement the best possible solutions for their programming problems. The purpose of Educational Pearls is to address the education problem of our community from many different angles. It will include contributions on curricula issues, educational software support, and educational experiences. They will help teachers, professors, researchers, and software developers to promote functional programming languages and techniques in their respective contexts.

Assertions play an important role in the construction of robust software. Their use in programming languages dates back to the 1970s. Eiffel, an object-oriented programming language, wholeheartedly adopted assertions and developed the "Design by Contract" philosophy. Indeed, the entire object-oriented community recognizes the value of assertion-based contracts on methods.In contrast, languages with higher-order functions do not support assertion-based contracts. Because predicates on functions are, in general, undecidable, specifying such predicates appears to be meaningless. Instead, the functional languages community developed type systems that statically approximate interesting predicates.In this paper, we show how to support higher-order function contracts in a theoretically well-founded and practically viable manner. Specifically, we introduce λcon, a typed lambda calculus with assertions for higher-order functions. The calculus models the assertion monitoring system that we employ in DrScheme. We establish basic properties of the model (type soundness, etc.) and illustrate the usefulness of contract checking with examples from DrScheme's code base.We believe that the development of an assertion system for higher-order functions serves two purposes. On one hand, the system has strong practical potential because existing type systems simply cannot express many assertions that programmers would like to state. On the other hand, an inspection of a large base of invariants may provide inspiration for the direction of practical future type system research.

This invited talk presents an overview of the TeachScheme! and DrScheme projects. The former aims at bringing the principles of programming and programming languages into the introductory programming curriculum. The latter is a program development environment that supports the pedagogy and design principles of the TeachScheme! project. Carrying out these projects enriched our research life with many interesting programming language and system design problems.

DrScheme is a programming environment for Scheme. It fully integrates a graphics-enriched editor, a parser for multiple variants of Scheme, a functional read-eval-print loop, and an algebraic printer. The environment is especially useful for students, because it has a tower of syntactically restricted variants of Scheme that are designed to catch typical student mistakes and explain them in terms the students understand. The environment is also useful for professional programmers, due to its sophisticated programming tools, such as the static debugger, and its advanced language features, such as units and mixins. Beyond the ordinary programming environment tools, DrScheme provides an algebraic stepper, a context-sensitive syntax checker, and a static debugger. The stepper reduces Scheme programs to values, according to the reduction semantics of Scheme. It is useful for explaining the semantics of linguistic facilities and for studying the behavior of small programs. The syntax checker annotates programs with font and color changes based on the syntactic structure of the program. On demand, it draws arrows that point from bound to binding occurrences of identifiers. It also supports α-renaming. Finally, the static debugger provides a type inference system that explains specific inferences in terms of a value-flow graph, selectively overlaid on the program text.

The construction of interactive server-side Web applications differs substantially from the construction of traditional interactive programs. In contrast, existing Web programming paradigms force programmers to save and restore control state between user interactions. We present an automated transformation that converts traditional interactive programs into standard CGI programs. This enables reuse of existing software development methodologies. Furthermore, an adaptation of existing programming environments supports the development of Web programs.

Checking pre- and post-conditions of procedures and methods at runtime helps improve software reliability. In the procedural world, pre- and post-conditions have a straightforward interpretation. If a procedure's pre-condition doesn't hold, the caller failed to establish the proper context. If a post-condition doesn't hold, the caller failed to establish the proper context. If a post-condition doesn't hold, the procedure failed to compute the expected result.

Component-based software manufacturing has the potential to bring division-of-labor benefits to the world of software engineering. In order to make a market of software components viable, however, producers and consumers must agree on enforceable software contracts. In this paper, we show how to enforce contracts if components are manufactured from class and interface hierarchies. In particular, we focus on one style of contract: pre- and post-conditions. Programmers annotate class and interface methods with pre- and post-conditions and the run-time system checks these conditions during evaluation. These contracts guarantee that methods are called properly and provide appropriate results. In procedural languages, the use of pre- and post-condition contracts is well-established and studies have demonstrated its value. In object-oriented languages, however, assigning blame for pre- and post-condition failures poses subtle and complex problems. Specifically, assigning blame for malformed class and interface hierarchies is so difficult that none of the existing contract monitoring tools correctly assign blame for these failures. In this paper, we show how to overcome these problems in the context of Java. Our work is based on the notion of behavioral subtyping.

Most software metrics measure the syntactic qualities of a program. While measuring such properties may reveal problems in programs, these metrics fail to measure the essence of programs: (partial) correctness and robustness. We therefore propose to base metrics on semantic, instead of syntactic, criteria. To illustrate the idea of semantics-based metrics, we have built static debuggers, which are tools that detect potential run-time failures. More specifically, a static debugger analyses programs written in safe programming languages and pinpoints those program operations that might trigger a run-time error. This paper briefly recalls what safety means for a programming language. It then sketches how a static debugger works and the role it plays in measuring the robustness of a program. The last section discusses the use of static debuggers in the classroom, an NSF Educational Innovation Project.

The MrEd virtual machine serves both as the implementation platform for the DrScheme programming environment, and as the underlying Scheme engine for executing expressions and programs entered into DrScheme's read-eval-print loop. We describe the key elements of the MrEd virtual machine for building a programming environment, and we step through the implementation of a miniature version of DrScheme in MrEd. More generally, we show how MrEd defines a high-level operating system for graphical programs.

The future annotation of MultiLisp provides a simple method for taming the implicit parallelism of functional programs. Prior research on future has concentrated on implementation and design issues, and has largely ignored the development of a semantic characterization of future . This paper considers an idealized functional language with futures and presents a series of operational semantics with increasing degrees of intensionality. The first semantics defines future to be a semantically transparent annotation. The second semantics interprets a future expression as a potentially parallel task. The third semantics explicates the coordination of parallel tasks by introducing placeholder objects and touch operations. We use the last semantics to derive a program analysis algorithm and an optimization algorithm that removes provably redundant touch operations. Experiments with the Gambit compiler indicate that this optimization significantly reduces the overhead imposed by touch operations.

Set-based analysis (SBA) produces good predictions about the behavior of functional and object-oriented programs. The analysis proceeds by inferring constraints that characterize the data flow relationships of the analyzed program. Experiences with MrSpidey, a static debugger based on SBA, indicate that SBA can adequately deal with programs of up to a couple of thousand lines of code. SBA fails, however, to cope with larger programs because it generates systems of constraints that are at least linear, and possibility quadratic, in the size of the analyzed program. This article presents theoretical and practical results concerning methods for reducing the size of constraint systems. The theoretical results include of proof-theoretic characterization of the observable behavior of constraint systems for program components, and a complete algorithm for deciding the observable equivalence of constraint systems. In the course of this development we establish a close connection between the observable equivalence of constraint systems and the equivalence of regular-tree grammars. We then exploit this connection to adapt a variety of algoirthms for simplifying grammars to the problem of simplifying constraint systems. Based on the resulting algorithms, we have developed componential set-based analysis , a modular and polymorphic variant of SBA. Experimental results verify the effectiveness of the simplification algorithms and the componential analysis. The simplified constraint systems are typically an order of magnitude smaller than the original systems. These reductions in size produce significant gains in the speed of the analysis.

A module system ought to enable assembly-line programming using separate compilation and an expressive linking language. Separate compilation allows programmers to develop parts of a program independently. A linking language gives programmers precise control over the assembly of parts into a whole. This paper presents models of program units, MzScheme's module language for assembly-line programming. Units support separate compilation, independent module reuse, cyclic dependencies, hierarchical structuring, and dynamic linking. The models explain how to integrate units with untyped and typed languages such as Scheme and ML.

While class-based object-oriented programming languages provide a flexible mechanism for re-using and managing related pieces of code, they typically lack linguistic facilities for specifying a uniform extension of many classes with one set of fields and methods. As a result, programmers are unable to express certain abstractions over classes.In this paper we develop a model of class-to-class functions that we refer to as mixins. A mixin function maps a class to an extended class by adding or overriding fields and methods. Programming with mixins is similar to programming with single inheritance classes, but mixins more directly encourage programming to interfaces.The paper develops these ideas within the context of Java. The results are 1. an intuitive model of an essential Java subset; 2. an extension that explains and models mixins; and 3. type soundness theorems for these languages.

As software projects continue to grow in scale and scope, it becomes important to reuse software. An important kind of reuse is extensibility, i.e., the extension of software without accessing existing code to edit or copy it. In this paper, we propose a rigorous, semantics-based definition of software extensibility. Then we illustrate the utility of our definitions by applying them to several programs. The examination shows how programming style affects extensibility and also drives the creation of a variant of an existing design pattern. We consider programs in both object-oriented and functional languages to prove the robustness of our definitions. 1 Introduction As software projects have continued to grow in scale and scope, it has become increasingly important to reuse program components. Reuse lowers software development costs by reducing development time, decreasing the number of errors, and increasing the consistency of software systems. In short, there are compelling reasons...

Set based analysis is a constraint-based whole program analysis that is applicable to functional and object-oriented programming language. Unfortunately, the analysis is useless for large programs, since it generates descriptions of data flow relationships that grow quadratically in the size of the program.This paper presents componential set-based analysis, which is faster and handles larger programs without any loss of accuracy over set-based analysis. The design of the analysis exploits a number of theoretical results concerning constraint systems, including a completeness result and a decision algorithm concerning the observable equivalance of constraint systems. Experimental results validate the practically of the analysis.

Plotkin (1975) showed that the lambda calculus is a good model of the evaluation process for call-by-name functional programs. Reducing programs to constants or lambda abstractions according to the leftmost-outermost strategy exactly mirrors execution on an abstract machine like Landin's SECD machine. The machine-based evaluator returns a constant or the token closure if and only if the standard reduction sequence starting at the same program will end in the same constant or in some lambda abstraction. However, the calculus does not capture the sharing of the evaluation of arguments that lazy implementations use to speed up the execution. More precisely, a lazy implementation evaluates procedure arguments only when needed and then only once. All other references to the formal procedure parameter re-use the value of the first argument evaluation. The mismatch between the operational semantics of the lambda calculus and the actual behavior of the prototypical implementation is a major obstacle for compiler writers. Unlike implementors of the leftmost-outermost strategy or of a call-by-value language, implementors of lazy systems cannot easily explain the behavior of their evaluator in terms of source level syntax. Hence, they often cannot explain why a certain syntactic transformation ‘works’ and why another doesn't. In this paper we develop an equational characterization of the most popular lazy implementation technique – traditionally called ‘call-by-need’ – and prove it correct with respect to the original lambda calculus. The theory is a strictly smaller theory than Plotkin's call-by-name lambda calculus. Immediate applications of the theory concern the correctness proofs of a number of implementation strategies, e.g. the call-by-need continuation passing transformation and the realization of sharing via assignments. Some of this material first appeared in a paper presented at the 1995 ACM Conference on the Principles of Programming Languages. The paper was a joint effort with Maraist, Odersky and Wadler, who had independently developed a different equational characterization of call-by-need. We contrast our work with that of Maraist et al. in the body of this paper where appropriate.

MrSpidey is a user-friendly, interactive static debugger for Scheme. A static debugger supplements the standard debugger by analyzing the program and pinpointing those program operations that may cause run-time errors such as dereferencing the null pointer or applying non-functions. The program analysis of MrSpidey computes value set descriptions for each term in the program and constructs a value flow graph connecting the set descriptions. Using the set descriptions, MrSpidey can identify and highlight potentially erroneous program operations, whose cause the programmer can then explore by selectively exposing portions of the value flow graph.

The mismatch between the operational semantics of the lambda calculus and the actual behavior of implementations is a major obstacle for compiler writers. They cannot explain the behavior of their evaluator in terms of source level syntax, and they cannot easily compare distinct implementations of different lazy strategies. In this paper we derive an equational characterization of call-by-need and prove it correct with respect to the original lambda calculus. The theory is a strictly smaller theory than the lambda calculus. Immediate applications of the theory concern the correctness proofs of a number of implementation strategies, e.g., the call-by-need continuation passing transformation and the realization of sharing via assignments.

The future annotations of MultiLisp provide a simple method for taming the implicit parallelism of functional programs. Past research concerning futures has focused on implementation issues. In this paper, we present a series of operational semantics for an idealized functional language with futures with varying degrees of intensionality. We develop a set-based analysis algorithm from the most intensional semantics, and use that algorithm to perform touch optimization on programs. Experiments with the Gambit compiler indicates that this optimization substantially reduces program execution times. 1 Implicit Parallelism via Annotations Programs in functional languages offer numerous opportunities for executing program components in parallel. In a call-by-value language, for example, the evaluation of every function application could spawn a parallel thread for each sub-expression. However, if such a strategy were applied indiscriminately, the execution of a program would generate far t...

The widespread use of the continuation-passing style (CPS) transformation in compilers, optimizers, abstract interpreters, and partial evaluators reflects a common belief that the transformation has a positive effect on the analysis of programs. Investigations by Nielson [13] and Burn/Filho [5,6] support, to some degree, this belief with theoretical results. However, they do not pinpoint the source of increased abstract information and do not explain the observation of many people that continuation-passing confuses some conventional data flow analyses.

In order to simplify the compilation process, many compilers for higher-order languages use the continuation-passing style (CPS) transformation in a first phase to generate an intermediate representation of the source program. The salient aspect of this intermediate form is that all procedures take an argument that represents the rest of the computation (the “continuation”). Since the nai¨ve CPS transformation considerably increases the size of programs, CPS compilers perform reductions to produce a more compact intermediate representation. Although often implemented as a part of the CPS transformation, this step is conceptually a second phase. Finally, code generators for typical CPS compilers treat continuations specially in order to optimize the interpretation of continuation parameters.

According to folklore, Algol is an “orthogonal” extension of a simple imperative programming language with a call-by-name functional language. The former contains assignments, branching constructs, and compound statements; the latter is based on the typed λ-calculus. In an attempt to formalize the claim of “orthogonality”, we define a simple version of Algol and an extended λ-calculus. The calculus includes the full β-rule and rules for the reduction of assignment statements and commands. It has the usual properties, e.g., it satisfies a Church-Rosser and Strong Normalization Theorem. In support of the claim that the imperative and functional components are orthogonal to each other, we show that the proofs of these theorems are combinations of separate Church-Rosser and Strong Normalization theorems for each sublanguage.

ion Robert Cartwright Matthias Felleisen Department of Computer Science Rice University Houston, TX 77251-1892 Rice Technical Report CS 91-167 A preliminary version of this technical report appeared in the Proceedings of the 19th Annual ACM Symposium on Principles of Programming Languages, January 19--22, 1992, Albuquerque, New Mexico. Copyright c fl1992 by Robert Cartwright and Matthias Felleisen 1 Full Abstraction and Sequentiality 1 1.1 Summary of Previous Work : : : : : : : : : : : : : : : : : : : : : : : : : : : 2 1.2 Summary of Results : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 3 2 PCF 4 2.1 Formal Semantics : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 5 2.2 Observational Equivalence, Sequentiality : : : : : : : : : : : : : : : : : : : : 8 3 Observing Sequentiality 9 3.1 Using errors, programmers can observe the order of evaluation. : : : : : : : 10 3.2 Using control operators, programs can observe the order of evaluation. : : : 10...

The choice of a parameter-passing technique is an important decision in the design of a high-level programming language. To clarify some of the semantic aspects of the decision, we develop, analyze, and compare modifications of the $\\lambda$-calculus for the most common parameter-passing techniques. More specifically, for each parameter-passing technique we provide (1) a program rewriting semantics for a language with side-effects and first-class procedures based on the respective parameter-passing technique; (2) an equational theory derived from the rewriting semantics; (3) a formal analysis of the correspondence between the calculus and the semantics; and (4) a strong normalization theorem for the largest possible imperative fragment of the theory.\nA comparison of the various systems reveals that Algol's call-by-name indeed satisfies the well-known $\\beta$ rule of the original $\\lambda$-calculus, but at the cost of complicated axioms for the imperative part of the theory. The simplest and most appealing axiom system appears to be the one for a call-by-value language with reference cells as first-class values.

Article Free Access Share on Models of continuations without continuations Authors: Dorai Sitaram Department of Computer Science, Rice University, Houston, TX Department of Computer Science, Rice University, Houston, TXView Profile , Matthias Felleisen Department of Computer Science, Rice University, Houston, TX Department of Computer Science, Rice University, Houston, TXView Profile Authors Info & Claims POPL '91: Proceedings of the 18th ACM SIGPLAN-SIGACT symposium on Principles of programming languagesJanuary 1991 Pages 185–196https://doi.org/10.1145/99583.99611Online:03 January 1991Publication History 4citation439DownloadsMetricsTotal Citations4Total Downloads439Last 12 Months7Last 6 weeks2 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteeReaderPDF

Optimizing and parallelizing compilers for procedural languages rely on various forms of program dependence graphs (pdgs) to express the essential control and data dependencies among atomic program operations. In this paper, we provide a semantic justification for this practice by deriving two different forms of program dependence graph — the output pdg and the def-order pdg—and their semantic definitions from non-strict generalizations of the denotational semantics of the programming language. In the process, we demonstrate that both the output pdg and the def-order pdg (with minor technical modifications) are conventional data-flow programs. In addition, we show that the semantics of the def-order pdg dominates the semantics of the output pdg and that both of these semantics dominate—rather than preserve—the semantics of sequential execution.

An analysis of the λugr;-C-calculus and its problematic relationship to operational equivalence leads to a new control facility: the prompt-application. With the introduction of prompt-applications, the control calculus becomes a traditional calculus all of whose equations imply operational equivalence. In addition, prompt-applications enhance the expressiveness and efficiency of the language. We illustrate the latter claim with examples from such distinct areas as systems programming and tree processing.

Imperative assignments are abstractions of recurring programming patterns in purely functional programming languages. When added to higher-order functional languages, they provide a higher-level of modularity and security but invalidate the simple substitution semantics. We show that, given an operational interpretation of a denotational semantics for such a language, it is possible to design a two-level extension of the lu-calculus. This calculus provides a location-free rewriting semantics of the language and offers new possibilities for reasoning with assignments. The upper level of the calculus factors out all the steps in a reduction sequence which must be in a linear order; the lower level allows a partial ordering of reduction steps.