HaL-10: Programm

Man muss keine Monaden kennen, um Haskell zu programmieren, denn es ist nur eine Abstraktionsschicht, also ein Muster, mit dem man seine Programme strukturiert. Als solches aber ein sehr erfolgreiches, und mit der richtigen Monade werden komplizierte Programmieraufgaben plötzlich einfach, übersichtlich und weniger fehlerträchtig.

Eine oft übersehene Variante der Monade wird durch die MonadFix-Typklasse beschrieben: Monaden, in denen sich Fixpunkte berechnen kann. Damit kann man, in gewisser Weise, Werte benutzen, die erst später berechnet werden.

In einer Live-Coding-Sitzung zeigt Joachim Breitner, wie er dank einer selbstgestrickten Monaden die Ausgabe eines Binär-Datenformates „schön“ implementiert, wie er dem mit MonadFix den letzten Schliff gibt, und warum das eigentlich überhaupt funktionieren kann.

In einem Real-World-Haskell Beitrag stelle ich eine Software zum Durchführen und Auswerten von A/B und MVT-Tests vor, welche ich 2014 im Rahmen meiner Bachelorarbeit gebaut habe. Es gibt einen Rundumschlag um Webservices, Statistik und freien Monaden zur Programmstrukturierung geben.

Konstruktive Mathematikerinnen und Mathematiker verzichten auf das Gesetz vom ausgeschlossenen Dritten, welches in etwa besagt, dass für jede Behauptung P entweder P oder die Negation von P wahr ist. Aus dem Verzicht auf dieses sonst grundlegende Axiom erwachsen einige Vorteile, wie dass man aus konstruktiven Beweisen von Existenzaussagen entsprechende Algorithmen extrahieren und man rigoros mit nichtstandard “Traumaxiomen”, die in klassischer Mathematik schlicht falsch sind, umgehen kann.

Um sich mit klassischen Mathematikerinnen und Mathematikern unterhalten zu können, können ihre konstruktiven Kolleginnen und Kollegen die Doppelnegationsübersetzung verwenden. Diese hat die fundamentale Eigenschaft, dass die Übersetzung einer Behauptung genau dann konstruktiv gilt, wenn die ursprüngliche Behauptung klassisch gilt.

Nun gibt es eine faszinierende Verbindung zwischen der
Doppelnegationsübersetzung und der in der Informatik wohlbekannten Continuation-Passing-Style-Transformation: In einem gewissen Sinn sind sie ein und dasselbe. Das ist ein wunderschöner Aspekt des “computational trinitarianism”.

Der Vortrag wird in diese Thematik einführen und anhand von Beispielcode in Haskell illustrieren. Scheinbar unmögliche Aufgaben wie das Minimum einer unendlichen Liste von natürlichen Zahlen zu finden werden damit – in einem gewissen monadischen Sinn – möglich. Der Vortrag setzt keine Vorkenntnisse in formaler Logik oder konstruktiver Mathematik voraus, wohl aber gewisse allgemeine Vertrautheit mit mathematischen Fragestellungen und mathematischer Sprache.

Typsicherheit erlaubt die Erstellung von effizientem Code mit wenigen Fehlern. Um diese Eigenschaft auszunutzen, ist es jedoch wichtig mit gut entwickelten Typen zu arbeiten. In diesem Paper beschreiben wir eine Bibliothek für numerischer Optimierung, mit Typen und Typklassen basierend auf dem mathematischen Begriff der Mannigfaltigkeit. Die grundlegende Typklasse in der Bibliothek ist Manifold, welche die Methode dimension definiert, entsprechend der Dimension des jeweiligen Typs. Der Haupttyp in der Bibliothek ist der sogenannte Point, der aus einer Instanz der Manifold und einem Vektor von Koordinaten besteht. Die Länge des Vektors muss der Dimension der Instanz entsprechen, und der Typ ist mit einem Phantomtyp ausgestattet, den wir einen Chart nennen, der auf das verwendete Koordinatensystem hinweist. Ein Punkt dient als ein Container für numerische Information, und die Karte erlaubt mehrere Implementationen von Typklassen für denselben Punkt, basierend auf verschiedenen Koordinatensystemen. Da eine Mannigfaltigkeit ein sehr allgemeines mathematisches Objekt ist, hat diese Bibliothek vielfältige Anwendungen. Man kann zum Beispiel Dualräume, Tangentialräume, hamiltonsche und lagrangesche Systeme, parametrische Funktionen, und Warscheinlichkeitsverteilungen aus der Klasse der Exponentialfamilie effektiv beschreiben, sodass praktische Typsicherheit mit numerischen Objekten ermöglicht wird.

Die Firma Metrix Financial Reporting Solutions entwickelt Software, welche BaFin-regulierten Unternehmen dabei hilft, nach Spezifikation des Supervisory Reportings der European Banking Authority (EBA) aufsichtsrechliche XBRL-Meldungen zu erstellen.

Moritz Drexl spricht darueber, wie Haskell dabei geholfen hat, in kurzer Zeit ein Produkt zu entwickeln, welches auf robuste Art und Weise mit den komplexen Spezifikationen der EBA umgehen kann. Weiterer Schwerpunkt des Vortrags sind die Herausforderungen, eine in Haskell geschriebene Desktop-Anwendung unter Windows anzubieten, und wie diese gelöst wurden.

