Lennart Augustsson <lennart@augustsson.net> wrote in article <439F4539.4070205@augustsson.net> 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)

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

...

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

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

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 <jobmattcon@gmail.com> 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 Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell