I've got a function that's doing something currently working with particular datatypes. I was wondering if I could make it a general. Here's a generalised version of it's signature:
f :: Monad m => ((a -> b) -> c -> d) -> (a -> m b) -> m c -> m d
If the above can't be written, perhaps the more restricted version can?
f2 :: Monad m => ((a -> a) -> b -> b) -> (a -> m a) -> m b -> m b
No, it is impossible, at least without non-termination or unsafe operations.
The argument is essentially similar to this one: we exploit f to inhabit a type which we know can't be inhabited.
Assume there exists
f :: Monad m => ((a -> b) -> c -> d) -> (a -> m b) -> m c -> m d
Specialize c ~ ()
f :: Monad m => ((a -> b) -> () -> d) -> (a -> m b) -> m () -> m d
Hence
(\g h -> f (\x _ -> g x) h (return ()))
:: Monad m => ((a -> b) -> d) -> (a -> m b) -> m d
Speciazlize d ~ a.
(\g h -> f (\x _ -> g x) h (return ()))
:: Monad m => ((a -> b) -> a) -> (a -> m b) -> m a
Speclialize m ~ Cont t
(\g h -> runCont $ f (\x _ -> g x) (cont . h) (return ()))
:: ((a1 -> b) -> a) -> (a1 -> (b -> r) -> r) -> (a -> r) -> r
Take h = const
(\g -> runCont $ f (\x _ -> g x) (cont . const) (return ()))
:: ((r -> b) -> a) -> (a -> r) -> r
Hence
(\g -> runCont (f (\x _ -> g x) (cont . const) (return ())) id)
:: ((r -> b) -> r) -> r
So, the type ((r -> b) -> r) -> r is inhabited, hence by the Curry-Howard isomoprhism it corresponds to a theorem of propositional intuitionistic logic. However, the formula ((A -> B) -> A) -> A is Peirce's law which is known to be non provable in such logic.
We obtain a contradiction, hence there is no such f.
By contrast, the type
f2 :: Monad m => ((a -> a) -> b -> b) -> (a -> m a) -> m b -> m b
is inhabited by the term
f2 = \ g h x -> x
but I suspect this is not what you really want.
There's a problem. Knowing c doesn't give you any information about which as will be passed to (a -> b). You either need to be able to enumerate the universe of as or be able to inspect the provided a arguments with something like
(forall f. Functor f => ((a -> f b) -> c -> f d)
In which case it becomes almost trivial to implement f.
Instead of trying to implement f in general, you should try to generalize your functions like ((a -> b) -> c -> d) to see if you can replace them with lenses, traversals, or something similar.
