On Monads

Monads are like lions. It is easy to show what a lion is, but afterwards the students won’t understand lions or be able to work with them.

I will use a Java8-like syntax and terminology for code. A monad consists of a generic type M<T> and two functions–M<T> unit(T t) and M<U> bind(M<T> mt, Function<T,M<U>> f)–that satisfy the monad laws:

• bind(unit(x),f) == f(x)
• bind(x,unit) == x
• bind(bind(x,f),g) == bind(x,y -> bind(f.apply(y),g))

That is all.

To understand monads you need to know why people use them. Programs are usually composed of smaller programs and monads let you redefine how composition works. This way, you can extend all datatypes with new operators, while preserving existing ones.

Take the a typical list monad for example. Instances of the generic type List<T> have methods for working with lists as part of the generic type itself. The function unit sends and object x to a one element list unit(x). That way it makes list operations available on the object. On the other hand, unit(x.anyMethod(y)) turns the result of any method defined on x into a list. Finally the function bind(l,f) applies the list valued function f to every element of the list l and concatenates the results in order into one big list. That way we can apply list valued functions to lists like we can apply ordinary functions to ordinary objects. Hence List<T> has access to both the methods of T and of List and also to every possible combination of them.

You can use the list monad for non deterministic algorithms, where functions can have several different return values. Many other kinds of functions and other methods of composition have their own monads. For example, a futures monad takes care of non blocking asynchronous computations while hiding the callback hell that usually goes with it.

Working with monads is a matter of remembering that you introduce a new form of composition on purpose and that you usually neither have to leave it behind, nor want to do so. Generally you want to keep using the bind and unit functions to keep everything happening “inside the monad” until “the end of the world”, which is the main method of your program. As always, practice makes perfect.

Mijn artikel

Ruim een jaar na mijn contract in Warschau eindigde, ben ik nog steeds bezig met het artikel dat de belangrijkste resultaten van mijn onderzoek wereldkundig moet maken. Ik heb wel geprobeerd het af te maken voor mijn contract afliep, maar het resultaat was een onbegrijpelijk artikel vol fouten, dat ik nu nog steeds aan het verbeteren ben.

Ik wilde bij de onderzoekers die zich bezig houden met homotopietypetheorie, interesse wekken in realizeerbaarheidstopossen, het onderwerp waarop ik gepromoveerd ben. Homotopie gaat over de mogelijkheid om topologische ruimtes–dat zijn een zeer algemeen soort meetkundige vormen–door uitrekken en samentrekken, maar zonder te knippen of scheuren, in elkaar om te vormen. Twee topologische ruimtes zijn homotopie-equivalent als zo’n vervorming mogelijk is. Een homotope-type is een homotopie-equivalentieklasse van topologische ruimtes. Homotopietypen dienen de “essentie” van een topologische ruimte te vertegenwoordigen.

Realiseerbaarheid is een poging om constructieve wiskunde toegankelijk te maken voor klassieke wiskundigen. Het intuïtionisme van L.E.J. Brouwer vereist dat elke wiskundige waarheid door een mentale constructie word gerealiseerd. Om dit concreet te maken verving S.C.Kleene de mentale constructies door getallen en bouwde daarmee de recursieve realizeerbaarheidsinterpretatie van de rekenkunde. Wat bijzonder is aan deze interpretatie is dat de uitspraak “P(n) of niet P(n) voor elk getal n” onwaar is voor een zeker predicaat P, hoewel er geen voorbeelden bestaan van getallen waarvoor P(n) waar noch onwaar is. De effectieve topos breid dit idee verder uit. Een topos is een soort parallel wiskundig universum. In de effectieve topos schuilt achter elke vergelijking “x=y” een (mogelijk lege) verzameling van getallen die hem realiseren.

Het verband tussen homotopie en realiseerbaarheid gaat als volgt. Wanneer er een pad ligt tussen twee punten binnen een topologische ruimte dan kunnen we de ruimte zo vervormen dat de punten gelijk worden. Paden realiseren daarmee de vergelijking van hun eindpunten. Homotopietypetheorie lijkt daardoor op een realiseerbaarheid waarin de mentale constructies paden zijn in plaats van getallen. Ik kan ruimtes in een realiseerbaarheidstopos aanwijzen waar die twee soorten realiseerbaarheid samenvallen, de “modest Kan complexes”. Helaas ben ik voorlopig de enige die daarvan overtuigd is.

Het idee van modest Kan complexes was zo wild, dat ik het aanvankelijk niet in mijn onderzoeksvoorstellen durfde te zetten. Ik had op dat moment gewoon te weinig verstand van homotopie. Voor de baan in Warschau moest ik echter verder kijken om aansluiting te vinden bij de onderzoeksgroep. Omdat ik al maanden op zoek was naar een postdoc was ik bovendien een beetje wanhopig.

Ik had er eigenlijk niet op gerekend dat doorgaan in de wetenschap veel moeite zou kosten. Pas toen mijn proefschrift bij de promotiecommissie lag ontdekte ik dat de academische wereld geen gebrek aan mensen heeft en wel aan geld. Tegen de tijd dat ik daadwerkelijk mijn proefschrift moest verdedigen had ik de hoop al opgegeven en besloten de academische wereld te verlaten. Ik werd echter ineens aangenomen in Warschau op dat krankzinnige onderzoeksvoorstel.

In Warschau hebben mijn onderzoeksgroep in ik de simpliciale homotopie bestudeerd. Die theorie maakt met name in het kleine-objecten-argument en in minimale vezelingen gebruik van een paar principes uit de klassieke wiskunde die in niet realiseerbaar zijn. Als ik me niet heel erg vergis, zijn ze overbodig. De constructieve alternatieven zijn echter verschrikkelijk ingewikkeld. Daarom is het een groot probleem om duidelijk te maken dat die alternatieven niet stiekem toch afhankelijk zijn van niet realiseerbare uitspraken.

Ik heb na Warschau de academische wereld alsnog verlaten. Ik probeer nu elke week een paar uurtjes te steken in het herschrijven van mijn artikel.  Er staan een paar preprints op Arxiv en de rest van mijn werk staat op Github. Op die manier heb ik in elk geval een keer de aandacht weten te trekken van homotopietypetheorieonderzoekers. Ik zit nu te worstelen met het laatste grote bewijs. Daarna moet ik een voorbeeld toevoegen, de inleiding aanpassen en uitgebreid op fouten controleren. Ik ben daar nog wel even zoet mee.