Fortgeschrittene Konzepte der funktionalen Programmierung, Sommersemester 2015

Übersicht

TitelFortgeschrittene Konzepte der funktionalen Programmierung
SemesterSommersemester 2015
ModuleBachelorseminar (IN0014), Masterseminar (IN2107)
VoraussetzungenGrundlegende Kenntnisse in funktionaler Programmierung (z.B. Einführung in die Informatik 2 (IN0003))
SWS2
ECTS4
OrganisationJulian Brunner, Lars Hupel, Tobias Nipkow

Ablauf

Jeder Teilnehmer erhält ein Thema, zu welchem er oder sie eine schriftliche Ausarbeitung anfertigt und einen Vortrag vor den anderen Teilnehmern hält. Außerdem gibt jeder Teilnehmer kurze schriftliche Rezensionen zu den Ausarbeitungen zweier anderer Teilnehmer ab. Der genaue zeitliche Ablauf kann dem Abschnitt 'Termine' entnommen werden.

Belegung

Die Veranstaltung kann sowohl als Bachelorseminar als auch als Masterseminar belegt werden, wobei für jedes Thema angegeben ist, für welche Module es sich eignet. Einige Themen sind sowohl für das Bachelorseminar als auch für das Masterseminar geeignet, wobei im Rahmen des Masterseminars eine ausführlichere Bearbeitung des Themas erwartet wird.

Sprache

Die Rezensionen, der Vortrag und die Ausarbeitung können sowohl auf Deutsch als auch auf Englisch angefertigt bzw. abgehalten werden.

Abgaben

Sämtliche Abgaben sind bei Julian Brunner einzureichen.

Vorbesprechung

Die Vorbesprechung dient dazu, einen ersten Eindruck über die potentiellen Teilnehmer und deren Interessen zu erhalten, sowie Informationen zu Ablauf und Themen zu vermitteln und Fragen zu beantworten. Anwesenheit bei der Vorbesprechung ist nicht Voraussetzung für die Teilnahme am Seminar, wird jedoch bei der späteren Platzvergabe eine Rolle spielen. Wir bitten auch um Interessensbekundung per E-Mail, falls die Teilnahme an der Vorbesprechung nicht möglich sein sollte.

Platzvergabe

Die Platzvergabe erfolgt durch das Matchingsystem.

Themenvergabe

Die Themenvergabe erfolgt auf Basis von durch die Teilnehmer angegebenen Präferenzen.

Zuordnung der Rezensionsthemen

Unabhängig von der Themenvergabe werden jedem Teilnehmer zwei Rezensionsthemen zugeordnet. Diese Zuordnung wird nur den Rezensoren per E-Mail mitgeteilt, sodass diese die Möglichkeit haben, anonym zu bleiben.

Entwurf

Jeder Teilnehmer reicht 4 Wochen vor dem Vortrag einen Entwurf seiner Ausarbeitung ein. Ein Entwurf ist eine ausformulierte und inhaltlich vollständige Version der Ausarbeitung, auf deren Basis die Rezensionen angefertigt werden.

Rezensionen

Die Rezensoren erhalten die Entwürfe, sobald sie von den jeweiligen Autoren eingereicht werden und haben 2 Wochen für das Anfertigen der Rezension. Eine Rezension sollte etwa 1 Seite umfassen. Diese Rezensionen werden anschließend den Autoren zugänglich gemacht. Die Autoren haben dann noch 2 Wochen, die Kritik einzuarbeiten, bevor der Vortrag gehalten und die endgültige Version der Ausarbeitung eingereicht wird.

Die Rezensionen sollten sich hauptsächlich auf den Inhalt konzentrieren, wobei nicht erwartet wird, dass vom Rezensor weitere Recherche an den Quellen betrieben wird. Wichtig sind z.B. gute Strukturierung des Themas, schlüssige Argumentation und leicht verständliche Darstellung von Sachverhalten, die der Leser auch dann nachvollziehen kann, wenn er oder sie die Quelle dazu nicht gelesen hat. Rechtschreibung und Grammatik sind weniger wichtig, es macht aber natürlich Sinn, auch solche Fehler in der Rezension zu erwähnen. Eine Zusammenfassung des Themas ist nicht nötig. Die äußere Form der Rezensionen ist den Teilnehmern überlassen. Sowohl Stichpunkte als auch Fließtext sind in Ordnung.

