Tools4ever Tech Blog

Monades

Ralph Langendam - Sr. Software Engineer | 14 maart 2017

Introductie

Monade - introductieBeschouw de volgende pure functie:

Het spreekt voor zich dat het resultaat van deze functie voor value = 0.0 onzin oplevert. Het liefst zouden we dan ook willen verbieden dat evaluatie plaatsvindt voor de waarde 0. Hiertoe zijn diverse gebruikelijke opties:

  • Definieer een nieuw input type voor value dat per definitie nooit 0 kan zijn.
  • Gooi een exceptie indien de input waarde 0 is.
  • Verwerk de foutstatus in de output waarden. Bijvoorbeeld,
    • Pas de signatuur van de functie aan naar
      bool reciprocal(double const& inValue, double& outValue)
      en gebruik de return waarde om over foutstatus te communiceren.
    • Retourneer een double* uit de functie en gebruik de waarde nullptr om over foutstatus te communiceren.

Op ieder van deze opties bestaan vele variaties en iedere optie kent voor en nadelen. Met het template type std::optional<T>, uit C++17, is er een nieuwe variatie op de derde optie beschikbaar gekomen. Voor oudere compilers is er een optional implementatie beschikbaar in Boost.

Op basis van de geretourneerde waarde kunnen nu beslissingen worden genomen:

Compositie

Monades - compositieMet de introductie van nieuwe technieken in bestaande code verdient de ontwikkeling van leesbare interfaces en gebruiksvriendelijke adapters onze aandacht. We schrijven code immers in eerste plaats voor mensen, pas in tweede instantie voor computers.
Ofschoon de geretourneerde std::optional<double> de validiteit van berekening in zich draagt is er in bestaande codebases waarschijnlijk geen enkele functie waarvoor een dergelijke instantie als input kan worden gebruikt. Onze adapter bestaat in zo'n geval uit het uitpakken van de waarde met if-statements, alvorens executie te kunnen vervolgen. Gelukkig kunnen we deze adapter refactoren.
Gegeven een willekeurige functie die aan een instantie van type A een instantie van type B toekent, dan is het eenvoudig om deze functie 'op te tillen' naar een functie die aan een std::optional<A> een std::optional<B> toekent:

Een legacy functie als de volgende kan nu eenvoudig interfacen met reciprocal.

Met wat template foo kan de interface syntactisch verder worden verbeterd voor vrije functies. Door de volgende FunctionTraits verder te specialiseren zijn in theorie alle Callables te ondersteunen.

De restrictie van de Lift functie op unaire functies (functies met één input argument) is slechts een schijnbare beperking. Immers, iedere functie met willekeurige ariteit kan worden gereduceerd tot een unaire functie door alle argumenten in een std::tuple te verpakken.

Binding

Monade - bindingNauw verwant aan de Lift functie, is de Bind functie. Deze stelt nieuwe functies als reciprocal in staat om ook met andere nieuwe functies te interfacen:

Deze compositie van reciprocal gevolgd door reflect en reciprocal zal uiteraard alleen nullopt retourneren indien de input waarde 0.0 of 1.0 is.

Met de adapters Bind, Lift en de constructor van std::optional kunnen we alle binaire foutafhandeling reduceren tot dergelijke composities. Zij lezen altijd als het happy path van executie en vertroebelen het beeld niet langer met de syntactische overhead van foutafhandeling. Idiomatisch is hiermee volledig van binaire foutafhandeling weg geabstraheerd.

Coherentie

Monades - coherentie

In het licht van voorgaande merken we een drietal trivialiteiten op.

  1. Voor alle functies f : A -> std::optional<B> en a van type A, geldt dat f(a) gelijk is aan Bind(f)(std::optional<A>{a}).
  2. Voor alle waarden m van type std::optional<T> geldt dat m gelijk is aan Bind(std::optional<T>::optional)(m).
  3. Voor alle types A, B, C; waarden m van type std::optional<A> en functies f : A -> std::optional<B> en g : B -> std::optional<C> geldt dat Bind(g)(Bind(f)(m)) = Bind(h)(m), waarbij h : A -> std::optional<C> met h(a) := Bind(g)(f(a)).

Deze trivialiteiten worden ook wel coherentie-voorwaarden genoemd en beschrijven informeel gesproken 'coherent' gedrag op onze adapters. We zullen dit later meer concreet maken.

Abstractie

