Skip to main content
main-content

Über dieses Buch

This book constitutes the thoroughly refereed post-conference
proceedings of the 22nd International Symposium on Implementation and
Applications of Functional Languages, IFL 2010, held in Alphen aan den
Rijn, The Netherlands, in September 2010.

The 13 revised full papers presented were carefully reviewed and were
selected from 31 submissions. The IFL symposia bring together
researchers and practitioners that are actively engaged in the
implementation and the use of functional and function based programming
languages. Every year IFL provides a venue for the presentation and
discussion of new ideas and concepts, of work in progress, and of
publication-ripe results.

Inhaltsverzeichnis

Frontmatter

Haskell Boards the Ferry

Database-Supported Program Execution for Haskell
Relational database management systems can be used as a coprocessor for general-purpose programming languages, especially for those program fragments that carry out data-intensive and data-parallel computations. In this paper we present a Haskell library for database-supported program execution. Data-intensive and data-parallel computations are expressed using familiar combinators from the standard list prelude and are entirely executed on the database coprocessor. Programming with the expressive list comprehension notation is also supported. The library, in addition to queries of basic types, supports computations over arbitrarily nested tuples and lists. The implementation avoids unnecessary data transfer and context switching between the database coprocessor and the programming language runtime by ensuring that the number of generated relational queries is only determined by the program fragment’s type and not by the database size.
George Giorgidze, Torsten Grust, Tom Schreiber, Jeroen Weijers

Theory and Practice of Fusion

There are a number of approaches for eliminating intermediate data structures in functional programs—this elimination is commonly known as fusion. Existing fusion strategies are built upon various, but related, recursion schemes, such as folds and unfolds. We use the concept of recursive coalgebras as a unifying theoretical and notational framework to explore the foundations of these fusion techniques. We first introduce the calculational properties of recursive coalgebras and demonstrate their use with proofs and derivations in a calculational style, then provide an overview of fusion techniques by bringing them together in this setting. We also showcase these developments with examples in Haskell.
Ralf Hinze, Thomas Harper, Daniel W. H. James

Orthogonal Serialisation for Haskell

Data serialisation is a crucial feature of real-world programming languages, often provided by standard libraries or even built-in to the language. However, a number of questions arise when the language in question uses demand-driven evaluation and supports higher-order functions, as is the case for the lazy functional language Haskell. To date, solutions to serialisation for Haskell generally do not support higher-order functions and introduce additional strictness.
This paper investigates a novel approach to serialisation of Haskell data structures with a high degree of flexibility, based on runtime support for parallel Haskell on distributed memory platforms. This serialisation has highly desirable and so-far unrivalled properties: it is truly orthogonal to evaluation and also does not require any type class mechanisms. Especially, (almost) any kind of value can be serialised, including functions and IO actions. We outline the runtime support on which our serialisation is based, and present an API of Haskell functions and types which ensure dynamic type safety of the serialisation process. Furthermore, we explore and exemplify potential application areas for orthogonal serialisation.
Jost Berthold

Introducing the PilGRIM: A Processor for Executing Lazy Functional Languages

Processor designs specialized for functional languages received very little attention in the past 20 years. The potential for exploiting more parallelism and the developments in hardware technology, ask for renewed investigation of this topic. In this paper, we use ideas from modern processor architectures and the state of the art in compilation, to guide the design of our processor, the PilGRIM. We define a high-level instruction set for lazy functional languages and show the processor architecture, that can efficiently execute these instructions.
Arjan Boeijink, Philip K. F. Hölzenspies, Jan Kuper

Automating Derivations of Abstract Machines from Reduction Semantics:

A Generic Formalization of Refocusing in Coq
We present a generic formalization of the refocusing transformation for functional languages in the Coq proof assistant. The refocusing technique, due to Danvy and Nielsen, allows for mechanical transformation of an evaluator implementing a reduction semantics into an equivalent abstract machine via a succession of simple program transformations. So far, refocusing has been used only as an informal procedure: the conditions required of a reduction semantics have not been formally captured, and the transformation has not been formally proved correct.
The aim of this work is to formalize and prove correct the refocusing technique. To this end, we first propose an axiomatization of reduction semantics that is sufficient to automatically apply the refocusing method. Next, we prove that any reduction semantics conforming to this axiomatization can be automatically transformed into an abstract machine equivalent to it. The article is accompanied by a Coq development that contains the formalization of the refocusing method and a number of case studies that serve both as an illustration of the method and as a sanity check on the axiomatization.
Filip Sieczkowski, Małgorzata Biernacka, Dariusz Biernacki

From Bayesian Notation to Pure Racket via Discrete Measure-Theoretic Probability in λ ZFC

Bayesian practitioners build models of the world without regarding how difficult it will be to answer questions about them. When answering questions, they put off approximating as long as possible, and usually must write programs to compute converging approximations. Writing the programs is distracting, tedious and error-prone, and we wish to relieve them of it by providing languages and compilers.
Their style constrains our work: the tools we provide cannot approximate early. Our approach to meeting this constraint is to 1) determine their notation’s meaning in a suitable theoretical framework; 2) generalize our interpretation in an uncomputable, exact semantics; 3) approximate the exact semantics and prove convergence; and 4) implement the approximating semantics in Racket (formerly PLT Scheme). In this way, we define languages with at least as much exactness as Bayesian practitioners have in mind, and also put off approximating as long as possible.
In this paper, we demonstrate the approach using our preliminary work on discrete (countably infinite) Bayesian models.
Neil Toronto, Jay McCarthy

Dependently Typed Attribute Grammars

