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 |
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 |
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 |
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 |
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 |
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 |
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 |
In reply to this post by Lennart Augustsson
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.
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
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 |
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 |
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 |
[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 |
> > 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 |
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 |
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 |
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:
_______________________________________________ Haskell mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell |
Free forum by Nabble | Edit this page |