data Nat = Succ Nat | Zero
가 이렇게 바뀌는 거임:
Zero = \f → \x → x.
Succ = \n → \f → \x → f (n f x).

plus :: Nat → Nat → Nat
plus x Zero = x
plus x (Succ y) = Succ (plus x y)
가 이렇게 바뀌는 거임:
plus = \m → \n → \f → \x → m f (n f x)