monads - How to apply higher order function to an effectful function in Haskell?

Question

I have too functions:

higherOrderPure :: (a -> b) -> c
effectful :: Monad m => (a -> m b)

I'd like to apply the first function to the second:

higherOrderPure `someOp` effectful :: Monad m => m c

where

someOp :: Monad m => ((a -> b) -> c) -> (a -> m b) -> m c

Example:

curve :: (Double -> Double) -> Dia Any 
curve f = fromVertices $ map p2 [(x, f x) | x <- [1..100]]

func :: Double -> Either String Double
func _ = Left "Parse error" -- in other cases this func can be a useful arithmetic computation as a Right value

someOp :: ((Double -> Double) -> Dia Any) -> (Double -> Either String Double) -> Either String (Dia Any)
someOp = ???

curve `someOp` func :: Either String (Dia Any)

Answer 1

The type

Monad m => ((a -> b) -> c) -> (a -> m b) -> m c

is not inhabited, i.e., there is no term t having that type (unless you exploit divergence, e.g. infinite recursion, error, undefined, etc.).

This means, unfortunately, that it is impossible to implement the operator someOp.

Proof

To prove that it is impossible to construct such a t, we proceed by contradiction. Assume t exists with type

t :: Monad m => ((a -> b) -> c) -> (a -> m b) -> m c

Now, specialize c to (a -> b). We obtain

t :: Monad m => ((a -> b) -> a -> b) -> (a -> m b) -> m (a -> b)

Hence

t id :: Monad m => (a -> m b) -> m (a -> b)

Then, specialize the monad m to the continuation monad (* -> r) -> r

t id :: (a -> (b -> r) -> r) -> ((a -> b) -> r) -> r

Further specialize r to a

t id :: (a -> (b -> a) -> a) -> ((a -> b) -> a) -> a

So, we obtain

t id const :: ((a -> b) -> a) -> a

Finally, by the Curry-Howard isomorphism, we deduce that the following is an intuitionistic tautology:

((A -> B) -> A) -> A

But the above is the well-known Peirce's law, which is not provable in intuitionistic logic. Hence we obtain a contradiction.

Conclusion

The above proves that t can not be implemented in a general way, i.e., working in any monad. In a specific monad this may still be possible.