Skip to main content
main-content

Über dieses Buch

This book constitutes the thoroughly refereed post-proceedings of the 20th International Workshop on Implementation and Applications of Functional Languages, IFL 2008, held in Hatfield, UK, in September 2008. The 15 revised full papers presented were carefully reviewed and selected from 31 submissions. Topics of interest cover a wide range from novel language designs, theoretical underpinnings, compilation and optimisation techniques for diverse hardware architectures, to applications, programming techniques and novel tools.

Inhaltsverzeichnis

Frontmatter

Scans and Convolutions— A Calculational Proof of Moessner’s Theorem

The paper introduces two corecursion schemes for stream-generating functions, scans and convolutions, and discusses their properties. As an application of the framework, a calculational proof of Paasche’s generalisation of Moessner’s intriguing theorem is presented.

Ralf Hinze

From Functional Logic Programs to Purely Functional Programs Preserving Laziness

Functional logic languages extend the setting of functional programming by non-deterministic choices, free variables and narrowing.

Most existing approaches to simulate logic features in functional languages do not preserve laziness, i.e., they can only model strict logic programming like in Prolog. Lazy functional logic programming however, has interesting properties supporting a more declarative style of programming search without sacrificing efficiency.

We will present a recently developed technique to reduce all logic extensions to the single problem of generating unique identifiers. The impact of this reduction is a general scheme for compiling functional logic programs to lazy functional programs without side effects.

One of the design goals is that the purely functional parts of a program should not suffer from significant run-time overhead. Preliminary experiments confirm our hope for significant improvements of run-time performance even for non-deterministic programs but suggest further work to improve the memory requirements of those.

Bernd Braßel, Sebastian Fischer

An Interaction Net Implementation of Closed Reduction

Closed reduction is a very efficient reduction strategy for the lambda calculus, which is explained using a simple form of explicit substitutions. This paper introduces this strategy, and gives an implementation as a system of interaction nets. We obtain one of the most efficient implementations of this kind to date.

Ian Mackie

Implementation Architecture and Multithreaded Runtime System of S-Net

S-

Net

is a declarative coordination language and component technology aimed at modern multi-core/many-core architectures and systems-on-chip. It builds on the concept of stream processing to structure networks of communicating asynchronous components, which can be implemented using a conventional (sequential) language. In this paper we present the architecture of our S-

Net

implementation. After sketching out the interplay between compiler and runtime system, we characterise the deployment and operational behaviour of our multithreaded runtime system for contemporary multi-core processors. Preliminary runtime figures demonstrate the effectiveness of our approach.

Clemens Grelck, Frank Penczek

Parsing Mixfix Operators

A simple grammar scheme for expressions containing mixfix operators is presented. The scheme is parameterised by a precedence relation which is only restricted to be a directed acyclic graph; this makes it possible to build up precedence relations in a modular way. Efficient and simple implementations of parsers for languages with user-defined mixfix operators, based on the grammar scheme, are also discussed. In the future we plan to replace the support for mixfix operators in the language Agda with a grammar scheme and an implementation based on this work.

Nils Anders Danielsson, Ulf Norell

Descriptor-Free Representation of Arrays with Dependent Types

Besides element type and values, a multidimensional array is characterized by the number of axes (rank) and their respective lengths (shape vector). Both properties are essential for bounds checking and to compute linear offsets into heap memory at run time. In order to have an array’s rank and shape available at any time during program execution, both are typically kept in an array descriptor that is maintained at run time in addition to the array itself.

In this paper, we propose a different approach: we treat array rank and shape as first-class citizens themselves. Firstly, we use dependent types to reflect structural properties of arrays in the type system. Secondly, we annotate a program with the explicit array properties wherever necessary. This choice not only renders implicit run time array descriptors obsolete, but exposing all rank and shape computations explicitly in intermediate code also allows us to perform extensive compile time optimisation on them. We have implemented the proposed approach in our experimental array language

Qube

; preliminary experimental results indicate the suitability of the proposed approach.

Kai Trojahner, Clemens Grelck

Collected Size Semantics for Functional Programs over Lists

This work introduces collected size semantics of strict functional programs over lists. The collected size semantics of a function definition is a multivalued size function that collects the dependencies between every possible output size and the corresponding input sizes. Such functions annotate standard types and are defined by conditional rewriting rules generated during type inference.

We focus on the connection between the rewriting rules and lower and upper bounds on the multivalued size functions, when the bounds are given by piecewise polynomials. We show how, given a set of conditional rewriting rules, one can infer bounds that define an indexed family of polynomials that approximates the multivalued size function.

Using collected size semantics we are able to infer non-monotonic and non-linear lower and upper polynomial bounds for many functional programs. As a feasibility study, we use the procedure to infer lower and upper polynomial size-bounds on typical functions of a list library.

Olha Shkaravska, Marko van Eekelen, Alejandro Tamalet

Embedding a Functional Hybrid Modelling Language in Haskell

In this paper we present the first investigation into the implementation of a Functional Hybrid Modelling language for non-causal modelling and simulation of physical systems. In particular, we present a simple way to handle connect constructs: a facility for composing model fragments present in some form in most non-causal modelling languages. Our implementation is realised as a domain-specific language embedded in Haskell. The method of embedding employs quasiquoting, thus demonstrating the effectiveness of this approach for languages that are not suitable for embedding in more traditional ways. Our implementation is available on-line, and thus the first publicly available prototype implementation of a Functional Hybrid Modelling language.

George Giorgidze, Henrik Nilsson

Obsidian: A Domain Specific Embedded Language for Parallel Programming of Graphics Processors