Monade - abstractieTot dusver hebben we alleen gekeken naar std::optional. De bovengenoemde technieken zijn echter veel breder toepasbaar dan we tot dusver hebben beschouwd. We hebben gezien hoe de wereld van precondities kan worden verborgen achter een façade. Dergelijke façades kunnen worden opgeworpen om van een pluraliteit aan concepten weg te abstraheren. Dit brengt ons op het begrip monade.
Zonder wiskundige achtergrond is het moeilijk om een rigoureuze definitie van het begrip monade te geven, maar een beperkte realisatie van dit concept, binnen een programmeertaal als C++, zal hopelijk voldoende verhelderen om de praktische toepasbaarheid te illustreren. We laten ons hierbij inspireren door de terminologie uit de functionele programmeertaal Haskell.
Voor onze begrippen zal een monade gegeven zijn door:

  • Een template type / type constructor:
    template <typename> class M;
  • Een constructor voor instanties van dit type, genaamd Return
    template <typename T>
    M<T> Return (T);
  • Een Bind functie voor de monadische transformatie van functies (Callables)
    template <typename A, typename B>
    std::function<M<B>(M<A>)> Bind(std::function<M<B>(A)>);

Daarnaast moet er voldaan zijn aan de volgende drie coherentie voorwaarden voordat deze data een monade vormt.

  • Linker identiteit: voor alle types A en B; alle instanties a van type A en alle functies f : A -> M<B> moet gelden dat Bind(f)(Return(a)) gelijk is aan f(a).
  • Rechter identiteit: voor alle types A en alle instanties m van type M<A> moet gelden dat Bind(Return)(m) gelijk is aan m.
  • Associativiteit: voor alle types A, B, C; m instanties van type M<A> en functies f : A -> M<B> en g : B -> M<C> moet gelden dat Bind(g)(Bind(f)(m)) gelijk is aan Bind(h)(m), waarbij h : A -> M<C> de functie is waarvoor geldt dat h(a) := Bind(g)(f(a)).

Het is niet moeilijk in te zien dat de voorgaande definitie reduceert tot wat reeds vanzelfsprekend was voor M = std::optional; Return = std::optional<T>::optional(T) en Bind zoals voorheen.

Monades

Monade - monadesHet platform onafhankelijk en generiek bepalen van traits voor alle Callables is weliswaar een leuke exercitie, maar niet het onderwerp van deze blog. Om de hoeveelheid afleiding te minimaliseren zullen we onze implementatie vanaf nu dan ook beperken tot std::function objecten.

Om het definiëren van monades te vereenvoudigen introduceren we het volgende object met bijbehorende hulpfuncties:

Maybe

Monade - maybeOm een monade te definiëren hoeven we slechts de gedeclareerde static methodes te implementeren. Ter illustratie zullen we dit doen voor std::optional. De bijbehorende implementatie staat in de literatuur beter bekend als de Maybe monade.

Input en Output

Monade - input outputIn Haskell zijn alle functies stateloos, ofwel ze hebben geen side-effecten. Iedere output waarde van een functie is daarmee alleen afhankelijk van de input waarden. Als een functie vaker met dezelfde argumenten wordt aangeroepen blijft het resultaat altijd gelijk. Dit maakt functies meer voorspelbaar en makkelijker te testen.

In de dagelijkse praktijk interfacen we echter met een statevolle omgeving: de wereld. Of we nu communiceren met bestanden op schijf, servers op het internet of databases in het netwerk, de staat van de wereld veranderd door iedere actie.

De brug tussen deze statevolle praktijk en stateloze theorie kan worden geslagen door de stateveranderingen op de buitenwereld stateloos te beschrijven. De statevolle functie int std::getchar() levert mogelijk steeds verschillende waardes op, terwijl we deze ook kunnen modelleren als een stateloze functie std::tuple<int, RealWorld> getchar(RealWorld). Gegeven dezelfde state van RealWorld, retourneert getchar nu hetzelfde karakter, tezamen met een nieuwe RealWorld waaruit dit karakter gelezen is.

Daar waar we met de Maybe monade weg abstraheren van alle statevolle precondities kunnen we voor IO een nieuwe monade introduceren om weg te abstraheren van de alle statevolle input en output.

We laten het als een eenvoudige oefening aan de lezer om de bijbehorende coherentie voorwaarden voor de IO-monade te valideren. Zoals IO en Maybe zijn er nog veel meer monades. Voor veel idiomen en patronen in diverse programmeertalen kunnen bijbehorende monades worden geformuleerd. Niet alleen bevordert dit abstractie en herbruikbaarheid, maar de syntactische reductie van complexe algoritmiek maakt deze inzichtelijker en dus beter onderhoudbaar. Het vergt enkel een scherpe blik om de vele monades om je heen te herkennen en extraheren.

