Lennart Augustsson announced Djinnon the Haskell mailing list recently.
He included this demonstration:
I've written a small program that takes a (Haskell) type
and gives you back a function of that type if one exists.
It's kind of fun, so I thought I'd share it.
It's probably best explained with a sample session.
Welcome to Djinn version 2005-12-11.
Type :h to get help.
# Djinn is interactive if not given any arguments.
# Let's see if it can find the identity function.
Djinn> f ? a->a
f :: a -> a
f x1 = x1
# Yes, that was easy. Let's try some tuple munging.
Djinn> sel ? ((a,b),(c,d)) -> (b,c)
sel :: ((a, b), (c, d)) -> (b, c)
sel ((_, v5), (v6, _)) = (v5, v6)
# We can ask for the impossible, but then we get what we
Djinn> cast ? a->b
-- cast cannot be realized.
# OK, let's be bold and try some functions that are tricky to write:
# return, bind, and callCC in the continuation monad
# Well, poor Djinn has a sweaty brow after deducing the code
# for callCC so we had better quit.
To play with Djinn do a
darcs get http://darcs.augustsson.net/Darcs/Djinn
Then just type make. (You need a Haskell 98 implementation and
some libraries.) And then start djinn.
For the curious, Djinn uses a decision procedure for intuitionistic
propositional calculus due to Roy Dyckhoff. It's a variation of
Gentzen's LJ system. This means that (in theory) Djinn will always
find a function if one exists, and if one doesn't exist Djinn will
terminate telling you so.
This is the very first version, so expect bugs. :)
Don Stewart wrote a lambdabot plugin for Djinn a few hours later.
15:39:01 @djinn a -> b -> a
15:39:02 x :: a -> b -> a
15:39:02 x x1 _ = x1
15:39:11 @djinn (a -> b -> c) -> ((a,b) -> c)
15:39:11 x :: (a -> b -> c) -> (a, b) -> c
15:39:11 x x1 (v3, v4) = x1 v3 v4
15:39:27 @djinn (a -> b) -> (c -> b) -> Either a c -> b
15:39:27 x :: (a -> b) -> (c -> b) -> Either a c -> b