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

At the risk of seeming terribly naive, I'm going to go ahead and share my intuition. Would not any function of type (forall a. a -> b) be a constant function in b? If the function is allowed no inspection of its argument, it must not depend on its argument. The same intuition could be applied to the codomain. The type (forall a. m a -> m b) would tell me that this function is not allowed to inspect the carrier of its input type. I would need to know more about the type variable m in order to suggest what this function could do. E.G. if m were required to be a functor, then the function could be: theFun :: Functor m => (forall a. a -> b) -> (forall a. m a -> m b) theFun f m_a = fmap f m_a Is this the sort of pondering you were after? Gurus: did I miss something? On 2/27/07, 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 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!.

Jacques _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe