24 Jan
2010
24 Jan
'10
6:26 p.m.
On Sun, Jan 24, 2010 at 3:12 PM, Stephen Tetley
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.