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.
a church¹ encoding of booleans:
just says that, given a boolean value, you can choose one of two control flow paths, i.e. do or using the church-encoded version: a product type just means "you can do stuff using the parts", i.e. and that just means you can do e.g. or, using the church encoded version 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`