Neat, but I think it would have even more interesting to use church encoding for your numbers. It would have shown some of the wonderful inhabitants this seemingly simple structure can lead to :)
not related to the article itself, but Church (or Scott) encoding is, to me, one of the most eye-opening FP concepts – in order to describe a data type, you just write the way it can be pattern-matched on. and that's essentially describing how the value can "drive" your program's control flow, because you give it one or more continuations to call with some arguments.
a church¹ encoding of booleans:
false = λ f t -> f ()
true = λ f t -> t ()
just says that, given a boolean value, you can choose one of two control flow paths, i.e. do
case myBool of
False -> "a"
True -> "b"
or using the church-encoded version:
myBoolEnc
(λ () -> "a")
(λ () -> "b")
a product type just means "you can do stuff using the parts", i.e.
threeAndFive = λ k -> k 3 5
trueAndFoo = λ k -> k true "foo"
and that just means you can do e.g.
case myPair of
(a, b) -> a+b
or, using the church encoded version
myPairEnc
(λ a b -> a+b)
it's like the ultimate "inversion of control" - the values are driving the program by calling the continuations passed to them! tbh i always get chills when i think about this, bc it just seems like such a deep thing... lambdas really are the ultimate everything, especially values :)
(and now, a handwavy, possibly rambling conclusion)
to me, this embodies the fact that booleans, numbers and other values have no inherent meaning - what matters about them is that we can, via pattern matching or something else, distinguish e.g. True and False, or 0 and 13 and 725, and do different things. like, the bits we use to represent binary numbers have no meaning either; what matters about a particular pattern of bits is how it changes the execution of a program relative to other patterns of bits that could be in its place.
---
¹ with some added () to work in non-lazy languages and to highlight that the type `Bool` is just the sum `Unit + Unit`
Yes, it is really cool space to explore and you can keep finding interesting gems :)
>with some added () to work in non-lazy languages and to highlight that the type `Bool` is just the sum `Unit + Unit`
Nice. But it makes sense, also semantically. Booleans are about choice and the types of the sum don't carry information, so they can be unit. While left and right mean false and true.
You don’t think it would have needlessly obscured the point of the article, which was about giving a concrete example of some interesting category theory concepts? This is clearly not a post about lambda calculus, but about explaining some pretty abstract stuff in terms of an example more understandable (at least to people familiar with components).
Also, church-encoding numbers makes no sense if the purpose is to lift JavaScript values into a function which react can swallow.
No, I don't think so. But it depends how you look at the article. If it is about what you can do in javascript then it doesn't make sense. But if you view it as a fun introduction to the algebraic structure of functions, where you use javascript as educational vehicle then yes it makes sense. Church encoding is a consequence of the algebraic structure of functions, which is really cool to realize.
It kinda lights up the bulb in your head, shows you that lambda calculus (which cannot be separated from the algebraic structure of functions) is a powerful concept.
It really is a small universe.