Mehr Typsicherheit durch GADTs

Statische Typsysteme haben zahlreiche Vorteile. Der naheliegendste Vorteil ist vermutlich, dass mögliche Laufzeitfehler verhindert werden.

Stellen wir uns zum Beispiel vor, wir wollten SQL-Anfragen modellieren. Wählen wir einen String als Repräsentation, so können wir ohne weiteres syntaktisch inkorrekte Anfragen basteln, und haben keinen hohen Grad an Sicherheit. Wählen wir statt dessen einen spezifischen Datentyp SQL, der einen abstrakten Syntaxbaum modelliert, so können wir uns auf syntaktische Korrektheit verlassen, aber wir können noch immer andere Fehler machen. Was, wenn wir sicherstellen wollten, dass die verwendeten Namen von Tabellen und Feldern tatsächlich in unserer Datenbank enthalten sind? Was, wenn wir garantieren wollen, dass wir SQL-Operatoren in typkorrekter Art und Weise verwenden wollen? Es ist einfach, sich vorzustellen, dass wir dies durch Tests zur Laufzeit sicherstellen können. Aber ist es auch möglich, dies bereits durch statische Typen zu garantieren?

Ein einfacheres Beispiel: Wir haben eine Applikation, die Fragebögen und zugehörige Antworten verwaltet. Es gibt verschiedene Sorten von Fragen. Manche Fragen sollten mit „Ja“ oder „Nein“ beantwortet werden, andere mit einer Antwort aus einer vorgegebenen Auswahl, wieder andere mit einer quantitativen Angabe. Sicher können wir Datentypen definieren, die die verschiedenen Sorten von Fragen und die verschiedenen Sorten von Antworten modellieren. Aber wenn wir nun Fragen und zugehörige Antworten haben, wie wissen wir dann, dass die Sorten der Fragen und die Sorten der Antworten zueinander passen? Wiederum ist es einfach, dies zur dynamisch zu testen. Es ist nicht ganz so einfach – aber durchaus möglich – dies auch statisch im Typsystem sicherzustellen.

Das Sprachmittel, welches wir dazu verwenden werden, heißt „GADT“. Die Abkürzung steht für „Generalized Algebraic Data Type“, zu Deutsch „generalisierter algebraischer Datentyp“. GADTs stehen in Haskell bereits seit vielen Jahren als Spracherweiterung zur Verfügung (und werden vermutlich auch irgendwann in den Standard Einzug halten), und sind mittlerweile auch in einigen anderen Programmiersprachen verfügbar.

Im folgenden will ich das Beispiel mit den Fragebögen in Haskell etwas näher beleuchten. Zunächst werden wir mit normalen Sprachmitteln skizzieren, wie man eine solche Applikation in Haskell implementieren könnte. Dann werden wir sehen, an welcher Stelle die Verwendung von GADTs sinnvoll wird, und was GADTs genau sind.

Weiterlesen...

Noch mehr über Software Transactional Memory

Heute geht‘s nochmal um Software Transactional Memory (STM), eine schöne und saubere Möglichkeit, um in Programmen mit Nebenläufigkeit umzugehen. Hier im Blog gab‘s ja schon eine Einleitung zu STM sowie einen weiterführenden Artikel. Bisher haben wir gesehen, dass STM traditionellen Techniken zum Umgang mit Nebenläufigkeit (wie z.B. Locks) überlegen ist:

  • Atomare Blöcke werden einfach als solche deklariert werden und der Programmier muss Atomizität nicht explizit durch Locks sicherstellen.
  • Mit STM entwickelte Komponenten können einfach zu neuen Komponenten zusammengebaut werden, was mit Locks oftmals die Überarbeitung des Locking-Modells nach sich zieht.

Heute soll es nun abschließend um ein mögliches Ausführungsmodell für STM gehen. Das vorgestellte Modell ist konzeptionell sehr einfach und vom Prinzip auch so im GHC Compiler für Haskell umgesetzt. Natürlich können anderen STM-Implementierungen auch anderes Ausführungsmodelle verwenden, vorausgesetzt die Atomizitätsgarantien werden nicht verletzt.

Weiterlesen...

