We inter-derive two prototypical styles of graph reduction: reduction machines à la Turner and graph rewriting systems à la Barendregt et al. To this end, we adapt Danvy et al.'s mechanical program derivations from the world of terms to the world of cyclic graphs. We also outline how to inter-derive a third style of graph reduction: a graph evaluator.
We present a so-called labelling method to insert cost annotations in a higher-order functional program, to certify their correctness with respect to a standard compilation chain to assembly code, and to reason on them in a higher-order Hoare logic.
We present a graph-based approach to the definition and creation of process topologies in the parallel Haskell extension Eden. Grace (Graph-based communication in Eden) allows the programmer to specify a network of processes as a graph, where the graph nodes represent processes and the edges represent communication channels. This simplifies the specification and creation of complex communication topologies. The main benefit of the Grace approach is the clean separation between coordination and computation. A special problem is the maintenance of type-safety. Runtime experiments show that Grace has a marginal overhead in comparison with traditional Eden code.
The Symposium on Trends in Functional Programming has a 25-year history as an annual forum for discussing emerging aspects of methods, tools, and theoretical frameworks supporting the development of declarative software.This volume contains major revisions of papers selected from the post-symposium proceedings of the 2009 symposium in Komárno, Slovakia and the 2010 symposium in Norman, Oklahoma.Out of 50 papers presented at these symposia, the program chairs selected 10 papers, and invited their authors to submit extended versions.The resulting articles went through the normal journal reviewing process, with each article being reviewed by three reviewers.Based on the reviews six were selected for inclusion in the special issue.Parallel computing is becoming increasingly important, due to the prevalence of multicores, and it has long been recognized that pure functional languages, due to their lack of side effects, are potentially very useful for parallel computing.The paper Comparing Low-Pain and No-Pain Multicore Haskells by Mustafa Aswad, Phil Trinder, Abdallah Al Zain, Greg Michaelson and Jost Berthold assesses the state of the art in parallel Haskell.This paper evaluates various parallel Haskell implementations, characterized as low-pain (some parallel annotations required) and no-pain (no parallel annotations required), in terms of performance and ease of programming.This systematic study forms a reference point for the state of the art as well as creating a foundation for future evaluations.The paper Graph-based Communication in Eden by Thomas Horstmeyer and Rita Loogen also addresses ease of programming parallel systems, this time in the context of distributed
We present a graph grammar based type inference system for a totally graphic development language. NiMo (Nets in Motion) can be seen as a graphic equivalent to Haskell that acts as an on-line tracer and debugger. Programs are process networks that evolve giving total visibility of the execution state, and can be interactively completed, changed or stored at any step. In such a context, type inference must be incremental. During the net construction or modification only type safe connections are allowed. The user visualizes the type information evolution and, in case of conflict, can easily identify the causes. Though based on the same ideas, the type inference system has significant differences with its analogues in functional languages. Process types are a non-trivial generalization of functional types to handle multiple outputs, partial application in any order, and curried-uncurried coercion. Here we present the elements to model graphical inference, the notion of structural and non-structural equivalence of type graphs, and a graph unification and composition calculus for typing nets in an incremental way.
Scala-Virtualized extends the Scala language to better support hosting embedded DSLs. Scala is an expressive language that provides a flexible syntax, type-level computation using implicits, and other features that facilitate the development of embedded DSLs. However, many of these features work well only for shallow embeddings, i.e. DSLs which are implemented as plain libraries. Shallow embeddings automatically profit from features of the host language through linguistic reuse: any DSL expression is just as a regular Scala expression. But in many cases, directly executing DSL programs within the host language is not enough and deep embeddings are needed, which reify DSL programs into a data structure representation that can be analyzed, optimized, or further translated. For deep embeddings, linguistic reuse is no longer automatic. Scala-Virtualized defines many of the language’s built-in constructs as method calls, which enables DSLs to redefine the built-in semantics using familiar language mechanisms like overloading and overriding. This in turn enables an easier progression from shallow to deep embeddings, as core language constructs such as conditionals or pattern matching can be redefined to build a reified representation of the operation itself. While this facility brings shallow, syntactic, reuse to deep embeddings, we also present examples of what we call deep linguistic reuse: combining shallow and deep components in a single DSL in such a way that certain features are fully implemented in the shallow embedding part and do not need to be reified at the deep embedding level.
We propose an application of programming language techniques to lossless data compression, where tree data are compressed as functional programs that generate them. This “functional programs as compressed data” approach has several advantages. First, it follows from the standard argument of Kolmogorov complexity that the size of compressed data can be optimal up to an additive constant. Secondly, a compression algorithm is clean: it is just a sequence of β -expansions (i.e., the inverse of β -reductions) for λ -terms. Thirdly, one can use program verification and transformation techniques (higher-order model checking, in particular) to apply certain operations on data without decompression. In this article, we present algorithms for data compression and manipulation based on the approach, and prove their correctness. We also report preliminary experiments on prototype data compression/transformation systems.
We present a PLT Redex model of a substantial portion of the Racket virtual machine and bytecode verifier (formerly known as MzScheme), along with lessons learned in developing the model. Inspired by the “warts-and-all” approach of the VLISP project, in which Wand et al. produced a verified implementation of Scheme, our model reflects many of the realities of a production system. Our methodology departs from the VLISP project’s in its approach to validation; instead of producing a proof of correctness, we explore the use of QuickCheck-style randomized testing, finding it a cheap and effective technique for discovering a variety of errors in the model—from simple typos to more fundamental design mistakes.
This paper presents an approach to completing variable names when writing programs in an implicitly typed functional language. As a first step toward developing practical systems, we considered a simple case: up to the cursor position the program text is given completely. With this assumption we specify a variable completion problem for an implicitly typed core functional language with let-polymorphism, and show an algorithm for solving the problem. Based on the algorithm we have implemented a variable name completion system for the language as an Emacs-mode.
Contract monitoring for strict higher-order functional languages has an intuitive meaning, an established theoretical basis, and a standard implementation. For lazy functional languages, the situation is less clear-cut. There is no agreed-upon intended meaning or theory, and there are competing implementations with subtle semantic differences.
The problem of inverse computation has many potential applications such as serialization/deserialization, providing support for undo, and test-case generation for software testing. In this paper, we propose an inverse computation method that always terminates for a class of functions known as parameter-linear macro tree transducers, which involve multiple data traversals and the use of accumulations. The key to our method is the observation that a function in the class can be regarded as a non-accumulative context-generating transformation without multiple data traversals. Accordingly, we demonstrate that it is easy to achieve terminating inverse computation for the class by context-wise memoization of the inverse computation results. We also show that when we use a tree automaton to express the inverse computation results, the inverse computation runs in time polynomial to the size of the original output and the textual program size.
Characterising a problem in terms of a system of equations is common to many branches of science and engineering. Due to their size, such systems are often described in a modular fashion by composition of individual equation system fragments. Checking the balance between the number of variables (unknowns) and equations is a common approach to early detection of mistakes that might render such a system unsolvable. However, current approaches to modular balance checking have a number of limitations. This paper investigates a more flexible approach that makes it possible to treat equation system fragments as true first-class entities. Furthermore, the approach handles so-called structurally dynamic systems, systems whose behaviour changes discretely and abruptly over time. The central idea is to record balance information in the type of an equation fragment. This information can then be used to determine if individual fragments are well formed, and if composing fragments preserves this property. The type system presented in this paper is developed in the context of Functional Hybrid Modelling (FHM). However, the key ideas are in no way specific to FHM, but should be applicable to any language featuring a notion of modular systems of equations, including systems with first-class components and structural dynamism.
Many side-effecting programming activities, such as profiling and tracing, can be formulated as crosscutting concerns and be framed as side-effecting aspects in the aspect-oriented programming paradigm. The benefit gained from this separation of concerns is particularly evident in purely functional programming, as adding such aspects using techniques such as monadification will generally lead to crosscutting changes. This paper presents an approach to provide side-effecting aspects for lazy purely functional languages in a user transparent fashion. We propose a simple yet direct state manipulation construct for developing side-effecting aspects and devise a systematic monadification scheme to translate the woven code to monadic style purely functional code. Furthermore, we present a static and dynamic semantics of the aspect programs and reason about the correctness of our monadification scheme with respect to them.
The Verilog hardware description language has padding semantics that allow designers to write descriptions where wires of different bit widths can be interconnected. However, many such connections are nothing more than bugs inadvertently introduced by the designer and often result in circuits that behave incorrectly or use more resources than required. A similar problem occurs when wires are incorrectly indexed by values (or ranges) that exceed their bounds. These two problems are exacerbated by generate blocks. While desirable for reusability and conciseness, the use of generate blocks to describe circuit families only makes the situation worse as it hides such inconsistencies. Inconsistencies in the generated code are only exposed after elaboration when the code is fully-expanded. In this paper we show that these inconsistencies can be pinned down prior to elaboration using static analysis. We combine dependent types and constraint generation to reduce the problem of detecting the aforementioned inconsistencies to a satisfiability problem. Once reduced, the problem can easily be solved with a standard satisfiability modulo theories (SMT) solver. In addition, this technique allows us to detect unreachable code when it resides in a block guarded by an unsatisfiable set of constraints. To illustrate these ideas, we develop a type system for Featherweight Verilog (FV), a core calculus of structural Verilog with generative constructs and previously defined elaboration semantics. We prove that a well-typed FV description will always elaborate into an inconsistency-free description. We also provide an open-source implementation demonstrating our approach.
This paper presents a library based on improving sequences and demonstrates that they are effective for pruning unnecessary computations while retaining program clarity. An improving sequence is a monotonic sequence of approximation values of a final value that are improved gradually according to some ordering relation. A computation using improving sequences proceeds by demanding for the next approximation value. If an approximation value in the middle of the improving sequence has sufficient information to yield the result of some part of the program, the computations that produce the remaining values can be pruned. By combining suitable improving sequences and primitive functions defined for the sequences, we can write efficient programs in the same form as simple and naive programs. We give examples that show the effectiveness of improving sequences and show by program calculation that a simple minimax-like program using improving sequences implements a well-known branch-and-bound searching algorithm.
Danvy’s functional unparsing problem (Danvy in J. Funct. Program. 8(6), 621–625, 1998) is to implement a type-safe ‘printf’ function, which converts a sequence of heterogeneous arguments to a string according to a given format. The dual problem is to implement a type-safe ‘scanf’ function, which extracts a sequence of heterogeneous arguments from a string by interpreting (Friedman and Wand in LFP, pp. 348–355, 1984 and in Essentials of Programming Languages, MIT Press, 2008) the same format as an equally heterogeneous sequence of patterns that binds zero or more variables. We derive multiple solutions to both problems (Wand in J. ACM 27(1), 164–180, 1980) from their formal specifications (Wand in Theor. Comput. Sci. 20(1), 3–32, 1982).
In this paper, we introduce Continuation Passing C (CPC), a programming language for concurrent systems in which native and cooperative threads are unified and presented to the programmer as a single abstraction. The CPC compiler uses a compilation technique, based on the CPS transform, that yields efficient code and an extremely lightweight representation for contexts. We provide a proof of the correctness of our compilation scheme. We show in particular that lambda-lifting, a common compilation technique for functional languages, is also correct in an imperative language like C, under some conditions enforced by the CPC compiler. The current CPC compiler is mature enough to write substantial programs such as Hekate, a highly concurrent BitTorrent seeder. Our benchmark results show that CPC is as efficient, while using significantly less space, as the most efficient thread libraries available.
Staging is a powerful language construct that allows a program at one stage to manipulate and specialize a program at the next. We propose ML as a new staged calculus designed with novel features for staged programming in modern computing platforms such as embedded systems. A distinguishing feature of ML is a model of process separation, whereby different stages of computation are executed in different process spaces. Our language also supports dynamic type specialization via type abstraction, dynamic type construction, and a limited form of type dependence. ML is endowed with a largely standard metatheory, including type preservation and type safety results. We discuss the utility of our language via code examples from the domain of wireless sensor network programming.
Functional programs often combine separate parts using intermediate data structures for communicating results. Programs so defined are modular, easier to understand and maintain, but suffer from inefficiencies due to the generation of those gluing data structures. To eliminate such redundant data structures, some program transformation techniques have been proposed. One such technique is shortcut fusion, and has been studied in the context of both pure and monadic functional programs. In this paper, we study several shortcut fusion extensions, so that, alternatively, circular or higher-order programs are derived. These extensions are also provided for effect-free programs and monadic ones. Our work results in a set of generic calculation rules, that are widely applicable, and whose correctness is formally established.
