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

8 hours 9 min ago

8 hours 30 min ago

10 hours 18 min ago

10 hours 21 min ago

10 hours 22 min ago

10 hours 29 min ago

10 hours 52 min ago

11 hours 1 min ago

11 hours 7 min ago

11 hours 20 min ago