title: Is the Church numeral encoding of natural numbers unnecessarily complicated?
body: <p>The <em>Structure and Interpretation of Computer Programs</em> book I've been reading presents Church numerals by defining zero and an increment function</p>
  
  <pre><code>zero: λf. λx. x
  increment: λf. λx. f ((n f) x)
  </code></pre>
  
  <p>This seemed pretty complicated to me and it took me a really long time to figure it out and derive one (<code>λf.λx. f x</code>) and two (<code>λf.λx. f (f x)</code>).</p>
  
  <p>Wouldn't it be much simpler to encode numbers this way instead, with zero being the empty lambda?</p>
  
  <pre><code>zero: λ
  increment: λf. λ. f
  </code></pre>
  
  <p>Now it's trivial to derive one (<code>λ. λ</code>) and two (<code>λ. λ. λ</code>), and so on.</p>
  
  <p>This seems like a much more immediately obvious and intuitive way to represent numbers with lambdas. Is there some problem with this approach and thus a good reason why Church numerals work the way they do? Is this approach already attested?</p>