[Haskell-cafe] Naive booleans and numbers - type-checking fails

[Derek Elkins]

On Sun, Jan 24, 2010 at 3:12 PM, Stephen Tetley
<stephen.tetley at gmail.com> wrote:
> Doesn't the simply typed lambda calculus introduce if-then-else as a
> primitive precisely so that it can be typed?
>
> Its not an illuminating answer to your question and I'd welcome
> clarification for my own understanding, but I don't think you can
> solve the problem without appealing to Haskell's built-in
> if-then-else.

Yes, encoding data types as pure typed lambda terms requires rank-2
types.  I'd recommend that Dušan Kolář start giving types to all these
functions.  However, it will, eventually, be necessary to go beyond
Haskell 98 to give the appropriate types.