# Typelevel Church Numerals in Scala 3

Modeling church numerals as functions in most languages is straightforward.
Scala’s type system is powerful enough that we can represent them *and* express
computation with them directly in the type system!

The definitions in Scala follow immediately from the definitions in the untyped lambda calculus; functions in the latter correspond to typelevel functions in the former.

```
object ChurchNumerals extends App {
type zero[s[_], z] = z
type succ[m[s[_], z], s[_], z] = s[m[s, z]]
type one[s[_], z] = succ[zero, s, z]
type two[s[_], z] = succ[one, s, z]
type plus = [m[_[_], _]] =>> [n[_[_], _]] =>> [s[_], z] =>> m[s, n[s, z]]
type +[m[_[_], _], n[_[_], _]] = [s[_], z] =>> plus[m][n][s, z]
type times = [m[_[_], _]] =>> [n[_[_], _]] =>> [s[_], z] =>> m[[z0] =>> n[s, z0], z]
type *[m[_[_], _], n[_[_], _]] = [s[_], z] =>> times[m][n][s, z]
// use typeclasses to fold over the type structure
trait Nat[T]:
def real: Int
trait Succ[T]
trait Zero
given natForSucc[T](using N: Nat[T]): Nat[Succ[T]] with
override def real: Int = N.real + 1
given natForZero: Nat[Zero] with
override def real: Int = 0
def real[T](using N: Nat[T]): Int =
N.real
type expr[s[_], z] = (one + one + one)[s, z]
type expr2[s[_], z] = (expr * expr)[s, z]
println(real[expr2[Succ, Zero]]) // 9
}
```

It’s been possible to write this out in Scala 2 for a long time (see this post), but the presence of type lambdas in Scala 3 lets us defer some type application until actually we need to “perform evaluation”, which makes for prettier and more composable types.