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