Announcing Djinn, version 2004-12-11, a coding wizard

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
7 messages Options
Reply | Threaded
Open this post in threaded view
|

Announcing Djinn, version 2004-12-11, a coding wizard

Lennart Augustsson
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
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Announcing Djinn, version 2004-12-11, a coding wizard

Stefan Monnier
> 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
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Re: Announcing Djinn, version 2004-12-11, a coding wizard

Tomasz Zielonka
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
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Re: Announcing Djinn, version 2004-12-11, a coding wizard

Lennart Augustsson
In reply to this post by Stefan Monnier
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
> [hidden email]
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Re: Announcing Djinn, version 2004-12-11, a coding wizard

Donald Bruce Stewart
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
> >[hidden email]
> >http://www.haskell.org/mailman/listinfo/haskell-cafe
> >
>
> _______________________________________________
> Haskell-Cafe mailing list
> [hidden email]
> http://www.haskell.org/mailman/listinfo/haskell-cafe
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Announcing Djinn, version 2004-12-11, a coding wizard

oleg-7
In reply to this post by Lennart Augustsson

Stefan Monnier wrote:
> 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 has already been done:

De-typechecker: converting from a type to a term
http://www.haskell.org/pipermail/haskell/2005-March/015423.html

``We ask the Haskell typechecker to derive us a function of the
specified type. We get the real function, which we can then apply to
various arguments. ... Informally, we converted from `undefined' to defined.

It must be emphasized that no modifications to the Haskell compiler are
needed, and no external programs are relied upon. In particular,
however surprising it may seem, we get by without `eval' -- because
Haskell has reflexive facilities already built-in.''


_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Announcing Djinn, version 2004-12-11, a coding wizard

Lennart Augustsson
Very cool! :)

[hidden email] wrote:

> Stefan Monnier wrote:
>
>>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 has already been done:
>
> De-typechecker: converting from a type to a term
> http://www.haskell.org/pipermail/haskell/2005-March/015423.html
>
> ``We ask the Haskell typechecker to derive us a function of the
> specified type. We get the real function, which we can then apply to
> various arguments. ... Informally, we converted from `undefined' to defined.
>
> It must be emphasized that no modifications to the Haskell compiler are
> needed, and no external programs are relied upon. In particular,
> however surprising it may seem, we get by without `eval' -- because
> Haskell has reflexive facilities already built-in.''
>
>

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe