3rd International Summer School on Advanced Functional Programming

The school consists of four parts:

  1. Haskell Tutorial
  2. The School on Advanced Functional Programming
    1. Sorting Morphisms, Lex Augusteijn (Philips Research Laboratories, the Netherlands)
    2. Generic Programs - An Introduction - , Roland Backhouse (Eindhoven University) and Patrik Jansson (Chalmers University of Technology) and Johan Jeuring (Utrecht University) and Lambert Meertens (CWI and Utrecht University)
    3. Designing and Implementing Combinator Languages, Doaitse Swierstra (Utrecht University) and Pablo Azero (Utrecht University) and Joao Saraiva (Utrecht and Minho University)
    4. Functional Scripting, Erik Meijer and Daan Leijen (Utrecht University)
    5. CAYENNE - A Language With Dependent Types, Lennart Augustsson (Chalmers University of Technology)
    6. Generic Program Transformation, Oege de Moor and Ganesh Sittampalan (Oxford University)
    7. Using MetaML: A Staged Programming Language, Tim Sheard (Oregon Graduate Institute)
  3. Special Tutorials
  4. Students Workshop

A: Haskell Tutorial

On Sunday before the actual school begins it will be possible to attend a special course, where the main concepts of modern functional programming are reviewed. Time will also be spent on getting acquainted with the language Haskell. The goal of this course is to familiarize students with the notation and basic concepts which are assumed in most of the lectures.

The lecture notes
The Haskell Report

The course will be given by José Barros and João Almeida, from Minho.

B: The School on Advanced Functional Programming

1) Sorting Morphisms

Lecturer: Lex Augusteijn (Philips Research Laboratories, the Netherlands)

Sorting algorithms can be classified in many different ways. The way presented here is by expressing the algorithms as functional programs and to classify them by means of their recursion patterns . These patterns on their turn can be classified as the natural recursion patterns that destruct or construct a given data-type, the so called cata- and anamorphisms respectively. We show that the selection of the recursion pattern can be seen as the major design decision, in most cases leaving no more room for more decisions in the design of the sorting algorithm. It is also shown that the use of alternative data structures may lead to new sorting algorithms.

This presentation also serves as a gentle, light-weight, introduction into the various morphisms.
The lecture notes

2) Construction and Implementation of Generic Programs

Lecturers: Roland Backhouse (Eindhoven University) and Johan Jeuring (Utrecht University)

Generic programming is about making programs more useful by making them more general. This series of lectures will introduce a framework for constructing and reasoning about generic programs based on recent developments in functional programming.

Generic programming has a number of advantages. It makes it possible to write programs that solve a class of problems once and for all, instead of writing new code over and over again for each different instance. Furthermore, it pays to spend time on writing efficient and reliable code.

The theoretical basis of the framework will be presented and illustrated by a series of carefully chosen examples. During the course of the lectures the students will be challenged to solve a number of exercises in generic program construction in interaction with the lecturer. Additionally, practical experience of the techniques will be gained using [PolyP], a preprocessor to the Haskell compiler.

The lectures are divided into four parts:

The Basis
The [generic] programs we will discuss are called "polytypic" programs because they are parametrized by data types. The initial lectures will present the theoretical basis for polytypism. We will discuss how algebras and data types can be characterized in such a way that parametrization by data types becomes feasible.
In this lecture we will discuss PolyP, an extension to the programming language Haskell that facilitates the practical implementation of polytypic programs. Simple illustrations of polytypic programs will be presented, and exercises will be set giving hands-on experience of the techniques.
Generic Unification
Generic unification is an example of a substantial programming task that has both theoretical and practical interest. We will show how the program is specified, derived and implemented.
Deeper issues
In this final lecture we will discuss some of the (many) challenges that remain in the field of generic programming. The focus will be on the issue of what it means for a program to be ``generic''. We will review a formal characterization of ``being polymorphic'' due to Reynolds and show how this is extended to polytypic programs.
The lecture notes

3) Designing and Implementing Combinator Languages

Lecturer: Doaitse Swierstra (Utrecht University)

One of the advantages of functional languages is the ease with which another language can be ``embedded'' in a program. We will investigate what it is that makes this possible, and show some very general approaches for designing and implementing such embedded languages.

We will use a number of notational conventions and design-patterns, borrowed from the field of attribute grammars, and show how combinators can be designed in an incremental way. One of he basic steps we take is moving from a positional system for passing arguments, to a naming system. In this way we are liberated from the order in which parameters have to be passed as fixed by the type of the function, as is the case in traditional declarative languages like Haskell and Prolog. Despite its notational difference the actual mapping of the notation on a lazily evaluated functional program is straightforward. Finally we show how very efficient but definitely less straightforward implementations can be obtained automatically by analyzing and transforming the original definitions.

The lecture notes
Parsing combinators
Micro attribute grammar system
The attribute grammar system LRC

4) Functional Scriptingt

Lecturer: Erik Meijer (Utrecht University)

The new wave in programming is component based programming. In this paradigm, applications are built by gluing together off the shelf software binary components. It is important that reuse is based on binary code. There is no programming language in the world that is suitable for solving every possible problem so we want to choose the right tool for the right job when implementing a component. Without a binary standard it becomes impossible to utilize the vast amount of legacy code, for example highly optimized numeric libraries written in FORTRAN. Language independence is therefore more important than platform independence.

