Trends in Functional Programming

16th International Symposium, TFP 2015, Sophia Antipolis, France, June 3-5, 2015. Revised Selected Papers

herausgegeben von: Manuel Serrano, Jurriaan Hage

Verlag: Springer International Publishing

Buchreihe : Lecture Notes in Computer Science

Enthalten in: Springer Professional "Wirtschaft+Technik" , Springer Professional "Technik" , Springer Professional "Wirtschaft"

Einloggen, um Zugang zu erhalten

Über dieses Buch

This book constitutes the thoroughly refereed revised selected papers of the 16th International Symposium on Trends in Functional Programming, TFP 2015, held in Sophia Antipolis, France, in June 2015. The 8 revised full papers included in this volume were carefully and selected from 26 submissions. TFP is an international forum for researchers with interests in all aspects of functional programming, taking a broad view of current and future trends in the area. It aspires to be a lively environment for presenting the latest research results, and other contributions, described in draft papers submitted prior to the symposium.

Inhaltsverzeichnis

Frontmatter

Lightweight Higher-Order Rewriting in Haskell

Abstract

We present a generic Haskell library for expressing rewrite rules with a safe treatment of variables and binders. Both sides of the rules are written as typed EDSL expressions, which leads to syntactically appealing rules and hides the underlying term representation. Matching is defined as an instance of Miller’s higher-order pattern unification and has the same complexity as first-order matching. The restrictions of pattern unification are captured in the types of the library, and we show by example that the library is capable of expressing useful simplifications that might be used in a compiler.

Emil Axelsson, Andrea Vezzosi

Towards a Theory of Reach

Abstract

When testing a program, there are usually some parts that are rarely executed and hence more difficult to test. Finding inputs that guarantee that such parts are executed is an example of a reach problem, which in general seeks to ensure that targeted parts of a program are always executed. In previous work, Naylor and Runciman have developed a reachability solver for Haskell, based on the use of lazy narrowing from functional logic programming. Their work was focused on practical issues concerning implementation and performance. In this paper, we lay the groundwork for an underlying theory of such a system, by formally establishing the correctness of a simple reach solver.

Jonathan Fowler, Graham Huttom

Functional Testing of Java Programs

Abstract

This paper describes an approach to testing Java code using a functional programming language. Models for Java programs are expressed as Quviq Erlang QuickCheck properties, from which random tests are generated and executed. To remove the need for writing boilerplate code to interface Java and Erlang, a new library, JavaErlang, has been developed. The library provides a number of interesting features, e.g., it supports automatic garbage collection of Java objects communicated to Erlang, and permits Java classes to be written entirely in Erlang. Moreover, as the library is built on top of the Erlang distributed node concept, the Java program under test runs in isolation from the Erlang testing code. The chief advantage of this testing approach is that a functional programming language, with expressive data types and side-effect free libraries, is very suited to formulating models for imperative programs. The resulting testing methodology has been applied extensively to evaluate student Java exercises.

Clara Benac Earle, Lars-Åke Fredlund

Type Class Instances for Type-Level Lambdas in Haskell

Abstract

Haskell 2010 lacks flexibility in creating instances of type classes for type constructors with multiple type arguments. We would like to make the order of type arguments to a type constructor irrelevant to how type class instances can be specified. None of the currently available techniques in Haskell allows to do this in a satisfactory way.

To flexibly create type-class instances we have added the concept of type-level lambdas as anonymous type synonyms to Haskell. As higher-order unification of lambda terms in general is undecidable, we take a conservative approach to equality between type-level lambdas. We propose a number of small changes to the constraint solver that will allow type-level lambdas to be used in type class instances. We show that this satisfies our goal, while having only minor impact on existing Haskell code.

Thijs Alkemade, Johan Jeuring

Laminar Data Flow: On the Role of Slicing in Functional Data-Flow Programming

Research Paper

Abstract

We use the concept of laminar flow, as opposed to turbulent flow, as a metaphor for the decomposition of well-behaved purely functional data-flow programs into largely independent parts, necessitated by aspects with different execution constraints. In the context of the total functional data-flow language Sig, we identify three distinct but methodologically related implementation challenges, namely multi-rate scheduling, declarative initialization, and conditional execution, and demonstrate how they can be solved orthogonally, by decomposition using the standard program transformation technique, slicing.

Baltasar Trancón y Widemann, Markus Lepper

A Shallow Embedded Type Safe Extendable DSL for the Arduino

Abstract

This paper extends our method to construct a shallow embedded domain specific language, DSL, embedded in a function programming language. We show how one can add functions and tasks that are typed by the type system of the functional host language.

The DSL is clearly separated from its host functional language to facilitate the compilation to small executables in C++. The type system of the host language verifies the types in the DSL, including the types and proper use of variables. The DSL is extendable by new language constructs and interpretations without breaking any existing code. The type system guarantees that everything used in a DSL program is properly defined. We apply these techniques for a DSL to program Arduino microprocessor systems from Clean. The long term goal is to incorporate these microprocessors in the iTask system.

Pieter Koopman, Rinus Plasmeijer

Programmable Signatures

Abstract

When compiling Embedded Domain Specific Languages (EDSLs) into other languages, the compiler translates types in the source language into corresponding types in the target language. The translation is often driven by a small set of rules that map a single type in the source language into a single type in the target language. This simple approach is limiting when there are multiple possible mappings, and it may lead to poor interoperability and poor performance in the generated code. Instead of hard-wiring a single set of translation rules into a compiler, this paper introduces a small language that lets the programmer describe the mapping of each argument and function separately.

Anders Persson, Emil Axelsson

Termination Proofs for Recursive Functions in FoCaLiZe

Abstract

FoCaLiZe is a development environment allowing the writing of specifications, implementations and correctness proofs. It generates both OCaml (executable) and Coq code (for verification needs). This paper extends the language and the compiler to handle termination proofs relying on well-founded relations or measures. We propose an approach where the user’s burden is lightened as much as possible, leaving glue code to the compiler. Proofs are written using the declarative proof language provided by FoCaLiZe, and the automatic theorem prover Zenon. When compiling to Coq we rely on the Coq construct Function.

Catherine Dubois, François Pessaux

Backmatter

Titel: Trends in Functional Programming
herausgegeben von: Manuel Serrano
Jurriaan Hage
Verlag: Springer International Publishing
Electronic ISBN: 978-3-319-39110-6
Print ISBN: 978-3-319-39109-0
DOI: https://doi.org/10.1007/978-3-319-39110-6