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.

calvin% djinn
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
# deserve.
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.
Djinn> :q
Bye.

To play with Djinn do a

darcs get http://darcs.augustsson.net/Darcs/Djinn

or get

http://darcs.augustsson.net/Darcs/Djinn/Djinn.tar.gz

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 @djinn
15:40:09 Generates Haskell code from a type.

Djinn has proven to be much fun on #haskell.

## Recent comments

4 hours 52 min ago

5 hours 24 min ago

5 hours 26 min ago

5 hours 31 min ago

11 hours 48 min ago

14 hours 39 min ago

15 hours 38 min ago

15 hours 53 min ago

16 hours 18 min ago

17 hours 57 sec ago