Also reminds me of this: <https://aphyr.com/posts/342-typing-the-technical-interview>

# getting-started

[gabrielfv]

Also reminds me of this: https://aphyr.com/posts/342-typing-the-technical-interview

[karelpeeters]

Haha I tried to read that once but I can't stand the writing style.

[benleggiero]

Every time I see Church Numerals, I die a little inside 😂

[Hullaballoonatic]

Are church numerals when values are aligned vertically, leading sometimes to the values for a single member more than ten spaces away from its declaration?

[karelpeeters]

I believe they're the formal definitions of the numbers in these higher order type systems.

[karelpeeters]

So for the linked article basically this part:

data Z
data S n

type N0 = Z
type N1 = S N0
type N2 = S N1
type N3 = S N2
type N4 = S N3
type N5 = S N4
type N6 = S N5
type N7 = S N6
type N8 = S N7

[gabrielfv]

That's it for the numerals indeed, but the Church concept from lambda calculus is basically the core of the article

[benleggiero]

Church numerals are where:

0 = x
1 = f(x)
2 = f(f(x))
3 = f(f(f(x)))
4 = f(f(f(f(x))))

etc.
For short, they are also written

0 = f⁰(x)
1 = f¹(x)
2 = f²(x)
3 = f³(x)
4 = f⁴(x)

etc.

https://en.wikipedia.org/wiki/Church_encoding#Church_numerals