Lennart Augustsson announced Djinn on 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
Djinn> type C a = (a -> r) -> r
Djinn> returnC ? a -> C a
returnC :: a -> C a
returnC x1 x2 = x2 x1
Djinn> bindC ? C a -> (a -> C b) -> C b
bindC :: C a -> (a -> C b) -> C b
bindC x1 x2 x3 = x1 (\ c15 -> x2 c15 (\ c17 -> x3 c17))
Djinn> callCC ? ((a -> C b) -> C a) -> C a
callCC :: ((a -> C b) -> C a) -> C a
callCC x1 x2 = x1 (\ c15 _ -> x2 c15) (\ c11 -> x2 c11)
# 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
15:39:27 x x1 x2 x3 = case x3 of
15:39:27 Left l4 -> x1 l4
15:39:27 Right r5 -> x2 r5
15:40:06 @djinn a -> [a] -> [a]
15:40:07 x :: a -> [a] -> [a]
15:40:07 x _ x2 = x2
15:40:08 @help djinn
15:40:09 Generates Haskell code from a type.
Djinn has proven to be much fun on #haskell.