Vorversion der Präsentationsfolien

Eine Vorversion der Präsentationsfolien wird 2 Wochen vor dem Vortrag eingereicht.

Vortrag

Die Länge eines Vortrags sollte ca. 45 Minuten betragen. Die Vorträge werden in Sitzungen zu je 2-3 Vorträgen abgehalten.

Ausarbeitung

Die endgültige Version der Ausarbeitung wird am Tag des Vortrags eingereicht. Der Umfang sollte sich auf ca. 10 Seiten belaufen. Die äußere Form der Ausarbeitung ist im Rahmen des Üblichen den Teilnehmern überlassen. Es gibt keine Vorlage.

Präsentationsfolien

Die Endfassung der Präsentationsfolien wird am Tag des Vortrags im PDF Format eingereicht.

Notenzusammensetzung

Die Note setzt sich wie folgt zusammen: 20% Rezensionen + 40% Vortrag + 40% Ausarbeitung

Tipps

Bei der Recherchearbeit können Dienste wie Google Scholar dabei helfen, wissenschaftliche Veröffentlichungen zu finden. Anschließend kann mit Hilfe von eAccess darauf zugegriffen werden. Dieser Schritt ist meist notwendig, da die Verlage oft hohe Kosten für den Download dieser Veröffentlichungen veranschlagen.

Themenzuordnung

TeilnehmerIDTitel
Elias Marquart6Hindley-Milner Type Inference
Jennifer Tipecska7Type Classes in Haskell
Lukas Fürmetz8Monads in Haskell
Michael Andonie1The Rust Programming Language
Julian Biendarra2The Clean Programming Language
Jannik Theiß3The Idris Programming Language
Marcel Lotze4The Agda Programming Language
Pascal Möller9Theorems for Free
Daniel Stüwe10GADTs, Existential Types, Type-Level Programming
Simon Roßkopf11Zippers and Data Type Derivatives
Hauke Brinkop12Purely Functional Data Structures 1
Michael Schreier13Purely Functional Data Structures 2
Julia Martini14Exact Real Numbers in Haskell
Florian Dreier15Type-Safe Modular Hash-Consing
Andreas Bergmaier16Finger Trees
Albert Steckermeier17Lenses in Functional Programming

Termine

Vorbesprechung

Datum: 28.01.2015
Uhrzeit: 16:00 - 17:00
Ort: MI 00.09.038 (Turing)

Platzvergabe

Datum: 16.02.2015

Themenvergabe

Datum: 23.02.2015

Abgabefristen für die Entwürfe

Datum: 22.04.2015 (Themen 6, 7, 8)
Datum: 29.04.2015 (Themen 1, 2)
Datum: 06.05.2015 (Themen 3, 4)
Datum: 13.05.2015 (Themen 9, 10)
Datum: 20.05.2015 (Themen 11, 12, 13)
Datum: 27.05.2015 (Themen 14, 15)
Datum: 03.06.2015 (Themen 16, 17)

Abgabefristen für die Rezensionen und Vorversionen der Präsentationsfolien

Datum: 06.05.2015 (Themen 6, 7, 8)
Datum: 13.05.2015 (Themen 1, 2)
Datum: 20.05.2015 (Themen 3, 4)
Datum: 27.05.2015 (Themen 9, 10)
Datum: 03.06.2015 (Themen 11, 12, 13)
Datum: 10.06.2015 (Themen 14, 15)
Datum: 17.06.2015 (Themen 16, 17)

Vorträge und Abgabefristen für die Ausarbeitungen und Präsentationsfolien

Datum: 20.05.2015 (Themen 6, 7, 8)
Datum: 27.05.2015 (Themen 1, 2)
Datum: 03.06.2015 (Themen 3, 4)
Datum: 10.06.2015 (Themen 9, 10)
Datum: 17.06.2015 (Themen 11, 12, 13)
Datum: 24.06.2015 (Themen 14, 15)
Datum: 01.07.2015 (Themen 16, 17)
Uhrzeit: 14:00 - 16:00/17:00
Ort: MI 00.09.038 (Turing)