Nach einer Einführung in XBRL-basierte Meldungen und Vorstellung der wichtigsten Features der Software wird erklaert, wie die Kombination von Haskell und PureScript es ermöglicht, komplexe Desktop-Anwendungen zu entwickeln. Danach wird vorgestellt, welche Rolle die wichtigsten Bibliotheken in der Entwicklung gespielt haben und ein Fazit über die Nutzung von Haskell gezogen.

Wer braucht schon Typklassen? Oder überhaupt ein statisches Typsystem? Warum müssen Nebenwirkungen immer so kompliziert sein? Und was sind eigentlich Monaden? Da muss es doch etwas besseres geben!

dg ist Python mit Haskell-Syntax. In einem kurzen Vortrag (15 Minuten) möchte ich mit einem Augenzwinkern das “bessere Haskell” vorstellen.

Elm ist eine funktionale Programmiersprache, die als JavaScript-Alternative positioniert wird. Sie übernimmt viele Sprachmerkmale aus der ML-Familie und aus Haskell, etwa: strenge, statische Typung und Typinferenz, algebraische Datentypen, Polymorphie, Records mit Subtyping, pur wie Haskell (mit per Typsystem kontrollierten Seiteneffekten), strikt auswertend wie ML. Einfache Haskell-Programme sind oft bis auf kleine syntaktische Differenzen (etwa Umbenennung von Schlüsselworten) auch Elm-Programme. Andererseits gibt es bewusste Abweichungen hinsichtlich Sprachmerkmalen (etwa bisher keine Typklassen) und Philosophie. Vorderstes erklärtes Zieleinsatzgebiet ist Web-Frontend-Programmierung. Entsprechend gut ist die Unterstützung für deklaratives HTML, Canvas etc. Der existierende Compiler übersetzt nach JavaScript.

Wenn es um “Typtricks” geht, dann läuft es häufig auf neuartige Typerweiterungen des GHC hinaus. Das muss nicht so sein, denn schon mit Haskell 98 kann man mit Typen viel mehr ausdrücken, als es auf den ersten Blick aussieht. Manchmal entpuppt sich eine scheinbar naheliegende Typerweiterung auch gar nicht als das richtige Werkzeug, man muss immer mehr Typeerweiterungen hinzunehmen und am Ende wird es sehr komplex und ist doch nicht so richtig befriedigend. In meinem Vortrag möchte ich ein paar Tricks vorstellen, die es verdienen, häufiger verwendet zu werden.

In diesem Tutorium werden Aspekte der Implementierung des E-Lern- und Prüfungs-Systems autotool behandelt. Das ist ein umfangreiches komplett in Haskell realisiertes Projekt. Es besteht aus einem zustandslosen Semantik-Service zur Erzeugung von Aufgaben-Instanzen und Bewertung von Lösungsversuchen sowie einer Web-Oberfläche und einer Datenbank-Anbindung. autotool wird seit ca. 15 Jahren benutzt und weiterentwickelt. Das Tutorium soll die Teilnehmer auf Refaktorisierungen und Erweiterungen des Quelltextes vorbereiten. Damit richtet es sich zunächst an Studierende der HTWK, ist aber für Gäste interessant, denn es werden typische Entwurfs- und Implementierungs-Fragen, -Entscheidungen (und auch -Fehler) in realen Haskell-Projekten verdeutlicht. Insbesondere zu offenen Fragen sind Hinweise und Erfahrungen aus anderen Projekten sehr willkommen.

Haskell eignet sich durch seine spezifischen Eigenschaften (statische und starke Typisierung, lazy evaluation, funktionale Konzepte, Monaden) hervorragend zur Arbeit an sprachwissenschaftlichen Problemen im Allgemeinen bzw. formalsemantischen Probleme im Speziellen. Der Vortrag soll diesen Umstand anhand der Modellierung von Skopusverhältnissen in natürlicher Sprache illustrieren. Dabei soll aufgezeigt werden, dass die zwischen beiden Disziplinen bestehende Nähe auf sehr ähnlichen formalen Grundlagen beruht (Lambda-Kalkül, Kategorientheorie) und dass diese gemeinsamen Grundlagen eine wertvolle, aber häufig nicht genutzte Ressource darstellen.

Haskell hat ein außergewöhnlich mächtiges Typsystem. Es hat eine komfortable Balance zwischen praktischer Anwendbarkeit und Ausdrücksstärke. Dennoch liegen einige Sachen noch außerhalb seiner Möglichkeiten, ein Beispiel davon sind voll value-dependent Typen. Liquid Haskell ist eine Erweiterung des Typsystems in diese Richtung, indem Ideen aus der Verification von imperativen Programmen und die Fähigkeiten von SMT Solvern integriert werden.

Mit dieser neuen Kraft kann LH Typen über Datenstrukturen entscheiden, welche sich mit denen von dependent Typsystemen vergleichen lassen. Darüber hinaus hält LH die Menge an zusätzlichen Annotationen minimal. Dieser Vortrag behandelt die Ideen hinter LH, wie es funktioniert und wie man es anwendet, um Korrektheit in real-world Situationen zu beweisen.

Zielgruppe: Der Vortrag setzt nur grundlegende Kenntnisse mit Haskell-98 Typen voraus. Erfahrungen mit Typinferenz und Typchecking sind ebenfalls hilfreich.