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