The use of visualization tools to instruct Computer Science students on dynamic processes has a long and successful history. Unlike most articles on visualization tools, that often only focus on classroom experiences, this articles focuses on implementation features that are important to make the user's and the developer's experience pleasant and smooth. To create such an experience for the user, dynamic visualizations need a fast start-up time and a fast response time to user interactions. Factors that impact the user experience include start-up time, demand for volatile memory, and interference from a garbage collector. Presented empirical results suggest using restricted parallelism to generate images, using thunks to represent images at runtime, and not requesting more frequent incremental collections. To create such an experience for the developer, the amount of repeated code needs to be minimal. To this end, the article describes a macro-based abstraction to generate event handlers.
Binding Trees extend Abstract Syntax Trees with binding structure. We take up on this idea and propose Context-Free Binding Grammars: a novel extension to Context-Free Grammars that allows us to express binding structure in a declarative fashion. In this way, we are able to define not only the syntax of a language but also how its variables are bound within their scope. By means of two representative examples from functional programming, we illustrate this capability. Our work is complemented by a proof of completeness and a restricted form of soundness, which ultimately renders our grammar formalism as a context-sensitive approach. In summary, our formalism facilitates the description of languages that incorporate the idea of name binding and thus contributes to the development of (Embedded) Domain-Specific Languages.
Type-preserving compilation is an approach to building reliable compilers. The technique has recently been extended to dependently typed languages, but existing approaches have practical and theoretical shortcomings. We present a dependent-type-preserving translation into continuation-passing style (CPS). As improvements from previous work, our translation yields no administrative redexes, and its output can be typed using standard typing rules. This is achieved by defining an auxiliary translation that produces let-represented continuations in selected cases. The unique design makes the output of the translation partly look like A-normal form (ANF).
The classification of bugs in functional languages is an understudied area when compared to their imperative counterparts, such as Java and C. This paper acts as an initial step to cover this gap into two complementary directions. First, a dataset of 142 bugs from 10 Haskell FOSS (Free and Open Source Software) repositories have been classified according to two taxonomies from the literature in order to assess how well they handle the differences in programming paradigms. Our results indicate that programming errors, i.e. defects in logic, algorithms and composition are the most common faults reported in open source repositories and are found nearly twice as much than in studies of imperative languages. Second, we performed interviews with 12 Haskell developers about their experience with bugs and the usefulness of taxonomies in practice. The interviewees expressed skepticism that taxonomies will help them in fixing bugs, but may provide support for reviews and knowledge sharing. Many of the interviewees specify that large parts of both taxonomies are irrelevant due to project domains, which aligns with the findings of our manual labeling. Participants asked for additional categories to cover programming errors specific to Haskell, GUI to be UI & UX and for explicit missed-requirement categories for any taxonomy they'd employ. Next to the taxonomies, we summarize some insight on the developers issues with memory leaks and the type system.
The algebraic path problem highlights an abstract setting for solving various graph-related problems, with the all-pairs shortest path problem being one of the most notable examples. A central operation for one solution of algebraic path problem is iterated multiplication until convergence, where the number of iterations is bounded by the number of vertices in the graph. This paper proves convergence for the general algebraic path problem using an arbitrary idempotent semiring over square matrices. The proof is machine-checked and done constructively in Agda, making use of the pigeonhole principle. Furthermore, we extend the proof to the Kleene algebra, demonstrating the equality between finite iterations of matrix multiplication and the Kleene closure under certain preconditions.
