[Haskell-cafe] What inhabits this type: (forall a. a -> b) -> (forall a. m a -> m b)

[Stefan O'Rear]

On Tue, Feb 27, 2007 at 06:01:44PM -0500, Jacques Carette wrote:
> Since my last query was answered so quickly, let's try another.
> 
> I have looked on Hoogle.  I would have asked Djinn, but I don't have it 

No you couldn't.  Djinn doesn't support rank2 types.  (FWIW you can go to
#haskell at chat.freenode.org and /msg 'lambdabot' with '@djinn <type>')

> around.  So, can someone find a term that inhabits
> (forall a. a -> b) -> (forall a. m a -> m b)
> ?  I think of this as the type of functions that, given a function from 
> any boxed-up a to a b, will give me a function from a boxed-up ma to a m 
> b -- m does not have to be a Monad!.

undefined (assuming impredicativity ...)

It doesn't exist without _|_.  Proof:

data Void a where
  Void :: Void Int

assumed :: (forall a. a -> b) -> (forall a. m a -> m b)

(const True) :: forall a. a -> Bool

assumed (const True) :: forall m a. m a -> m Bool
assumed (const True) :: Void Int -> Void Bool
assumed (const True) Void :: Void Bool

but there is no constructor of type Void Bool, so assumed (const True) Void
cannot evaluate to WHNF, contradicting our assumtion that assumed exists and
is total, QED.  (Go ahead mathematicians, I expect a good flaming here)

HTH

Stefan