[Haskell-cafe] currying combinators

wren ng thornton wren at freegeek.org
Thu May 27 13:43:57 EDT 2010


wren ng thornton wrote:
> David Sankel wrote:
>> keep :: ((t -> b) -> u -> b) -> ((t1 -> t) -> b) -> (t1 -> u) -> b
>>
>> 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.

Er, that's not quite right. That's only true if those arguments are 
rank-2 quantified. I'd had a longer (correct) explanation and tried 
shortening it. So here's the better proof:


In order to produce a value of type b, keep must either use one of those 
two arguments or return bottom.

If it uses the ((t -> b) -> u -> b) argument, then keep can only return 
non-bottom if that function [1] ignores its arguments and returns an 
arbitrary b, or [2] uses the (t -> b) argument to construct the b. If we 
assume #1 then keep is not total, because we have no way of proving that 
the assumption is valid. So we must expect #2; so in order for keep to 
be total it must be able to construct a total function (t -> b). In 
order to construct such a function it must use one of the original two 
arguments, so this is only possible if we can construct a b via ((t1 -> 
t) -> b).

If it uses the ((t1 -> t) -> b) argument, then keep can only return 
non-bottom if that function [1] ignores its arguments, or [2] uses the 
(t1 -> t) argument. We can't assume #1 and be total, so we must expect 
#2. In order to construct (t1 -> t) we must construct a t. But, since t 
is universally quantified, keep knows of no total functions which return 
t. Thus, keep can only construct a function which returns bottom.

Thus, keep can only return non-bottom under the assumption that the ((t 
-> b) -> u -> b) and ((t1 -> t) -> b) arguments ignore their arguments 
to return a constant b.

-- 
Live well,
~wren


More information about the Haskell-Cafe mailing list