They give a nice introduction to encoding state as pure functions. In fact, there are many more purely functional encodings for all kinds of data like trees, integers, sum/product types, images, monads, ...
The encodings can be a bit confusing, but really elegant and tiny at the same time. Take for example a functional implementation of the Maybe monad in javascript:
Nothing = nothing => just => nothing
Just = v => nothing => just => just(v)
pure = Just
bind = mx => f => mx(mx)(f)
evalMaybe = maybe => maybe("Nothing")(v => "Just " + v)
console.log(evalMaybe(bind(Nothing)(n => pure(n + 1)))) // Nothing
console.log(evalMaybe(bind(Just(42))(n => pure(n + 1)))) // Just 43
You can derive these implementations from the recursion principle for your type:
data Maybe a = Nothing | Just a
foldMaybe :: (Unit -> r) -> (a -> r) -> Maybe a -> r
The two higher order functions passed into `foldMaybe` are your `Nothing` and `Just` (modulo I added the Unit param to the Nothing case to be a little more precise).
You can see this as replacing an inductive type with its recursor's function type. It's pretty cool in type theory, but not so good for actually programming stuff.
In this particular case IMO it's bad because it essentially removes nominal typing for arguably no benefit.
Even in Lean, a dependently typed language where recursors can be made explicit, people prefer using pattern matching instead of them. There is even sugar for transforming some recursors-like functions into pattern matching like syntax. FYI in Lean recursors are marked as non-computable due to performance concerns, so you can use them to write proofs but not programs.
Seen from yet another point of view, this is transforming inductive types in a function corresponding to a visitor. And yet functional programming folks spent years trying to convince people to replace visitors with proper inductive/algebraic data types and pattern matching, so this idea is a step backwards even for them.
It may be elegant mathematically, but then conveyed through a language that is strictly in the ASCII character set without any alignment or internal justification, they're really just painful to look at.
I think it's all right if you're used to the notation. The first two lines are tagged unions and will be recognisable as such if you're familiar with encodings like Scott/Church pairs/lists/numbers. Once you understand the structure, the definition of `bind` becomes obvious, as its two arguments represent the cases "is nothing" and "is just", where in the first case Nothing is returned, and in the second case the function is applied to the value inside the Just.
I think that writing such code, if only for educational purposes, can be really helpful in actually understanding how the state "flows" during the monadic bind/return. Typical monad instantiations of Maybe do not give such deep insight (at least to me).
> Just because you can do a thing doesn’t mean you should.
Of course you should, where would be the fun in that?
>I think it's all right if you're used to the notation.
Higher mathematics in a nutshell.
>Of course you should, where would be the fun in that?
Also higher mathematics in a nutshell.
Narrator asks: Who should we put in charge of <<thing that will effect people in a tangible way>>?
Not the mathematicians! echo the crowd in unanmity.
Narrator asks: Who will we delegate the task of <<abuse of notation>> to?
The crowd grumbles, arguing amongst themselves whether such a question even warrants an answer. A mathematician stands up, proclaiming "We'll take it!", following up with, "Once you understand the notation involved in my previous statement, you will understand why this outcome is inevitable."
The crowd, seeing the wisdom of not even embarking on that tribulation, assents to the delegation, given the task of undoing the abuse of notation for the legibility of the layperson is also delegated to the aspiring mathematician.
When encoding tagged unions as lambdas, the tags are arguments. In this case `Nothing` has two available tags (`nothing` and `just`) and uses the tag `nothing`. `Just` does the same with the tag `just`, only that the tag gets an additional argument (as does its constructor `Just`), such that the value can be extracted afterwards - just like in an enum:
This is a big reason why legacy production code bases are such a nightmare to work with: developers refuse to learn anything beyond the minimum necessary to pile on yet another band-aid fix and the code base turns into a disorganized ball of mud
Alternative: successive developers each piled on their own, different coding preferences, leading to frankencode that requires keeping every paradigm at once in working memory
The encodings can be a bit confusing, but really elegant and tiny at the same time. Take for example a functional implementation of the Maybe monad in javascript: