Is there an effective way to generate a function given a generic (esp. with monads) type signature in Haskell?

Question

I have already seen a variety of questions of the form "Given type signature XXX, find implementation in Haskell." Therefore it is natural to ask whether this can be generalized or algorithmized. A similar question is here. However, it is clear that generally this task is impossible. So the next question is to trade some generality for practicality.

Question: Is the problem decidable if all the type signatures consists of rigid type variables together with some constraints, drawn from a fixed set (e.g. Monad, Traversable, Foldable?)

A typical problem would be (Monad m) => (m j -> [m d]) -> m [j] -> [m [d]], where I used [] instead of (..Constraints t) => t for convenience.

Answer 1

Amazingly enough, this is actually possible! Have a look at Djinn (or you could compile the executable yourself), which implements this for you. For instance, given f :: a -> (a -> b) -> (a -> b -> c) -> c, Djinn outputs f a b c = c a (b a) (amongst other possibilities). You can find more examples (with the command-line version) at http://lambda-the-ultimate.org/node/1178. Unfortunately it doesn’t support typeclasses though, but I wouldn’t rule out another tool that I haven’t found which does support them.

(If you’re interested in how this works, read up about the Curry-Howard Isomorphism, which states that a program in a language such as Haskell is equivalent to a proof. For instance, writing an implementation for f :: a -> (a -> b) -> (a -> b -> c) -> c is equivalent to proving the statement ‘given a proposition a, then if a implies b, and a and b together imply c, then c is true’. Because of this, you can use an automated prover to figure out the implementation and then just mechanically translate this into code to get an implementation.)