We present a domain specific language, embedded in Haskell, for general purpose parallel programming on GPUs. Our intention is to explore the use of

connection patterns

in parallel programming. We briefly present our earlier work on hardware generation, and outline the current state of GPU architectures and programming models. Finally, we present the current status of the

Obsidian

project, which aims to make GPU programming easier, without relinquishing detailed control of GPU resources. Both a programming example and some details of the implementation are presented. This is a report on work in progress.

Joel Svensson, Mary Sheeran, Koen Claessen

A Library for Processing Ad hoc Data in Haskell

Embedding a Data Description Language

Ad hoc data formats, i.e. semistructured non-standard data formats, are pervasive in many domains that need software tools — bioinformatics, demographic surveys, geophysics and network software are just a few. Building tools becomes easier if parsing and other standard input-output processing can be automated. Modern approaches for dealing with ad hoc data formats consist of domain specific languages based on type systems. Compilers for these languages generate data structures and parsing functions in a target programming language in which tools and applications are then written. We present a monadic library in Haskell that implements a data description language. Using our library, Haskell programmers have access to data description primitives that can be used for parsing and that can be integrated with other libraries and application programs without the need of yet another compiler.

Yan Wang, Verónica Gaspes

iEditors: Extending iTask with Interactive Plug-ins

The

iTask

library of

Clean

enables the user to specify web-enabled workflow systems on a high level of abstraction. Details like client-server communication, storage and retrieval of state information,

HTML

generation, and web form handling are all handled automatically. Using only standard

HTML

web browser elements also has a disadvantage: it does not offer the same level of interaction as we are used to from desktop applications. Browser plug-ins can fill this gap. They make it possible to extend web-applications with interactive functionality like the making of drawings. In this paper we explain how plug-ins can be nicely integrated in the

iTask

system. A special feature of the integration is the possibility for a plug-in to use

Clean

functions as call-back mechanism for the handling of events. These call-backs can be handled on the server as well as on the client. As a result we are now able to create interactive

iTask

applications (

iEditors

) using plug-ins like graphical editors. Although complicated, distributed multi-user applications can be created in this way, reasoning about the program remains easy since all code is generated from one and the same source: the high-level

iTask

specification in

Clean

.

Jan Martin Jansen, Rinus Plasmeijer, Pieter Koopman

An Executable and Testable Semantics for iTasks

The

iTask

system is an easy to use combinator library for specifying dynamic data dependent workflows in a very flexible way. The specified workflows are executed as a multi-user web-application. The implementation of the

iTask

system is fairly complicated. Hence we cannot use it for reasoning about the semantics of workflows in the

iTask

system. In this paper we define an executable semantics that specifies how workflows react on events generated by the workers executing them. The semantics is used to explain

iTask

and to reason about

iTask

. Based on this semantics we define a mathematical notion of equivalence of tasks and show how this equivalence for tasks can be approximated automatically. Advantages of this executable semantics are: it is easy to validate the semantics by interactive simulation; properties of the semantics can be tested by our model-based test system

G

 ∀ 

st

.

G

 ∀ 

st

can test a large number of properties within seconds. These tests appeared to be a good indication about the consistency of the specified semantics and equivalence relation for tasks. The automatic testing of properties was very helpful in the development of the semantics. The contribution of this paper is a semantics for

iTask

as well as the method used to construct this operational semantics.

Pieter Koopman, Rinus Plasmeijer, Peter Achten

Monatron: An Extensible Monad Transformer Library

Monads are pervasive in functional programming. In order to reap the benefits of their abstraction power, combinator libraries for monads are necessary. Monad transformers provide the basis for such libraries, and are based on a design that has proved to be successful. In this article, we show that this design has a number of shortcomings and provide a new design that builds on the strengths of the traditional design, but addresses its problems.

Mauro Jaskelioff

Catch Me If You Can

Looking for Type-Safe, Hierarchical, Lightweight, Polymorphic and Efficient Error Management in OCaml

This is the year 2008 and ML-style exceptions are everywhere. Most modern languages, whether academic or industrial, feature some variant of this mechanism. Languages such as Java even feature static coverage-checking for such exceptions, something not available for ML languages, at least not without resorting to external tools.

In this document, we demonstrate a design principle and a tiny library for managing errors in a functional manner, with static coverage-checking, automatically-inferred, structurally typed and hierarchical exceptional cases, with a reasonable run-time penalty. Our work is based on OCaml and features monads, polymorphic variants, compile-time code rewriting and trace elements of black magic.

David Teller, Arnaud Spiwack, Till Varoquaux

Between Types and Tables

Using Generic Programming for Automated Mapping between Data Types and Relational Databases

In today’s digital society, information systems play an important role in many organizations. While their construction is a well understood software engineering process, it still requires much engineering effort. The de facto storage mechanism in information systems is the relational database. Although the representation of data in these databases is optimized for efficient storage, it is less suitable for use in the software components that manipulate the data. Therefore, much of the construction of an information system consists of programming translations between the database and a more convenient representation in the software.

In this paper we present an approach which automates this work for data entry applications, by providing generic versions of the elementary CRUD (Create, Read, Update, Delete) operations. In the spirit of model based development we use Object Role Models, which are normally used to design databases, to derive not only a database, but also a set of data types in Clean to hold data during manipulation. These types represent all information related to a conceptual entity as a single value, and contain enough information about the database to enable automatic mapping. For data entry applications this means that all database operations can be handled by a single generic function.

To illustrate the viability of our approach, a prototype library, which performs this mapping, and an example information system have been implemented.

Bas Lijnse, Rinus Plasmeijer

Backmatter

Weitere Informationen

Premium Partner

Neuer Inhalt

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