HaL5 - Haskell in Leipzig, zum Fünften

Tutorien, Workshop, Party

Das traditionsreiche HaL-Treffen bietet eine gute Mischung von Haskell-bezogenen Themen aus Forschung, Anwendung und Lehre mit vielen Möglichkeiten zu Diskussion und Unterhaltung bei der anschließenden Party. Der Workshop wird ergänzt durch Hands-On und Tutorien für Haskell-Ein- und Umsteiger. Diesmal findet das Treffen im Leipziger Mediencampus statt.

Datum: Freitag, den 4. Juni 2010

Ort und Anfahrt: Leipzig, mediencampus-villa-ida.de/anfahrt

Ablauf:

(T) vormittags parallel Tutorien und Lambda-Camp ( Open-Space-Meeting / Barcamp)
(W) nachmittags Workshop (Fachvorträge) inkl. Hands-On
(P) abends Grillparty mit Musik (analoge und digitale Klangsynthese)

Während der gesamten Zeit gibt es Gelegenheit (Strom, WLAN, Kaffee) zum spontanen Diskutieren und Hacken.

Anmeldung

Wir bitten um eine Vorabanmeldung unter nfa.imn.htwk-leipzig.de/hal5. Bei der Anmeldung bitte gewünschte Tutorien angeben. Genauere Planung der Tutorien erfolgt nach Auszählung.

Kosten (Tageskasse)

Preise bei Vorabanmeldung bis zum 31. Mai 2010
Student : T 5 EUR , W 5 EUR, P 10 EUR,
berufstätig: T 10 EUR , W 10 EUR, P 10 EUR.

Anmeldungen sind auch am 4. Juni 2010 vor Ort möglich. Aufgrund des erhöhten Organisationsaufwandes müssen wir in diesen Fall einen Zusatzbeitrag in Höhe von einmalig 5 EUR erheben.

Programm

Erstmals haben wir bei HaL4 Tutorien angeboten, um Interessierten einen Einblick in die für viele Programmierer ungewohnte funktionale Programmierung zu geben. Da die Tutorien besser angenommen wurden, als wir erwarteten, soll es sie auch diesmal wieder geben und wir räumen ihnen noch mehr Zeit ein! Außerdem wollen wir dem gepflegten Fachsimpeln mit dem erstmalig abgehaltenen Lambda-Camp eine eigene Plattform bieten.

Vorbereitung Tutorium

09:00 Anmeldung (für Installation/Tutorium)
09:30 Installation / VirtualBox Image

Tutorium parallel Lambda-Camp

10:00 Tutorium 1: Tutorial: Die Leksah IDE benutzen, Jürgen Nicklisch-Franken (75min)
Die IDE kennenlernen, Cabal Pakete und Workspaces, der Modulbrowser, Compiler, Interpreter und Debugger, Leksah anpassen
11:15 Kaffee-Pause
11:30 Tutorium 2: Parsec oder Fkt. Höh. Ord oder HXT/Arrows (75min)

Map/Fold:
Oft trennt man Daten (Objekte) und Funktionen (Methoden). Im funktionalen Programmieren werden jedoch Funktionen als Daten behandelt. Damit können Funktionen auch Resultate und Argumente anderer Funktionen sein. Typische Beispiele sind map und fold (reduce). Solche Funktionen höherer Ordnung sind flexibel (wieder-) verwendbare Softwarekomponenten. In funktionalen Sprachen kann man damit ganz natürlich umgehen - während in rein objektorientierten Sprachen eine barocke Umschreibung durch sog. Entwurfsmuster erforderlich ist. Im Tutorium benutzen und programmieren wir Funktionen höherer Ordnung auf Listen und Bäumen.
Parsec/Monaden:
Parsec ist eine in Haskell eingebettete domainspezifische Sprache für die Beschreibung von Parsern. Sie besteht aus elementaren Parsern (zum Lesen von Zeichen) und Parser-Kombinatoren (für Verzweigung, Nacheinanderausführung und Wiederholung). Die Nacheinanderausführung ist eine Monaden-Operation. Im Tutorium schreiben wir einfache, aber realistische Parser und lernen dadurch das Rechnen mit Monaden.
HXT/Arrows, Uwe Schmidt:
HXT ist eine in Haskell eingebettete domainenspezifische Sprache (DSL) zur Verarbeitung von XML-Dokumenten. Diese Sprache ist mit Hilfe von Arrows formuliert.Arrows sind Verallgemeinerungen von Funktionen. Ähnlich wie bei Monaden können mit Arrows Berechnungen mit Seiteneffekten in einer Form formuliert werden, so dass die zusätzlichen Effekte gekapselt und vor der Anwendung versteckt werden.

