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

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
15 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 mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell
Reply | Threaded
Open this post in threaded view
|

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

Donald Bruce Stewart
lennart:

> 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)

I've written a little plugin to use Djinn from lambdabot. You
can interact with it on the #haskell irc channel *right now*

Transcript:

    15:39:01 <dons> @djinn a -> b -> a
    15:39:02 <lambdabot> x :: a -> b -> a
    15:39:02 <lambdabot> x x1 _ = x1
    15:39:11 <dons> @djinn (a -> b -> c) -> ((a,b) -> c)
    15:39:11 <lambdabot> x :: (a -> b -> c) -> (a, b) -> c
    15:39:11 <lambdabot> x x1 (v3, v4) = x1 v3 v4
    15:39:27 <dons> @djinn (a -> b) -> (c -> b) -> Either a c -> b
    15:39:27 <lambdabot> x :: (a -> b) -> (c -> b) -> Either a c -> b
    15:39:27 <lambdabot> x x1 x2 x3 = case x3 of
    15:39:27 <lambdabot>      Left l4 -> x1 l4
    15:39:27 <lambdabot>      Right r5 -> x2 r5
    15:40:06 <xerox> @djinn a -> [a] -> [a]
    15:40:07 <lambdabot> x :: a -> [a] -> [a]
    15:40:07 <lambdabot> x _ x2 = x2
    15:40:08 <dons> @help djinn
    15:40:09 <lambdabot>  @djinn <type>
    15:40:09 <lambdabot> Generates Haskell code from a type.

And then we go crazy with @djinn for about 10 minutes :)

Great stuff Lennart.

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

[Haskell-cafe] Announcing Djinn, new version 2004-12-13

Lennart Augustsson
In reply to this post by Lennart Augustsson
There is a new version of Djinn available, with two notable
new features: Haskell data types can be defined and the
found functions are sorted (heuristically) to present the
best one first.

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.

