Skip to main content
main-content

Über dieses Buch

This book constitutes the thoroughly refereed revised selected papers of the 19th International Symposium on Trends in Functional Programming, TFP 2018, held in Gothenburg, Sweden, in June 2018. The 7 revised full papers were selected from 13 submissions and present papers 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

Colocation of Potential Parallelism in a Distributed Adaptive Run-Time System for Parallel Haskell

Abstract
This paper presents a novel variant of work stealing for load balancing in a distributed graph reducer, executing a semi-explicit parallel dialect of Haskell. The key concept of this load-balancer is colocating related sparks (potential parallelism) using maximum prefix matching on the encoding of the spark’s ancestry within the computation tree, reconstructed at run time, in spark selection decisions. We evaluate spark colocation in terms of performance and scalability on a set of five benchmarks on a Beowulf-class cluster of multi-core machines using up to 256 cores. In comparison to the baseline mechanism, we achieve speedup increase of up to 46% for three out of five applications, due to improved locality and load balance throughout the execution as demonstrated by profiling data. For one less scalable program and one program with excessive amounts of very fine-grained parallelism we observe drops in speedup by \(17\%\) and \(42\%\), respectively. Overall, spark colocation results in reduced mean time to fetch the required data and in higher degree of parallelism of finer granularity, which is most beneficial on higher PE numbers.
Evgenij Belikov, Hans-Wolfgang Loidl, Greg Michaelson

Reversible Session-Based Concurrency in Haskell

Abstract
A reversible semantics enables to undo computation steps. Reversing message-passing, concurrent programs is a challenging and delicate task; one typically aims at causally consistent reversible semantics. Prior work has addressed this challenge in the context of a process model of multiparty protocols (or choreographies). In this paper, we describe a Haskell implementation of this reversible operational semantics. We exploit algebraic data types to faithfully represent three core ingredients: a process calculus, multiparty session types, and forward and backward reduction semantics. Our implementation bears witness to the convenience of pure functional programming for implementing reversible languages.
Folkert de Vries, Jorge A. Pérez

Intrinsic Currying for C++ Template Metaprograms

Abstract
C++ template metaprogramming is a form of strict functional programming, with a notable absence of intrinsic support for elementary higher-order operations. We describe a variadic template metaprogramming library which offers a model of implicitly curried, left-associative metafunction application through juxtaposition; inspired by languages such as Haskell, OCaml and F\(^\sharp \). New and existing traits and metafunctions, constructed according to conventional idioms, seemlessly take advantage of the framework’s features. Furthermore, a distinctive versatility is exposed, allowing a user to define higher-order metafunction classes using an equational definition syntax; without recourse to elaborate nested metafunctions. The primary type expression evaluator of the library is derived from a single application of an elementary folding combinator for type lists. The definition of the fold’s binary operator argument is therefore a focal point; and constructed mindful that substitution failure of a template parameter’s deduced type produces no compilation error. Two distinctive features of C++ metafunctions require particular consideration: zero argument metafunctions; and variadic metafunctions. We conclude by demonstrating characteristics of the library’s main evaluation metafunction in conjunction with the universal property of an updated right-fold combinator, to compose a range of metafunctions including map, reverse, left-fold, and the Ackermann function.
Paul Keir, Andrew Gozillon, Seyed Hossein Haeri

Towards Optic-Based Algebraic Theories: The Case of Lenses

Abstract
Optics provide rich abstractions and composition patterns to access and manipulate immutable data structures. However, the state of real applications is mostly handled through databases, caches, web services, etc. In this effectful setting, the usefulness of optics is severely limited, whereas algebraic theories, thanks to their potential to abstract away from particular infrastructures, shine. Unfortunately, there is a severe lack of standard algebraic theories, e.g. like MonadState, that programmers can reuse to avoid writing their domain repositories from scratch. This paper argues that optics can serve as a fruitful metaphor to design a rich catalogue of state-based algebraic theories, and focuses on the paradigmatic case of lenses. It shows how lenses can be generalised into an algebraic theory; how compositionality of these algebraic theories can be founded on lens composition; and how to exploit the resulting abstractions in the modular design of data layers. The paper systematically uses Coq for all its definitions and proofs.
J. López-González, Juan M. Serrano

Saint: An API-Generic Type-Safe Interpreter

Abstract
Typed functional programming allows us to write interesting programs without sacrificing type safety. Programs that expose their API to an open world, however, are faced with the problem of dynamic type checking. In Haskell, existing techniques that address this problem, such as Typeable and Dynamic, are often closed and difficult to extend. We have constructed an extensible Haskell library for describing APIs using annotated type representations. As a result, API calls can be interpreted in a type-safe manner without extra programming effort. In addition, the user has full control over the universe of allowed types, which helps to catch misconceptions in an early stage. We have applied our technique to connect a real-world DSL (GRACe) to a JavaScript GUI.
Maximilian Algehed, Patrik Jansson, Sólrún Halla Einarsdóttir, Alex Gerdes

Improving Haskell

Abstract
Lazy evaluation is a key feature of Haskell, but can make it difficult to reason about the efficiency of programs. Improvement theory addresses this problem by providing a foundation for proofs of program improvement in a call-by-need setting, and has recently been the subject of renewed interest. However, proofs of improvement are intricate and require an inequational style of reasoning that is unfamiliar to most Haskell programmers. In this article, we present the design and implementation of an inequational reasoning assistant that provides mechanical support for improvement proofs, and demonstrate its utility by verifying a range of improvement results from the literature.
Martin A. T. Handley, Graham Hutton

High-Performance Defunctionalisation in Futhark

Abstract
General-purpose massively parallel processors, such as GPUs, have become common, but are difficult to program. Pure functional programming can be a solution, as it guarantees referential transparency, and provides useful combinators for expressing data-parallel computations. Unfortunately, higher-order functions cannot be efficiently implemented on GPUs by the usual means. In this paper, we present a defunctionalisation transformation that relies on type-based restrictions on the use of expressions of functional type, such that we can completely eliminate higher-order functions in all cases, without introducing any branching. We prove the correctness of the transformation and discuss its implementation in Futhark, a data-parallel functional language that generates GPU code. The use of these restricted higher-order functions has no impact on run-time performance, and we argue that we gain many of the benefits of general higher-order functions, without in most practical cases being hindered by the restrictions.
Anders Kiel Hovgaard, Troels Henriksen, Martin Elsman

Backmatter

Weitere Informationen

Premium Partner

    Bildnachweise