Announcing Djinn, version 2004-12-11, a coding wizard
lennart at augustsson.net
Sun Dec 11 17:58:49 EST 2005
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. :)
Share and enjoy.
More information about the Haskell-Cafe