`-- 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, new version 2004-12-13

Chung-chieh Shan-2
Lennart Augustsson <[hidden email]> wrote in article <[hidden email]> in gmane.comp.lang.haskell.general:
> There is a new version of Djinn available, with two notable
> new features: Haskell data types can be defined and the
> found functions are sorted (heuristically) to present the
> best one first.

Hello,

I wonder why the only Church numerals Djinn found were 0 and 1?

    Djinn> :set +m
    Djinn> num ? (a -> a) -> (a -> a)
    num :: (a -> a) -> a -> a
    num x1 x2 = x1 x2
    -- or
    num _ x2 = x2

Very cool, in any case.

        Ken

--
Edit this signature at http://www.digitas.harvard.edu/cgi-bin/ken/sig
Medicine makes people ill, mathematics makes them sad, and theology
makes them sinful. -- Martin Luther (1483-1546)

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

Cabal support for djinn

Henning Guenther
In reply to this post by Lennart Augustsson
Hi Lennart,

I really like djinn and decided to write a quick darcs patch for it so
one can use cabal (http://haskell.org/cabal/) for building it. As I
couldn't find any license informations, I inserted "AllRightsReserved"
as the license field. Feel free to change that! I'd love to see it being
released under a GPL or BSD style license, but that's just my opinion.

Henning

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

cabal.darcs-patch.gz (4K) Download Attachment
signature.asc (196 bytes) Download Attachment
Reply | Threaded
Open this post in threaded view
|

[Haskell-cafe] Re: Re: Announcing Djinn, new version 2004-12-13

Lennart Augustsson
In reply to this post by Chung-chieh Shan-2
Well, the proof search is terminating (and complete) so
it has to stop somewhere.  That happens to be result with
this particular search strategy.

        -- Lennart

Chung-chieh Shan wrote:

> Lennart Augustsson <[hidden email]> wrote in article <[hidden email]> in gmane.comp.lang.haskell.general:
>
>>There is a new version of Djinn available, with two notable
>>new features: Haskell data types can be defined and the
>>found functions are sorted (heuristically) to present the
>>best one first.
>
>
> Hello,
>
> I wonder why the only Church numerals Djinn found were 0 and 1?
>
>     Djinn> :set +m
>     Djinn> num ? (a -> a) -> (a -> a)
>     num :: (a -> a) -> a -> a
>     num x1 x2 = x1 x2
>     -- or
>     num _ x2 = x2
>
> Very cool, in any case.
>
> Ken
>

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

Re: Cabal support for djinn

Lennart Augustsson
In reply to this post by Henning Guenther
Thanks!  It's in the next version.
I'll also make the license less restrictive.  (With no
explicit copyright information in the files the default
copyright applies, i.e., I have all rights.)

        -- Lennart

Henning Günther wrote:
> Hi Lennart,
>
> I really like djinn and decided to write a quick darcs patch for it so
> one can use cabal (http://haskell.org/cabal/) for building it. As I
> couldn't find any license informations, I inserted "AllRightsReserved"
> as the license field. Feel free to change that! I'd love to see it being
> released under a GPL or BSD style license, but that's just my opinion.
>
> Henning

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

Re: Announcing Djinn, new version 2004-12-13

Roy Dyckhoff
In reply to this post by Lennart Augustsson
[Haskell] Re: Announcing Djinn, new version 2004-12-13
Chung-chieh Shan wrote:

I wonder why the only Church numerals Djinn found were 0 and 1?

    Djinn> :set +m
    Djinn> num ? (a -> a) -> (a -> a)
    num :: (a -> a) -> a -> a
    num x1 x2 = x1 x2
    -- or
    num _ x2 = x2

Very cool, in any case.

        Ken

My answer would be the same as Lennart's; in detail, the point of this calculus (or, rather, the G4ip calculus on which the implementation is based) is that it is terminating---proofs are of bounded depth. (No loop-checking or tricks like "iterative deepening" are required.)

The idea for the calculus goes back not to myself but to Vorob'ev (1950), and was rediscovered around 1988-1990 by several people, notably (and independently) Joerg Hudelmaier (Arch. Math. Logic 1992; JLC 1993), Pat Lincoln et al (LICS 1991) and myself (JSL 1992). I called the calculus "LJT"(the "T" is for terminating) and abandoned this when Herbelin later named two important related calculi "LJT" and "LJQ".  "G4ip" is the name used in the Basic Proof Theory book by Troelstra & Schwichtenberg.

        Roy

-- 
------------------------------------------------------------------------
Roy Dyckhoff                                 e-mail: [hidden email]
(Researcher; Senior Lecturer;  Director of Teaching; ...)

School of Computer Science                      
University of St Andrews                            tel: +44-1334-463267
North Haugh, St Andrews,                           ^fax: +44-1334-463278
Fife, KY16 9SX, Scotland                           secr: +44-1334-463253
                                                   *mob: +44-7985-266847
Home page:    http://www.dcs.st-and.ac.uk/~rd

* Mobile number is for emergency use only    ;-)

^ There's also a personal e-fax number: +44-8707-064-446, which then
sends me an e-mail with the fax as an attachment.

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

Re: Re: Cabal support for djinn

Isaac Jones-2
In reply to this post by Lennart Augustsson
Lennart Augustsson <[hidden email]> writes:

> Thanks!  It's in the next version.
> I'll also make the license less restrictive.  (With no
> explicit copyright information in the files the default
> copyright applies, i.e., I have all rights.)

I just grabbed the darcs version and uploaded it to hackage, the
Haskell Package Database (Beta):

http://hackage.haskell.org/ModHackage/Hackage.hs?action=view



peace,

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

Djinn and the inverse of a typechecker

oleg-7
In reply to this post by Chung-chieh Shan-2

Lennart Augustsson wrote:
> I've written a small program that takes a (Haskell) type
> and gives you back a function of that type if one exists.

I'd like to point out an alternative approach: if we implement
a typechecker as a _pure_ logical relation
        (typecheck term type)
between a term and its type, we can use the relation to typecheck a
term, to find term(s) for a given type, or to give some part of the
term and some part of the type and ask the system to fill in the
missing parts.

That has been done. In fact, Dan Friedman is asking the students in
his C311 class to do exactly that:
        http://www.cs.indiana.edu/l/www/classes/c311
(e.g., Assignment 11)


In the following example we will be using a simplified (and perhaps,
more elegant) system than the one used in the class. The typechecker
uses only conjunctions and disjunctions. The evaluator of the logic
system is complete: if there is a solution, the evaluator
will always find it in finite time. The evaluator is also quite fast
and _very_ simple, and is the same as the one described in
  http://pobox.com/~oleg/ftp/Computation/monads.html#fair-bt-stream

The code for the typechecking relation can be found at kanren.sf.net,
file kanren/mini/type-inference.scm (it may take some time for the
code to be visible via viewCVS). The code implements the second
algorithm in the file kanren/examples/type-inference.scm


For example, we can ask the system to give us 5 terms of the type
Int->Int:

> (run 5 (q) (!- q '(--> int int)))
((lambda (_.0) (var _.0))
 (if (boolc _.0)
     (lambda (_.1) (var _.1))
     (lambda (_.2) (var _.2)))
 (lambda (_.0) (intc _.1))
 (if (zero? (intc _.0))
     (lambda (_.1) (var _.1))
     (lambda (_.2) (var _.2)))
 (lambda (_.0) (sub1 (var _.0))))

The results are naturally sorted in complexity of their derivation.
The terms and the types both are given in the prefix notation. The
terms can be pretty-printed as Haskell terms, of course.

We can ask the system for the first few terms of the type (a->a)->a->a
This is the polymorphic type, hence we use eigen variables (i.e.,
symbols):

> (run 10 (q) (!- q `(--> (--> a a) (--> a a))))
((lambda (_.0) (var _.0))
 (if (boolc _.0)
     (lambda (_.1) (var _.1))
     (lambda (_.2) (var _.2)))
 (app (lambda (_.0) (var _.0)) (lambda (_.1) (var _.1)))
 (if (zero? (intc _.0))
     (lambda (_.1) (var _.1))
     (lambda (_.2) (var _.2)))
 (lambda (_.0) (if (boolc _.1) (var _.0) (var _.0)))
 (if (boolc _.0)
     (if (boolc _.1)
         (lambda (_.2) (var _.2))
         (lambda (_.3) (var _.3)))
     (lambda (_.4) (var _.4)))
 (lambda (_.0) (lambda (_.1) (var _.1)))
 (fix (lambda (_.0) (var _.0)))
 (if (if (boolc _.0) (boolc _.1) (boolc _.2))
     (lambda (_.3) (var _.3))
     (lambda (_.4) (var _.4)))
 (lambda (_.0) (if (zero? (intc _.1)) (var _.0) (var _.0))))