Wiskundige achtergrond

Ofschoon het niet noodzakelijk is om de oorsprong van monades te begrijpen om ermee te kunnen werken, helpt het mij om een dieper begrip van de zaak te hebben. Voor diegenen met een wiskundige achtergrond of interesse geef ik in dit tweede deel dan ook een beknopt overzicht van monades uit het wiskundig deelgebied van de categorie theorie.

monade - wiskundige achtergrond

Een categorie (of 1-categorie) C is een paar van klassen (C0, C1) van respectievelijk zogenaamde objecten en morfismen met een extra structuur. Deze extra structuur bestaat uit de volgende onderdelen:

  • Ieder morfisme in C heeft een uniek zogenaamd domein object en codomein object in C. Conceptueel is ieder morfisme een pijl van diens domein naar diens codomein.
  • Voor ieder tweetal morfismen die kop-staart liggen voorziet de extra structuur in een compositie van morfismen. Voor f : X -> Y en g : Y -> Z is er een compositie gf : X -> Z.
  • Ieder object X heeft een zogenaamd identiteitsmorfisme 1X : X -> X, zodat voor alle morfismen f : Y -> Z geldt dat 1Zf = f en f1Y = f. Uniciteit volgt uit existentie, want als 1X en 1’X beiden identiteiten voor X zouden zijn, dan geldt dat 1’X = 1X1’X = 1X.

Een functor is vervolgens een gerichte associatie tussen twee categorieën. Bijvoorbeeld, F : C -> D representeert twee associaties F0 en F1 tussen respectievelijk de objecten en morfismen van beide categorieën, waarbij aan de volgende voorwaarden is voldaan:

  • Voor alle samenstelbare C-morfismen f en g als voorheen, geldt dat F(gf) = F(g)F(f) of F(gf) = F(f)F(g). De functor F heet dan respectievelijk covariant of contravariant.
  • Voor alle objecten X van C geldt dat F(1X) = 1F(X).

Gegeven twee (covariante) functoren F, G : C -> D, dan is een natuurlijke transformatie µ : F => G een klasse van D-morfismen µX : F(X) -> G(X) voor alle objecten X van C, zodanig dat voor alle C-morfismen f : Y -> Z geldt dat µZF(f) = G(f)µY. Ook natuurlijke transformaties kunnen op canonieke wijze worden samengesteld. Voor een ν : G => H definiëren we νµ : F => H voor C-componenten X als (νµ)X = νXµX.

Enkele voorbeelden van de begrippen die we tot nu toe hebben besproken.

  • Set is de categorie van verzamelingen als objecten en functies als morfismen.
  • Cat is de categorie van (lokaal kleine) categorieën met functoren als morfismen. Een categorie is lokaal klein als voor alle objecten X en Y van C, de morfismen X -> Y in C een verzameling Hom(X,Y) vormen.
  • Voor iedere categorie C heeft de categorie Cop dezelfde objecten als C, maar zijn alle morfismen in richting omgedraaid. Als zodanig is iedere contravariante functor F : C -> D gelijk aan covariante functoren F : Cop -> D en F : C -> Dop.
  • Mon is de categorie van monoïden met monoïde homomorfismen als morfismen. Er is een functor Mon -> Cat die aan iedere monoïde M de categorie met slechts een object * en voor ieder element van M een morfisme * -> * toekent, waarbij de compositie gegeven is door de binaire operatie van de monoïde. In deze hoedanigheid is het evident hoe monoïden aan hun naam komen.
  • Gegeven twee categorieën C en D, dan is DC de categorie met functoren C -> D als objecten en natuurlijke transformaties tussen deze functoren als morfismen.
  • Gegeven een topologische ruimte X. Diens topologie T vormt een categorie met inclusie van deelverzamelingen van X als morfismen. Een contravariante functor T -> C is een preschoof op de categorie C. Deze preschoven vormen een categorie met de restrictiemorfismen als morfismen.
  • Een functor tussen lokaal kleine categorieën heet volledig of getrouw als diens componenten respectievelijk surjectief of injectief zijn, beschouwd als klasse van functies tussen Hom-verzamelingen. Een functor is een inbedding als deze zowel volledig als getrouw is. Meer algemeen kent de categorie Presh(D), van contravariante functoren D -> Set op een lokaal kleine categorie D, een canonieke functor y : D -> Presh(D) met y(X)(Y) = Hom(X,Y). y is een inbedding en heet de Yoneda inbedding.
  • Gegeven een functor F : C -> D. Voor X een object in D laat nu ΔX : C -> D de functor zijn die constant is op X. Een kegel op F is nu een paar (X, µX : ΔX => F). De kegels op F vormen een categorie Cone(F) met die C-morfismen f : X -> Y als morfismen (kegel afbeeldingen), waarvoor geldt dat de kegels (X, µX), (Y, µY) transformeren als F(f)µX = µY.
  • Een object T in C heet terminaal als voor alle objecten X van C geldt dat er een uniek morfisme X -> T bestaat. Duaal heet een object initieel als deze terminaal is in Cop. Wederom volgt uniciteit uit existentie. Immers, als T en S beiden terminaal zijn in C, dan zijn er unieke morfismen T -> S en S -> T. Compositie van deze morfismen geeft morfismen S -> S en T -> T. Echter, uit terminaliteit van beide objecten en existentie van een identiteit moet gelden dat deze gelijk zijn aan respectievelijk 1S en 1T. Derhalve zijn S en T per definitie isomorf.
  • Als deze bestaat is de limiet van een functor F : C -> D per definitie het terminale object van de categorie Cone(F).
  • Een discrete categorie is een categorie wiens enige morfismen identiteitsmorfismen zijn. Een functor F : D -> C met D discreet is in essentie een klasse van C-objecten. De limiet (L, µL) van Cone(F) heet derhalve het product van deze objecten. De componenten van µL zijn de projecties op de objecten. Voor C = Set trivialiseert deze constructie tot het cartesisch product op verzamelingen.
  • Gegeven een functor F : 2 -> C met 2 de categorie bestaande uit twee parallelle morfismen, dan heet een limiet van Cone(F) een equalizer. Voor C = Set reduceert dit naar de reguliere equalizer voor functies.
  • Beschouwd voor contravariante functoren c.q. duale categorieën Cop, nemen voorgenoemde begrippen hun duale vorm aan. Zo is een coequalizer de colimiet van Cone(F), ofwel het initiële object van Cone(F), dan wel het terminale object van Cone(F)op.

