Vorlesung: Praxis der Funktionalen Programmierung | Index

Theorems for Free

Wir hatten schon den Bezug zur Kategorientheorie gesehen: ein Typkonstruktor ist ein Funktor (ein Endo-Funktor von der Kategorie der Datentypen in sich).

Eine polymorphe Funktion f :: c a -> d a (wobei c und d Typkonstruktoren sind) ist eine natürliche Transformation vom Funktor c zum Funktor d. Beispiel: flatten :: Tree a -> [a] Dann gilt

f . fmap g = fmap g . f
Auf die Typen aufpassen: es sind zwei verschiedene fmaps. Beispiel: flatten . tmap (+1) = map (+1) . flatten

Das läuft unter dem Slogan Theorems for Free (für umsonst), denn die Aussage gilt, sobald f wirklich den polymorphen Typ hat, und das kann ja der Compiler für uns feststellen. Wir selbst stecken also keinerlei Arbeit rein.


best viewed with any browser


http://www.informatik.uni-leipzig.de/~joe/ mailto:joe@informatik.uni-leipzig.de