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.
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.)