Monoïdale categorieën

monade - monoidale categorieenMet producten × zoals hiervoor, definiëren we een monoïdale categorie als een categorie C, tezamen met een associatieve functor ⊗ : C × C -> C, genaamd het tensorproduct, en een zogenaamd eenheidsobject I uit C. I moet zich als zowel als links- en rechts-identiteit gedragen ten aanzien van het tensorproduct. Tot slot moeten er een drietal natuurlijke isomorfismen (natuurlijke transformaties die tevens isomorfismen zijn) bestaan die voldoen aan te definiëren coherentie voorwaarden:

  • Associator: α met componenten αX,Y,Z : (X⊗Y)⊗Z -> X⊗(Y⊗Z)
  • Linker en rechter unitor: λ en ρ met componenten λX : I⊗X -> X en ρX : X⊗I -> X

De coherentievoorwaarden zijn:

  • Pentagon commutatie: voor alle W, X, Y, Z objecten van C moet gelden dat (1W ⊗αX,Y,Z) αW,XY,ZW,X,Y⊗1Z) = αW,X,YZ αWX,Y,Z
  • Driehoek commutatie: Voor alle X en Y objecten van C moet gelden dat αX,I,Y(1X⊗λY) = ρX⊗1Y

Een monoïdale categorie heet strikt als diens natuurlijke isomorfismen identiteiten zijn. We laten het als oefening aan de lezer om in te zien dat iedere monoïdale categorie equivalent is aan een strikte monoïdale categorie. Dat wil zeggen, gegeven een monoïdale categorie C, dan bestaan er een strikte monoïdale categorie M en functoren F : C -> M en G : M -> C tezamen met natuurlijke isomorfismen ε : FG => 1M en η : 1C => GF die ook de hiervoor gedefinieerde monoïdale structuur behouden.

Een monoïde (M, µ, η) in een monoïdale categorie (C, ⊗, I) is een object M tezamen met een tweetal morfismen:

  • Vermenigvuldiging: µ : M⊗M -> M
  • Eenheid: η : I -> M

Deze morfismen zijn zodanig dat aan de volgende coherentie voorwaarden is voldaan:

  • Pentagon commutatie: µ (1⊗µ) α = (1⊗µ) µ
  • Unitor commutatie: µ (η⊗1) = λ en µ (1⊗η) = ρ