There are Church numerals 1 and 0, and some curious terms like (fix id)
-- which certainly has the required type (as well as any other).

But suppose we wish to see only lambda-terms. That is easy to
arrange. We specify the parts we want, and let the system find the rest:
> (run 5 (q)
    (fresh (_) (== q `(lambda . ,_)) (!- q `(--> (--> a a) (--> a a)))))

((lambda (_.0) (var _.0))
 (lambda (_.0) (if (boolc _.1) (var _.0) (var _.0)))
 (lambda (_.0) (lambda (_.1) (var _.1)))
 (lambda (_.0) (if (zero? (intc _.1)) (var _.0) (var _.0)))
 (lambda (_.0) (app (lambda (_.1) (var _.1)) (var _.0))))

OTH, if we are only interested in combinators, we can make the
typechecking relation that uses only abstractions and applications:

(define sc!-
  (lambda (self)
    (lambda (e t)
      (conde
        (((lambda-rel self) e t))
        (((app-rel self) e t))
        ;(((fix-rel self) e t))
        ;(((polylet-rel self) e t))
        ))))
       
(define c!- (sc!- sc!-))

(time
  (map unparse
    (run 10 (q)
      (fresh (_) (== q `(lambda . ,_)) (c!- q '(--> (--> a a) (--> a a)))))))
>
((lambda (_.0) _.0)
 (lambda (_.0) (lambda (_.1) _.1))
 (lambda (_.0) ((lambda (_.1) _.1) _.0))
 (lambda (_.0) (lambda (_.1) (_.0 _.1)))
 (lambda (_.0) (((lambda (_.1) _.1) (lambda (_.2) _.2)) _.0))
 (lambda (_.0) (lambda (_.1) ((lambda (_.2) _.2) _.1)))
 (lambda (_.0) ((lambda (_.1) _.1) (lambda (_.2) _.2)))
 (lambda (_.0) (lambda (_.1) (_.0 (_.0 _.1))))
 (lambda (_.0) ((lambda (_.1) _.0) _.0))
 (lambda (_.0)
   (lambda (_.1) (((lambda (_.2) _.2) _.0) _.1))))

(time (map unparse ...))
    no collections
    1 ms elapsed cpu time
    1 ms elapsed real time
    67088 bytes allocated

And so we see Church numerals 0, 1, and 2 as the answers. The
typechecker and the logic system evaluator are running in a Petite
Chez *interpreter*. As we can see, the system is quite fast (Pentium
IV 2GHz).

The source code at the end of the file demonstrates inferring the
expressions for call/cc and bind in the continuation monad. The is
also an example for inferring the code for shift and reset.

Although Kanren is the first-order logic system, predicates are
first-class and can be passed around as arguments, returned as
results, etc. In particular, the typechecking algorithm implements the
type environment as such a predicate; we use open recursion to be able
to extend the environment, and so to typecheck abstractions, as well as
let-forms *with* let-polymorphism. The typechecker is a *pure*
predicate (that is, uses no `cuts', `var' or other infamous features
of logic languages).
_______________________________________________
Haskell mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell
Reply | Threaded
Open this post in threaded view
|

Re: Djinn and the inverse of a typechecker

Lennart Augustsson
[hidden email] wrote:
> In the following example we will be using a simplified (and perhaps,
> more elegant) system than the one used in the class. The typechecker
> uses only conjunctions and disjunctions. The evaluator of the logic
> system is complete: if there is a solution, the evaluator
> will always find it in finite time.

Is it also terminating?  So if there is no solution it will tell you so.

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

Re: Djinn and the inverse of a typechecker

oleg-7

> > The evaluator of the logic
> > system is complete: if there is a solution, the evaluator
> > will always find it in finite time.
>
> Is it also terminating?  So if there is no solution it will tell you so.

The evaluator used in the yesterday's message -- no. It is merely
complete; if no solution exists, it may terminate, but it is not
obliged to. It depends on the formulation of the problem.

We do have a refutationally complete evaluator, which does find a
contradiction if one exists. It easily handles the problems like (in
Prolog notation)
        X = 1, repeat, X = 2
and more complex problems. It might work for the de-typechecker, I
haven't tried. Alas, it takes _too_ much time at present for problems I
really want it to use; those problems, in addition to large depth,
have a very large breadth...

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

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

Martin
In reply to this post by Lennart Augustsson

After reading this post, i can only see a -> b

how to define more specific such as

flow 0 y = y
flow z flow x, y = flow z+x, y

could you demonstrate using djinn to do above mapping definition
to generate a function?



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

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

Ivan Lazar Miljenovic
On 7 April 2011 14:35, Martin <[hidden email]> wrote:
>
> flow 0 y = y
> flow z flow x, y = flow z+x, y

This doesn't appear to be a valid function definition...

--
Ivan Lazar Miljenovic
[hidden email]
IvanMiljenovic.wordpress.com

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

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

Lennart Augustsson
In reply to this post by Martin
Djinn takes a type, what you have written does not appear to be a type.

  -- Lennart

On Thu, Apr 7, 2011 at 3:35 PM, Martin <[hidden email]> wrote:

After reading this post, i can only see a -> b

how to define more specific such as

flow 0 y = y
flow z flow x, y = flow z+x, y

could you demonstrate using djinn to do above mapping definition
to generate a function?



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


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