Themen

1. The Rust Programming Language

Description: Rust is a systems programming language with a lot of functional elements, developed at Mozilla. Rust is a systems programming language that runs blazingly fast, prevents almost all crashes, and eliminates data races.
References: [1] The Rust Programming Language, [2] The Rust Guide
Type: Bachelor Seminar
Advisor: Johannes Hölzl

2. The Clean Programming Language

Description: The goal of this bachelor-topic is to give an introduction on the clean programming language, with a focus on its uniqueness typing feature. To make this a master topic, also a theoretical introduction to uniqueness and/or linear types is expected.
References: [1] Clean, [2] Uniqueness Typing Simplified [PDF]
Prerequisites: Knowledge of Haskell or another (lazy) functional language.
Type: Bachelor Seminar or Master Seminar
Advisor: Peter Lammich

3. The Idris Programming Language

Description: Idris is a general purpose pure functional programming language with dependent types. Dependent types allow types to be predicated on values, meaning that some aspects of a program’s behaviour can be specified precisely in the type. It is compiled, with eager evaluation.
References: [1] Idris, [2] Programming in Idris: A Tutorial [PDF]
Type: Master Seminar
Advisor: Johannes Hölzl

4. The Agda Programming Language

Description: Agda is a programming language based on type theory. It can also be used as a proof assistant by exploiting the Curry-Howard isomorphism. Roughly speaking, it states that propositions are equivalent to types, whereas values of these types correspond to proofs of the proposition. The language itself offers a variety of interesting features, most notably dependent types. The type of a value can depend on another value, for example, Vec a n where n is a natural number is the type of all vectors of length n with values of type a. It also has an interesting module system.
References: [1] Dependently Typed Programming in Agda [PDF]
Type: Master Seminar
Advisor: Lars Hupel

5. Combinatory Logic

References: [1] Combinatory Logic
Type: Bachelor Seminar
Advisor: Tobias Nipkow

6. Hindley-Milner Type Inference

References: [1] Hindley–Milner type system
Type: Bachelor Seminar
Advisor: Tobias Nipkow

7. Type Classes in Haskell

References: [1] Type Classes in Haskell
Type: Bachelor Seminar
Advisor: Tobias Nipkow

8. Monads in Haskell

Description: Monads are an important concept in purely functional programming languages like Haskell. In this seminar, we present the basic theory behind them as well as their definition using type classes and the associated do-notation. We also show some of their primary applications including list comprehensions, stateful computation, Input/Output, and error handling. A good overview of the topic is given in [1], with [2, chapters 12 and 13] and [3, chapter 14] providing a more gentle introduction. The topic can also be treated as a Master seminar by covering more advanced concepts related to monads.
References: [1] Monad (functional programming), [2] Learn You a Haskell for Great Good!, [3] Real World Haskell
Prerequisites: Basic knowledge of the Haskell programming language.
Type: Bachelor Seminar or Master Seminar
Advisor: Julian Brunner

9. Theorems for Free

Description: Wadler's influential paper about an application of the concept of parametricity explains how the types of functions give rise to theorems. For example, from the type signature id :: a -> a, we can, without looking at the corresponding implementation, deduce that id is in fact the ientity function (id x = x). There is a rich theory behind this. A good starting point is the eponymous paper by Wadler [1]. Some more resources can be found on Wadler's web site [2].
References: [1] Theorems for Free! [DVI], [2] Parametricity
Type: Master Seminar
Advisor: Lars Hupel

10. GADTs, Existential Types, Type-Level Programming

Description: Haskell provides a number of extensions that increase the capabilities of its type system. This topic focuses on Generalised Algebraic Data Types (GADTs), Existential Types, and type-level Programming (e.g. HLists, type-level naturals, etc). Due to the enormous complexity of the material, the student may choose a suitable subset of these subjects to present.
References: GADTs: [1] Silly Type Families [PDF], [2] Simple Unification-based Type Inference for GADTs [PDF], Existential Types: [3] Types and Programming Languages, Benjamin C. Pierce (Chapter 24)
Type: Master Seminar
Advisor: Manuel Eberl

