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
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
