[Haskell] Djinn and the inverse of a typechecker

[oleg at pobox.com]

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