[Haskell-cafe] Announcing Djinn, version 2004-12-11, a coding wizard
Howdy, y'all! 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. :) Share and enjoy. -- Lennart
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.
Doh! It seems your code takes a string representing the type and returns a string representing the code, whereas I expected at first you were doing some funky type class molestation so you can use "djinn" in your code and let Haskell fill it in. Stefan
On Thu, Dec 15, 2005 at 01:47:55AM -0500, Stefan Monnier wrote:
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.
Doh! It seems your code takes a string representing the type and returns a string representing the code, whereas I expected at first you were doing some funky type class molestation so you can use "djinn" in your code and let Haskell fill it in.
That would be nice, imagine: instance Monad MyMonad where return = djinn (>>=) = djinn or even newtype MyMonad a = ... djinning (Monad, Functor) ;-> Best regards Tomasz -- I am searching for a programmer who is good at least in some of [Haskell, ML, C++, Linux, FreeBSD, math] for work in Warsaw, Poland
I've certainly thought of providing the functionality you want, but I've not done that yet. Internally djinn uses some kind of ASTs, it might be possible to use GADTs to do what you want in a type safe way. If not it should be possible to use Dynamic. -- Lennart Stefan Monnier wrote:
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.
Doh! It seems your code takes a string representing the type and returns a string representing the code, whereas I expected at first you were doing some funky type class molestation so you can use "djinn" in your code and let Haskell fill it in.
Stefan
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Or some TH... $(djinn [t| a -> a |]) or something like it. lennart:
I've certainly thought of providing the functionality you want, but I've not done that yet. Internally djinn uses some kind of ASTs, it might be possible to use GADTs to do what you want in a type safe way. If not it should be possible to use Dynamic.
-- Lennart
Stefan Monnier wrote:
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.
Doh! It seems your code takes a string representing the type and returns a string representing the code, whereas I expected at first you were doing some funky type class molestation so you can use "djinn" in your code and let Haskell fill it in.
Stefan
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
participants (4)
-
dons＠cse.unsw.edu.au -
Lennart Augustsson -
Stefan Monnier -
Tomasz Zielonka