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