DSLs ohne Nahtstelle mit Kontrollabstraktion

In einem vorherigen Posting haben wir uns mit einer Monade für Wahrscheinlichkeitsverteilungen beschäftigt. Diese erlaubt uns, ein probabilistisches Szenarium als Programm aufzuschreiben, deren Ausführungen die Wahrscheinlichkeitsverteilung möglicher Resultate des Szenarios liefert. Allerdings ist die explizite monadische Programmierung etwas umständlich. Eigentlich hatten wir uns gewünscht, die Szenarien als „normales“ Racket-Programm unter Verwendung der gewohnten Operatoren wie and, if und let zu schreiben. Stattdessen mussten wir bisher monadische Versionen con, if_ und let_ benutzen. In diesem Post zeigen wir, wie wir genau das erreichen, und zwar unter Verwendung einer geradezu bewusstseinserweiternden Technik namens Kontrollabstraktion, die es in der Mächtigkeit nur in funktionalen Sprachen gibt. Dieses Posting ist technisch etwas anspruchsvoll.

Weiterlesen...

Mehr über Software Transactional Memory

Vor kurzem war Nebenläufigkeit mit Software Transactional Memory das Thema hier im Blog. Da Nebenläufigkeit auch in modernen Softwaresystemen immer noch häufig ein schwieriges Problem und eine Quelle vieler Fehler ist, schauen wir uns heute Software Transactional Memory (kurz: STM) nochmal genauer an. Funktionale Sprache wie z.B. Haskell, Scala oder clojure bieten gute Unterstützung für STM, denn der deklarative Programmierstil und der weitgehende Verzicht auf Seiteneffekte passen gut zum STM-Paradigma.

Wir haben in dem ersten Artikel gesehen, dass STM eine Alternative zu Locks darstellt, die einfacher zu benutzen ist und bei der Probleme wie Deadlocks oder Race Conditions typischerweise nicht oder nur sehr selten auftreten. Meine tägliche Erfahrung mit STM in unserem Softwareprodukt CheckpadMED bestätigt mich immer wieder darin, dass Nebenläufigkeit mit STM eigentlich (relativ) einfach ist: man muss lediglich spezifizieren, welche Codeblöcke atomar laufen sollen, und das Laufzeitsystem stellt dann diese Atomizitätseigentschaft sicher.

Im heutigen Artikel untersuchen wir STM etwas genauer. Wir gehen dabei der Behauptung nach, die wir im ersten Artikel aufgestellt haben, nämlich dass auch Gründe der Softwarearchitektur für STM sprechen: während zwei mit Locks implementierte Programmkomponenten oftmals nicht ohne Änderung des Locking-Protokolls zu einer neuen Komponenten zusammengebaut werden können, klappt ein solcher Zusammenbau mit STM meist problemlos, ohne dass man sich über Implementierungsdetails der Komponenten Gedanken machen muss.

Weiterlesen...

Eine Monade für Wahrscheinlichkeitsverteilungen

Uns erreichte neulich die Frage „Wozu sind Monaden eigentlich in dynamisch getypten Sprachen“ gut? In Haskell zum Beispiel sind ja Monaden fast allgegenwärtig und haben dort insbesondere die Aufgabe, anhand der Typen deutlich zu machen, mit welchen Effekte ein Entwickler bei der Auswertung eines Ausdrucks rechnen muss. Da Typen in dynamisch getypten Sprachen im Programmtext nicht direkt sichtbar sind, ist die Frage legitim, da viele Monaden nur jeweils einen Wert als Resultat einer Berechnung mit Seiteneffekten produzieren. Es gibt allerdings auch Monaden, die mehr leisten - wie zum Beispiel die Monade der Wahrscheinlichkeitsverteilungen. Um die geht es in diesem Beitrag - und zwar in einer dynamisch getypten Sprache, nämlich in Racket. Racket bietet für diese Anwendung relevante Abstraktionsmöglichkeiten, die noch über die Fähigkeiten von Haskell hinausgehen. Es wird nur rudimentäres Racket vorausgesetzt, wie zum Beispiel in unserem früheren Posting erläutert.

Weiterlesen...