11. Zippers and Data Type Derivatives

Description: Zippers facilitate moving through a data structure (such as a list or a tree). With a zipper, it is e.g. possible to denote a certain position in a tree while modifying its values. There is an interesting correspondence between between zippers of algebraic data types and formal derivatives, which is to be illustrated informally in the talk.
References: Zippers: [1] Functional Pearls: The Zipper [PDF], Derivatives: [2] The Derivative of a Regular Type is its Type of One-Hole Contexts [PDF]
Type: Bachelor Seminar
Advisor: Manuel Eberl

12. Purely Functional Data Structures 1

Description: The student introduces and explains the technique of implicit recursive slowdown, demonstrates the technique using a concrete data structure (e.g., double-ended queues) and discusses the complexity and difference between functional and procedural implementation. A different topic from the book is also possible after a consultation with the advisor.
References: [1] Chris Okasaki: Purely Functional Data Structures [read online (may require eAccess)]
Type: Bachelor Seminar
Advisor: Ondřej Kunčar

13. Purely Functional Data Structures 2

Description: The student introduces the technique of amortization and shows how to eliminate it (Chapter 5 in [1]). Demonstration on concrete data structures is expected.
References: [1] Chris Okasaki: Purely Functional Data Structures [read online (may require eAccess)]
Type: Bachelor Seminar
Advisor: Ondřej Kunčar

14. Exact Real Numbers in Haskell

Description: Infinite data structures (like Haskell's lazy lists) can be used to represent real numbers, e.g., think of a stream of digits. Operations defined on these data structures allow to obtain increasingly precise results by evaluating the data structure successively. An illustrative (and fun) example is given by "The Most Unreliable Technique in the World to compute pi" [1]. Further, more serious approaches can be found at [2, 3].
References: [1] The Most Unreliable Technique in the World to compute pi [PS], [2] Exact real arithmetic, [3] Applications and libraries/Mathematics/Real and rational numbers
Type: Bachelor Seminar
Advisor: Fabian Immler

15. Type-Safe Modular Hash-Consing

Description: Hash-consing is a technique to share purely functional data that are structurally equal. Beyond the obvious advantage of saving memory blocks, hash-consing may also be used to speed up fundamental operations and data structures by several orders of magnitude when sharing is maximal. Hash-consing is part of the programming folklore but, in most programming languages, it is more a design pattern than a library. In this seminar, we analyse a particular OCaml hash-consing library [1] that encapsulates hash-consed terms in an abstract datatype, thus safely ensuring maximal sharing.
References: [1] Type-Safe Modular Hash-Consing [PDF]
Type: Bachelor Seminar
Advisor: Dmitriy Traytel

16. Finger Trees

Description: The goal of this master topic is to describe the general purpose data structure of finger trees, its properties, and applications.
References: [1] Finger Trees: A Simple General-Purpose Data Structure
Prerequisites: (Basic) Knowledge of functional programming language, knowledge of at least one search-tree data structure (e.g., AVL-tree, RB-tree, 2,3-tree, ...)
Type: Master Seminar
Advisor: Peter Lammich

17. Lenses in Functional Programming

Description: Lenses, or "functional references", or "first-class labels" are a common concept in functional programming. They are used to deal with immutable data structures. In the simplest definition, a lens is a pair of a setter and a getter function. A getter function retrieves the value of a field in a record, whereas a setter function changes the value of a field, returning the updated record. What's nice about lenses is that they compose: If you have a lens for X in Y, and a lens for Y in Z, you can obtain a lens for X in Z. There's a multitude of resources on the web about lenses [1]. I recommend going through this overview on Stack Overflow [2] first.
References: [1] FAQ - ekmett/lens Wiki, [2] lenses, fclabels, data-accessor - which library for structure access and mutation is better
Type: Bachelor Seminar or Master Seminar
Advisor: Lars Hupel