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. Arrow s 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.
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)
|