Im Tutorium werden das Sprachmodell und die wichtigsten elementaren Operationen und Kombinatoren der XML-DSL vorgestellt. Mit diesen Bausteinen werden kleine aber realistische und nützliche Funktionen entwickelt, zum Beispiel zur XPath-ähnlichen Selektion von Dokumententeilen und zur Generierung und Transformation von XML-Dokumenten.

Voraussetzung: Grundkenntnisse über Funktionen und die Kombination von Funktionen, Typklassen und Monaden.
10:00 bis Workshop: Lambda-Camp
Beim LambdaCamp organisieren sich spontan Teilnehmer in kleinen Gruppen, um Themen zu bearbeiten, die sie interessieren. Angefangen von Installationsproblemen und Einsteigersorgen über Softwarearchitekturfragen und Tipps und Tricks im Umgang mit bestimmten Paketen bis zu tiefliegenden theoretischen und philosophischen Problemen oder dem Start neuer Projekte - beim LambdaCamp entscheiden allein die Teilnehmer, worum es geht!

Pause

13:00 Mittagspause für eigene Versorgung (Liste mit Restaurants in der Nähe liegt aus)

Workshop + Hands-On

15:00 Vortrag 1: Das Haskell Web-Framework Hawk, Björn Peemöller
Das Web-Famework Hawk ist von der Architektur und Funktionalität vergleichbar mit Ruby on Rails. Es folgt ebenfalls dem MVC-Muster. Hawk enthält einen einfachen OR-Mapper und ein auf validem XHTML basierendes Template-System. Das Template-System ist typsicher. Die Typen der von der Anwendung einzufügenden Werte werden statisch gegen die Templates überprüft. Hawk ist vollständig in Haskell implementiert. Neuere Sprachenwicklungen, wie Typ-Familien und Template-Haskell werden in der Implementierung von Hawk genutzt.
15:45 Vortrag 2: Dependent Types mit Agda, Wolfgang Jeltsch
Mit abhängigen Typen (dependent types) können nicht nur Typen, sondern auch Werte als Parameter von Typen fungieren. Dadurch kann man z.B. die Längen von Listen in deren Typen angeben. Damit wird es möglich, fehlerhafte Indizierungen zur Compilierzeit statt zur Laufzeit zu erkennen.

Die Möglichkeiten reichen aber noch viel weiter. Eine Programmiersprache mit abhängigen Typen ist nämlich automatisch eine Beweissprache für eine Prädikatenlogik. Daher kann man nahezu beliebige Spezifikationen als Typen darstellen und deren Einhaltung vom Typprüfer sicher stellen lassen.

16:30 Kaffee-Pause

Folgende Hands-On finden parallel statt:

17:00 Hands-On: Agda
Eine Einführung in Dependent Types mit Agda. Große Teile davon als Live-Programming zu folgenden Themen:
• Grundlagen zu Dependent Types
• Grundlagen zu induktiven Familien (GADTs)
• die Grundidee des Curry-Howard-Isomorphismus
• ein kleiner Beweis in Agda

Folgende Beispiele werden gezeigt:
• statische Bereichsprüfung für Listenindizes
• take mit Bereichsprüfung für die Resultatlänge
17:00 Hands-On: Hawk
Demo von Alexander Treptow und Björn Peemöller

Es wird ein Prototyp einer personalisierten Hayoo!-Suche mit Hilfe von Hawk vorgestellt. Außerdem wird beispielhaft gezeigt, wie eine einfache Hawk-Applikation erstellt werden kann.
18:00 Präsentation der Ergebnisse vom Lambda-Camp

Abendprogramm

18:30 Grillparty mit Musik (analoge und digitale Klangsynthese) Zur Grillparty gibt es die Unsafe Performance, eine Geräuschkulisse aufgebaut von:
• Daniel van den Eijkel mit Hilfe einer Haskell-SuperCollider-EDSL,
• Alfons Geser an einem Formant-Analog-Synthesizer,
• Henning Thielemann unter Verwendung einer Haskell-LLVM-EDSL und einem Haskell-MIDI-Stream-Editor,

Eventuell weitere spontan einspringenden Mitwirkenden sind herzlich eingeladen.

Veranstalter:

Programmkommittee:

Alf Richter (iba CG Leipzig), Uwe Schmidt (FH Wedel), Henning Thielemann (Univ. Halle), Janis Voigtländer (Univ. Bonn), Johannes Waldmann (HTWK Leipzig)