Microsoft's Component Object Model (COM) is a binary, language independent standard for component based software. We describe an interface between Haskell and Microsoft's Component Object Model (COM) that makes it easy to script COM components from a Haskell program and to package Haskell programs as COM components.

Of course COM is not the only possible component standard. Numerous research projects had similar goals, in particular CORBA. Unlike COM, though, CORBA is not a binary standard; to use CORBA for Haskell would required adding a language binding for Haskell to some manufacturer's ORB.

Of course Haskell in not the only possible scripting language. Numerous research projects had similar goals. However most contemporary scripting languages such as Visual Basic, ECMAScript, Perl, Tcl, etc. miss some of the essential properties of a truly high-level scripting language: strong typing, parametric polymorphism and overloading for flexibility of composition without sacrificing type safety, the unconditional principles of abstraction, parametrization, correspondence principles to exploit regularity and support reuse on the micro-level, laziness to hide non-termination effects on the way from the producer to the consumer, and monads to hide other side-effects on the way from the producer to the consumer.

The lecture notes

5) Cayenne - A Language With Dependent Types

Lecturer: Lennart Augustsson (Chalmers University of Technology)

Cayenne is a Haskell-like language. The main difference between Haskell and Cayenne is that Cayenne has dependent types, i.e., the result type of a function may depend on the argument value , and types of record components. Cayenne also combines the syntactic categories for value expressions and type expressions; thus reducing the number of language concepts.

Having dependent types and combined type and value expressions makes the language very powerful. It is powerful enough that a special module concept is unnecessary; ordinary records suffice. It is also powerful enough to encode predicate logic as the type level, allowing types to be used as specifications of programs. However, this power comes at a cost: type checking of Cayenne is undecidable. While this may appear to be a steep price to pay, it seems to work well in practice.

The lecture notes

6) Generic Program Transformation

Lecturer: Oege de Moor, (Oxford University)

When writing a program, especially in a high level language such as Haskell, the programmer is faced with a tension between abstraction and efficiency. A program that is easy to understand often fails to be efficient, while a more efficient solution often compromises clarity.

Fortunately Haskell permits us to reason about programs, so that we can start out with a program that is clear but inefficient, and transform it into a program that is efficient, but perhaps less readable. Indeed, such a transformation style of programming is as old as the subject of functional programming itself.

Programs developed in this style continue to suffer from a lack of readability, however: typically a functional programmer will develop his program on the back of an envelope, and only record the final results in his code. Of course he could document his ideas in comments, but as we all know, this is rarely done. Furthermore, when the programmer finds himself in a similar situation, using the same technique to develop a new piece of code, there is no way he can reuse the development recorded as a comment.

We claim that there is a handful of techniques that functional programmers routinely use to transform their programs, and that these techniques can themselves be coded as meta programs , allowing one to reuse the same optimization technique on different pieces of code. In these lectures we shall explore this claim, and ways in which such meta programs might be implemented.

Throughout, we shall take a cavalier attitude towards semantics. In particular, we shall chosen to ignore all issue of strictness: some of our transformation rules ought to state side conditions about strictness. While it is admittedly incorrect to ignore such side conditions, they would clutter the presentation and detract from the main thesis of these lectures.

The lecture notes

7) Using MetaML: A Staged Programming Language

Lecturer: Tim Sheard (Oregon Graduate Institute)

Many programs are a specific instances of a more general algorithm. We will show how, by using Metaprogramming (our name for staged programming, or run-time code generation), this step-wise specialization process can be precisely described. This allows programmers to write their own special purpose "partial evaluators" always under their complete control. However writing correct meta-programs quickly becomes a hazardous task since the addition of staging information complicates the process. MetaML helps the user by providing sophisticated tools that check both the level and the type of expressions. Type-checking is performed once and for all before any execution occurs. Type-checking succeeds only if every expression at every stage is well-typed. So, if the type-checker does not complain, the program won't go wrong at any stage of its execution. In addition, the system checks the soundness of binding-times. Broadly speaking, it prevents an expression e computed at level l from being used in another expression at level less than l (i.e. before l is computed).

The lecture notes

C: Special Tutorials

1) "Explosive" Programming Controlled by Calculation

Lecturer: Josť Nuno Oliveira (Minho University)

In the design of a functional library in the area of data-mining several algorithmic patterns have been identified which call for generic programming. Some of these have to do with flattening functions which arise in a particular group of hierarchical systems

In this paper we describe our efforts to make such functionalities generic. We start by a generic inductive construction of the intended class of hierarchical types. We conclude by relating the structure of the relevant base-functors with the algebraic structure which is required by the generic flattening functionality, in particular concerning its "deforestation" towards a linearly complex implementation.

The instances we provide as examples include the widely known bill of materials "explode" operation.

The lecture notes

2) The Fall and Rise of Functional Programming

Lecturer: Rafael Lins (Universidade Federal de Pernambuco)

Functional programming is a neat and very high-level programming paradigm, in which a program is formed by a series of function definitions.

This paper analyses the evolution of functional programming within almost four decades of its existence.

The lecture notes


D: Students Workshop

This workshop aims to provide a forum for presentation of recent research by PhD students attending the school. Everyone intending to make a presentation should submit an extended abstract along with the registration form. The extended abstracts will appear as a Technical Report of Universidade do Minho.
The Workshop Homepage