[Haskell-cafe] currying combinators

[wren ng thornton]

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 <lennart at augustsson.net
>> 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