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

1 day 22 hours ago

2 days 2 hours ago

2 days 3 hours ago

2 days 14 hours ago

2 days 14 hours ago

2 days 22 hours ago

2 days 23 hours ago

3 days 12 min ago

3 days 18 min ago

3 days 21 min ago