Attribute Grammars (AGs) are a domain-specific language for functional and composable descriptions of tree traversals. Given such a description, it is not immediately clear how to state and prove properties of AGs formally. To meet this challenge, we apply dependent types to AGs. In a dependently typed AG, the type of an attribute may refer to values of attributes. The type of an attribute is an invariant, the value of an attribute a proof for that invariant. Additionally, when an AG is cycle-free, the composition of the attributes is logically consistent. We present a lightweight approach using a preprocessor in combination with the dependently typed language Agda.
Arie Middelkoop, Atze Dijkstra, S. Doaitse Swierstra

The Design and Implementation of Feldspar

An Embedded Language for Digital Signal Processing
Feldspar is a domain specific language, embedded in Haskell, for programming digital signal processing algorithms. The final aim of a Feldspar program is to generate low level code with good performance. Still, we chose to provide the user with a purely functional DSL. The language is implemented as a minimal, deeply embedded core language, with shallow extensions built upon it. This paper presents full details of the essential parts of the implementation. Our initial conclusion is that this approach works well in our domain, although much work remains.
Emil Axelsson, Koen Claessen, Mary Sheeran, Josef Svenningsson, David Engdal, Anders Persson

Purity in Erlang

Motivated by a concrete goal, namely to extend Erlang with the ability to employ user-defined guards, we developed a parameterized static analysis tool called Purity, that classifies functions as referentially transparent (i.e., side-effect free with no dependency on the execution environment and never raising an exception), side-effect free with no dependencies but possibly raising exceptions, or side-effect free but with possible dependencies and possibly raising exceptions. We have applied Purity on a large corpus of Erlang code bases and report experimental results showing the percentage of functions that the analysis definitely classifies in each category. Moreover, we discuss how our analysis has been incorporated on a development branch of the Erlang/OTP compiler in order to allow extending the language with user-defined guards.
Mihalis Pitidis, Konstantinos Sagonas

iTask as a New Paradigm for Building GUI Applications

The iTask system is a combinator library written in Clean offering a declarative, domain-specific language for defining workflows. From a declarative specification, a complete multi-user, web-enabled, workflow management system (WFMS) is generated. In the iTask paradigm, a workflow is a definition in which interactive elements are defined by editors on model values (abstracting from concrete GUI implementation details). The order of their appearance is calculated dynamically using combinator functions (abstracting from concrete synchronisation details). Defining interactive elements and the order of their appearance are also major concerns when programming GUI applications. For this reason, the iTask paradigm is potentially suited to program GUI applications as well. However, the iTask system was designed for a different application domain and lacks a number of key features to make it suited for programming GUI applications. In this paper, we identify these key features and show how they can be added to the iTask system in an orthogonal way, thus creating a new paradigm for programming GUI applications.
Steffen Michels, Rinus Plasmeijer, Peter Achten

Improving Your CASH Flow: The Computer Algebra SHell

This paper describes CASH (the Computer Algebra SHell), a new interface that allows Haskell programmers to access the complete functionality of a number of computer algebra systems directly and interactively. Using CASH, Haskell programmers can access previously-unavailable mathematical software. Additionally, users of computer algebra systems can exploit the rapidly growing Haskell code base and its rich set of libraries. In particular, CASH provides a simple and effective interface for users of computer algebra systems to parallelise their algorithms using domain-specific skeletons written in Haskell.
Christopher Brown, Hans-Wolfgang Loidl, Jost Berthold, Kevin Hammond

Concurrent Non-deferred Reference Counting on the Microgrid: First Experiences

We present a first evaluation of our novel approach for non-deferred reference counting on the Microgrid many-core architecture. Non-deferred reference counting is a fundamental building block of implicit heap management of functional array languages in general and Single Assignment C in particular. Existing lock-free approaches for multi-core and SMP settings do not scale well for large numbers of cores in emerging many-core platforms. We, instead, employ a dedicated core for reference counting and use asynchronous messaging to emit reference counting operations. This novel approach decouples computational workload from reference-counting overhead. Experiments using cycle-accurate simulation of a realistic Microgrid show that, by exploiting asynchronism, we are able to tolerate even worst-case reference counting loads reasonably well. Scalability is essentially limited only by the combined sequential runtime of all reference counting operations, in accordance with Amdahl’s law. Even though developed in the context of Single Assignment C and the Microgrid, our approach is applicable to a wide range of languages and platforms.
Stephan Herhut, Carl Joslin, Sven-Bodo Scholz, Raphael Poss, Clemens Grelck

Composing Reactive GUIs in F# Using WebSharper

We present a generic library for constructing composable and interactive user interfaces in a declarative style. The paper introduces flowlets, an extension of formlets[3,2] providing interactivity. Real-world examples are given using the current implementation that compiles flowlets defined in F# to JavaScript with WebSharper.
Joel Bjornson, Anton Tayanovskyy, Adam Granicz

Backmatter

Weitere Informationen

Premium Partner

BranchenIndex Online

Die B2B-Firmensuche für Industrie und Wirtschaft: Kostenfrei in Firmenprofilen nach Lieferanten, Herstellern, Dienstleistern und Händlern recherchieren.

Whitepaper

- ANZEIGE -

Best Practices für die Mitarbeiter-Partizipation in der Produktentwicklung

Unternehmen haben das Innovationspotenzial der eigenen Mitarbeiter auch außerhalb der F&E-Abteilung erkannt. Viele Initiativen zur Partizipation scheitern in der Praxis jedoch häufig. Lesen Sie hier  - basierend auf einer qualitativ-explorativen Expertenstudie - mehr über die wesentlichen Problemfelder der mitarbeiterzentrierten Produktentwicklung und profitieren Sie von konkreten Handlungsempfehlungen aus der Praxis.
Jetzt gratis downloaden!

Bildnachweise