We bekijken nu enkele voorbeelden van monoïden.

  • Een monoïde in Set, met het cartesisch product als tensorproduct en het singleton als eenheid, is een monoïde in de gebruikelijke zin.
  • Een monoïde in de categorie AbGrp van Abelse (commutatieve) groepen, met ⊗Z het tensorproduct van Abelse groepen en I = Z de groep van gehele getallen als eenheidsobject, is een ring.
  • Een monoïde in de monoïdale categorie van R-modulen: (R-Mod, ⊗R, R), met R een commutatieve ring, is een R-algebra.
  • Voor K een lichaam, is een monoïde in de monoïdale categorie van K-vectorruimten (K-Vect, ⊗K, 0), een K-algebra.
  • Een monoïde in de monoïdale categorie van endofunctoren CC op een categorie C, met compositie als tensorproduct en 1C als eenheid, heet een monade.

    Monade - monades opnieuw

Monades opnieuw

Concreet is een monade dus een monoïde in de monoïdale categorie van endofunctoren op een categorie C. Het is daarmee dus een drietal (T : C -> C, µ : T2 => T, η : 1C => T) dat voldoet aan de coherentie voorwaarden:

  • Associativiteit: µ Tµ = µ µT : T3 => T
  • Identiteit: µ Tη = µ ηT = 1T

De noodzaak voor deze voorwaarden is daarmee evident uit de onderliggende theorie. De relatie met onze C++ implementatie is eveneens vanzelfsprekend wanneer we eenmaal opmerken dat

  • Return(a) = η(a)
  • Bind(f)(m) = µ(Tf)(m)

We besluiten deze blogpost met een stukje monade theorie. Wanneer we de definitie van categorische equivalentie afzwakken tot niet noodzakelijk isomorfe natuurlijke transformaties ε en η, dan houden we adjunctie over. Gegeven, categorieën C en D en functoren F : D -> C, G : C -> D, dan is per definitie F links geadjugeerd aan G als er twee natuurlijke transformaties (unit) ε : GF => 1C en (counit) η : 1D => FG bestaan waarvoor geldt dat 1F = εF Fη en 1G = Gε ηG.

Een dergelijke adjunctie (F, G, ε, η) geeft een monade (GF, η, µ = GεF). Omgekeerd, gegeven een monade (T, η, µ), laat nu Adj(C, T) de categorie van adjuncties (F, G, ε, η) zijn waarvoor geldt dat (GF, η, GεF) = (T, η, µ) op 1C is, met morfismen (F, G, ε, η) -> (F’, G’, ε’, η’) waarvoor geldt dat (F’F, G’G, Gη’F η, ε’F’εG’) een adjunctie is.

  • Een initieel object (FT, GT, η, µT) : C -> CT van Adj(C, T) is een adjunctie op de zogenaamde Kleisli categorie CT.
  • Een terminaal object (FT, GT, η, µT) : C -> CT van Adj(C, T) is een adjunctie op de zogenaamde Eilenberg-Moore categorie CT.

Een adjunctie (F : C -> D, G, ε, η) heet monadisch als D equivalent is aan CT voor T = GF. We noemen een functor monadisch als er een links geadjugeerde functor bestaat waarmee een monadische adjunctie gevormd kan worden.

We poneren de monadiciteitsstelling van Beck ter classificatie van monadische functoren zonder bewijs. Een functor G : D -> C is monadisch dan en slechts dan als aan de volgende voorwaarden is voldaan:

  1. G heeft een links geadjugeerde functor.
  2. G reflecteert isomorfismen. Dat wil zeggen, voor X een object D waarvoor G(X) een isomorfisme in C is, dan is X eveneens een isomorfisme.
  3. D heeft coequalizers voor alle reflexieve paren (tweetallen morfismen met gelijke rechts-inverse) en G behoudt deze coequalizers. Dat wil zeggen, voor E een coequalizer in D, dan is G(E) een coequalizer in C.

We bekijken enkele voorbeelden ter illustratie.

  • De vergeet-functor van de categorie van compacte Haussdorff-ruimtes (met continue afbeeldingen als morfismen) naar de onderliggende verzameling is monadisch met als links geadjugeerde de Stone-Čech compactificatie.
  • De vergeet-functor van semigroepen (en semigroepshomomorfismen als morfismen) naar Set is monadisch, maar behoud niet alle coequalizers. De beperking uit punt 3 is daarom noodzakelijk.
  • De machtsverzameling functor Setop -> Set is monadisch met als links geadjugeerde de functor van Set naar de categorie van vrije complete semi-tralies.
  • De meeste vergeet-functoren hebben links geadjugeerden, omdat zij meestal limieten behouden, maar dit maakt ze nog niet automatisch monadisch. De vergeet-functor van de categorie van topologische ruimten (met eveneens continue afbeeldingen als morfismen) naar Set behoudt weliswaar limieten, maar reflecteert geen isomofismen en is dus niet monadisch.

monades