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.
In their first Formal Languages and Automata Theory course, students find nondeterminism challenging. Most students struggle to understand the operational semantics of nondeterministic machines. Often, this includes understanding why a nondeterministic machine accepts or rejects a word, why there can be multiple computations on the same input, and, unlike a deterministic machine, why all the input is not consumed. This article presents a visualization tool, and its implementation, developed to help students understand nondeterministic behavior. The tool is integrated into FSM-a functional domain-specific language for the Automata Theory classroom. The strategy is based on the automatic generation of computation graphs. Unlike previous visualization tools, the computation graphs generated reflect the structure of the given machine's transition diagram and not the structure of the computation tree. Data obtained, as part of a formative study, from students using the described computation graphs suggests that they are well-received and useful.
In non-strict languages such as Haskell the execution of individual expressions in a program significantly deviates from the order in which they appear in the source code. This can make it difficult to find bugs related to this deviation, since the evaluation of expressions does not occur in the same order as in the source code. At the moment, Haskell errors focus on values being produced, whereas it is often the case that faults are due to values being consumed. For non-strict languages, values involved in a bug are often generated immediately prior to the evaluation of the buggy code. This creates an opportunity for evaluation traces, tracking recently evaluated locations (which can deviate from call-order) to help establish the origin of values involved in faults. In this paper, we describe an extension of GHC’s Haskell Program Coverage with evaluation traces, recording recent evaluations in the coverage file, and reporting an evaluation trace alongside the call stack on exception. This lets us reconstruct the chain of events and locate the origin of faults. As a case study, we applied our initial implementation to the nofib-buggy data set and found that some runtime errors greatly benefit from trace information.
Modulo operations on array indices provide a convenient means for specifying cyclic operations on arrays, such as rotations. A naive compilation of such operations involves integer divisions, which often can be avoided by partitioning or rearranging iteration spaces. This paper proposes an optimisation to this effect. The key idea is to systematically replace modulo operations within loops by partitioning such loops and replacing the modulo operations with division-free equivalents. We present two different code transformation schemes for the proposed optimisation, provide correctness arguments for both, and present initial performance observations of the effects of these transformations in the context of a compiler for the array language SaC. We look at several benchmarks ranging from micro-benchmarks to some more realistic applications and run them on hardware ranging from multi-core CPUs to GPUs. Depending on the problem size, machine characteristics, and application context, we see direct performance benefits of up to a factor of 25 and even higher indirect benefits due to other optimisations that the proposed transformations enable.
We present a small-step, frame stack style, semantics for sequential Core Erlang, a dynamically typed, impure functional programming language. The semantics and the properties that we prove are machine-checked with the Coq proof assistant. We improve on previous work by including exceptions and exception handling, as well as built-in data types and functions. Based on the semantics, we define multiple concepts of program equivalence (contextual, CIU equivalence, and equivalence based on logical relations) and prove that the definitions are all equivalent. Using this we are able to give a correctness criterion for refactorings by means of contextually equivalent symbolic expression pairs, which is one of the main motivations of this work.
Proof assistants and dependently typed languages such as Coq, Agda, Lean, and Idris can be used to ascertain the correctness of software with mathematical precision. While much research has been done on their theoretical foundations, their actual implementations have been studied to a much lesser extent. As a result, features that are not considered part of the theoretical foundations - such as implicit arguments and type classes - have their own bespoke implementation for each language, making for code bases that are hard to understand and maintain. To address some of the common problems in the implementations of dependently typed languages, we present a modular architecture for implementing the transformation from user-friendly surface syntax into a small and well-behaved core language, also known as elaboration. Our architecture is made modular through the use of an open datatype of constraints and a plugin system for solvers that work on these constraints, which means that each new feature is contained in its own module. We showcase our design with a proof-of-concept elaborator for a language with dependent types, implicit arguments, higher-order unification, and instance arguments.
Coordination is a well established computing paradigm with a plethora of languages, abstractions and approaches. The functional coordination language TeamPlay follows the approach of exogenous coordination and organises an application as a streaming data-flow graph of independently operating, state-free components. In this work we capitalise on this stringent application architecture for fault-tolerance against both permanent and transient hardware failure. We extend the TeamPlay language by a range of fault-tolerance features to be selected by the system integrator. We further propose a multi-core runtime system that is able to isolate hardware faults and manages to keep an application running flawlessly in the presence of hardware failure by adaptively morphing the application.
TopHat is a mathematically formalized language for Task-Oriented Programming (top). It allows developers to specify workflows and business processes in a formal language, reason about their equality and use symbolic execution to verify their correctness and generate next-step hints. TopHat can run workflow specifications supporting collaborators during their execution. However, it can only do so for a statically specified amount of work. That is, the number of tasks running in parallel is always predefined by the developer. In contrast, other top engines like iTasks and mTasks act like an operating system, starting and stopping tasks at will. To capture this dynamic nature of workflow systems, we introduce Dynamic TopHat: a moderate extension to the TopHat calculus which allows end-users to initialize and kill tasks at runtime. Although this is a restricted version of the dynamic task lists found in iTasks, where the system itself can initialize new tasks, we show that common use cases of this feature are still expressible in Dynamic TopHat. Also, our proposed solution does not compromise the formal reasoning properties of TopHat. TopHat’s metatheory is formalized in the dependently typed programming language Idris and its symbolic execution engine is implemented in Haskell.
In strict functional languages, a left-to-right evaluation of an application of a curried function to n arguments generally requires creating n - 1 intermediate closures and making n function calls. A type-based optimization can reduce the number of calls by consistently uncurrying function definitions and calls to them, and by inserting implicit currying coercions when functions receive too few arguments. However, it only uncurries calls to known (let-bound) functions. Naively uncurrying calls to unknown (lambda-bound) functions generally fails, since the implicit uncurrying coercions do not preserve the semantics of programs with side effects. We propose a characterization of when calls to unknown (lambda-bound) functions can be uncurried. We describe it as a type-based translation and outline an algorithm that implements the translation. We demonstrate that programs with side effect preserve their meaning across this translation, even when they require uncurrying coercions.
In this paper we present type patterns: a notation for shape-carrying array types that enables the specification of dependent type signatures while maintaining flexibility and a high level of code readability. Similar notations pre-exist, but we extend them to support rank-polymorphism and specifications of arbitrarily complex constraints between values and types. Furthermore, we enable type patterns to double as a pattern matching mechanism against shapes and shape-components of array arguments, making those values directly available in the corresponding function bodies. While this notation could be used as a basis for a dependently typed language, in our prototypical implementation in the context of SaC we do not require all dependencies to be resolved statically. Instead, we follow a hybrid approach: we map the proposed type patterns into the pre-existing type system of SaC, and we generate additional constraints which we try to statically resolve as far as possible by means of partial evaluation. Any remaining constraints are checked at run-time. We outline our implementation in the context of the SaC ecosystem, and present several examples demonstrating the effectiveness of this hybrid approach based on partial evaluation.
This paper introduces a new parallel run-time for QuickCheck, a Haskell library and EDSL for specifying and randomly testing properties of programs. The new run-time can run multiple tests for a single property in parallel, using the available cores. Moreover, if a counterexample is found, the run-time can also shrink the test case in parallel, implementing a parallel search for a locally minimal counterexample. Our experimental results show a 3–9 × speed-up for testing QuickCheck properties on a variety of heavy-weight benchmark problems. We also evaluate two different shrinking strategies; deterministic shrinking, which guarantees to produce the same minimal test case as standard sequential shrinking, and greedy shrinking, which does not have this guarantee but still produces a locally minimal test case, and is faster in practice.
We present and evaluate the Futhark implementation of reverse-mode automatic differentiation (AD) for the basic blocks of parallel programming: reduce, prefix sum (scan), and reduce-by-index (multi-reduce). We present derivations of general-case algorithms, and then discuss several specializations that result in efficient differentiation of most cases of practical interest. We report an experiment that evaluates the GPU performance of the differentiated code and highlights the impact of the proposed specializations as well as the strengths and weaknesses of differentiating at high level bulk-parallel operators vs “differentiating the memory”, i.e., low-level implementations that access/update individual array elements.
Differential privacy (DP) provides a robust framework for ensuring individual privacy while analyzing population data. To achieve DP, statistical noise is added to query results before publication, but accurately determining the required noise is challenging, especially for user-defined functions. Existing approaches often rely on limited pre-defined functions with known sensitivities, limiting the expressivity of DP systems. In this paper, we present a novel embedded domain-specific language (eDSL) in Haskell to automatically approximate the sensitivity of user-defined linear functions commonly used in synthetic data generation. Our approach leverages Haskell’s expressive type system and generic programming principles to infer function ranges, enabling us to approximate sensitivities efficiently. We demonstrate the effectiveness of our eDSL by integrating it into the Multiplicative Weights Exponential Mechanism (MWEM) for synthetic data generation. Our solution guides users when updating functions, ensuring proper sensitivity consideration, enhancing the robustness and reliability of synthetic data algorithms. By adopting this straightforward yet effective approach, we streamline the sensitivity calculation process for user-defined functions, making it more accessible and user-friendly. The contributions of our work include an eDSL capable of approximating sensitivity for linear functions and its evaluation within the context of MWEM workloads.
FPGAs have enjoyed exponential growth of on-chip hardware resources — reason to reinvestigate hardware implementations of functional languages. This paper presents Heron, an FPGA-based special purpose processor core for pure, non-strict functional languages. We co-design its language semantics and parametrised design, gaining a high reductions-per-cycle performance metric. The Heron core is energy efficient, performing up to six times as many reductions per cycle as GHC. Despite its infancy, a 193 MHz Heron core outperforms wall-clock time for a mid-range Intel i3 1.9 GHz mobile CPU for 5 of these benchmarks and is competitive with an Alder Lake Intel i7 CPU. Its performance-per-Watt shows that the Heron core is a compelling solution for embedded applications. The simplicity of Heron’s design results in just 2% FPGA resource usage, paving the way for future single-chip parallelism, further improving absolute performance.
Despite their ubiquitous use in the daily lives of programmers, build systems have only recently started being the subject of formal investigation. They span across a wide spectrum satisfying many properties: backwards, forward, error-recovering, parallelizable, etc. In this paper, we present a new extensible embedded domain-specific language for writing forward build tasks. We focus our attention to a small set of abstractions that simplify the treatment of incrementality, caching and parallelism. We purposefully move the focus away from file dependencies and side effects to give attention to compositionality of tasks, structural caching of host programs and tracking of value change. We showcase an hybrid approach between incremental computing and build systems, in which logical constructs in the host language can too be cached and made incremental.
Bags are ubiquitous in program verification. They are the means of choice when we want to express that a collection of elements is a rearrangement of another collection. We are working towards an "application proving interface" (API) for finite bags that is perspicuous, rich, and easy to use. We propose an implementation of the Bag API in the dependently typed language Agda that has minimal meta-theoretic requirements and that we believe is suitable for both instructional and practical applications. Bags form a free commutative monoid. The implementation boils down to the free structure: bag expressions built from the empty bag (sic), singleton bags (sic) x (sic), and the union of bags A (sic) B, quotiented by the laws of commutative monoids.
