Re: [Haskell-cafe] currying combinators

David Sankel wrote:

keep :: ((t -> b) -> u -> b) -> ((t1 -> t) -> b) -> (t1 -> u) -> b

On Wed, May 26, 2010 at 12:49 PM, Lennart Augustsson

...

wrote:

...

There are no interesting (i.e. total) functions of that type.

I wonder how one would prove that to be the case. I tried and didn't come up with anything.

By parametricty, presumably. We must ultimately construct some value of type b, where b is universally quantified. Therefore, the only 'constructors' available for b are the ((t -> b) -> u -> b) and ((t1 -> t) -> b) arguments. However, since b is universally quantified, these arguments have no way of actually constructing some b, other than by returning bottom. Remember, if a language lacks typecase, (forall a. X -> a) is just another way of saying (X -> Void). -- Live well, ~wren