[Haskell-cafe] What inhabits this type: (forall a. a -> b) ->
(forall a. m a -> m b)
Stefan O'Rear
stefanor at cox.net
Tue Feb 27 18:13:18 EST 2007
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
More information about the Haskell-Cafe
mailing list