[Haskell] Djinn and the inverse of a typechecker

oleg at pobox.com oleg at pobox.com
Thu Dec 15 05:11:34 EST 2005


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


More information about the Haskell mailing list