Djinn does this for a restricted subset of Haskell types, corresponding to a first-order logic. It can’t manage recursive types or types that require recursion to implement, though; so, for instance, it can’t write a term of type (a -> a) -> a
(the type of fix
), which corresponds to the proposition “if a implies a, then a“, which is clearly false; you can use it to prove anything. Indeed, this is why fix
gives rise to ⊥.
If you do allow fix
, then writing a program to give a term of any type is trivial; the program would simply print fix id
for every type.
Djinn is mostly a toy, but it can do some fun things, like deriving the correct Monad
instances for Reader
and Cont
given the types of return
and (>>=)
. You can try it out by installing the djinn package, or using lambdabot, which integrates it as the @djinn
command.