| Titel | Fortgeschrittene Konzepte der funktionalen Programmierung |
| Semester | Sommersemester 2015 |
| Module | Bachelorseminar (IN0014), Masterseminar (IN2107) |
| Voraussetzungen | Grundlegende Kenntnisse in funktionaler Programmierung (z.B. Einführung in die Informatik 2 (IN0003)) |
| SWS | 2 |
| ECTS | 4 |
| Organisation | Julian Brunner, Lars Hupel, Tobias Nipkow |
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.
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.
Die Rezensionen, der Vortrag und die Ausarbeitung können sowohl auf Deutsch als auch auf Englisch angefertigt bzw. abgehalten werden.
Sämtliche Abgaben sind bei Julian Brunner einzureichen.
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.
Die Platzvergabe erfolgt durch das Matchingsystem.
Die Themenvergabe erfolgt auf Basis von durch die Teilnehmer angegebenen Präferenzen.
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.
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.
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.
Eine Vorversion der Präsentationsfolien wird 2 Wochen vor dem Vortrag eingereicht.
Die Länge eines Vortrags sollte ca. 45 Minuten betragen. Die Vorträge werden in Sitzungen zu je 2-3 Vorträgen abgehalten.
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.
Die Endfassung der Präsentationsfolien wird am Tag des Vortrags im PDF Format eingereicht.
Die Note setzt sich wie folgt zusammen: 20% Rezensionen + 40% Vortrag + 40% Ausarbeitung
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.
| Teilnehmer | ID | Titel |
|---|---|---|
| Elias Marquart | 6 | Hindley-Milner Type Inference |
| Jennifer Tipecska | 7 | Type Classes in Haskell |
| Lukas Fürmetz | 8 | Monads in Haskell |
| Michael Andonie | 1 | The Rust Programming Language |
| Julian Biendarra | 2 | The Clean Programming Language |
| Jannik Theiß | 3 | The Idris Programming Language |
| Marcel Lotze | 4 | The Agda Programming Language |
| Pascal Möller | 9 | Theorems for Free |
| Daniel Stüwe | 10 | GADTs, Existential Types, Type-Level Programming |
| Simon Roßkopf | 11 | Zippers and Data Type Derivatives |
| Hauke Brinkop | 12 | Purely Functional Data Structures 1 |
| Michael Schreier | 13 | Purely Functional Data Structures 2 |
| Julia Martini | 14 | Exact Real Numbers in Haskell |
| Florian Dreier | 15 | Type-Safe Modular Hash-Consing |
| Andreas Bergmaier | 16 | Finger Trees |
| Albert Steckermeier | 17 | Lenses in Functional Programming |
Datum: 28.01.2015
Uhrzeit: 16:00 - 17:00
Ort: MI 00.09.038 (Turing)
Datum: 16.02.2015
Datum: 23.02.2015
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)
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)
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)
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
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
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
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
References: [1] Combinatory Logic
Type: Bachelor Seminar
Advisor: Tobias Nipkow
References: [1] Hindley–Milner type system
Type: Bachelor Seminar
Advisor: Tobias Nipkow
References: [1] Type Classes in Haskell
Type: Bachelor Seminar
Advisor: Tobias Nipkow
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
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
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
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
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
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
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
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
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
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