I'd like to point out a different take on Djinn:

http://cvs.sourceforge.net/viewcvs.py/kanren/kanren/mini/type-inference.scm

http://cvs.sourceforge.net/viewcvs.py/kanren/kanren/mini/logic.scm

The first defines the Hindley-Milner typechecking relation for a

language with polymorphic let, sums and products. We use the Scheme

notation for the source language (as explained at the beginning of the

first file); ML or Haskell-like notations are straightforward. The

notation for type terms is infix, with the right-associative arrow.

The typechecking relation relates a term and its type: given a term we

obtain its type. The relation is *pure* and so it can work in reverse: given a type, we can obtain terms that have this type. Or, we can give a term with blanks and a type with blanks, and ask the relation to fill in the blanks.

As an example, the end of the file type-inference.scm shows the derivation for the terms call/cc, shift and reset from their types in the continuation monad. Given the type

(((a -> . ,(cont 'b 'r)) -> . ,(cont 'b 'b)) -> . ,(cont 'a 'b))

we get the expression for shift:

(lambda (_.0) (lambda (_.1)
((_.0 (lambda (_.2) (lambda (_.3) (_.3 (_.1 _.2)))))
(lambda (_.4) _.4))))

It took only 2 milli-seconds.

More interesting is using the typechecker for proving theorems in

intuitionistic logic: see logic.scm. We formulate the proposition in types, for example:

(,(neg '(a * b)) -> . ,(neg (neg `(,(neg 'a) + ,(neg 'b)))))

This is one direction of the deMorgan law. In intuitionistic logic,

deMorgan law is more involved:

NOT (A & B) == NOTNOT (NOT A | NOT B)

The system gives us the corresponding term, the proof:

(lambda (_.0)
(lambda (_.1)
(_.1 (inl (lambda (_.2)
(_.1 (inr (lambda (_.3) (_.0 (cons _.2 _.3))))))))))

The de-typechecker can also prove theorems in classical logic,

via double-negation (aka CPS) translation. The second part of

logic.scm demonstrates that. We can formulate a proposition:

(neg (neg `(,(neg 'a) + ,(neg (neg 'a)))))

and get a (non-trivial) term

(lambda (_.0) (_.0 (inr (lambda (_.1) (_.0 (inl _.1))))))

It took only 403 ms. The proposition is the statement of the Law of

Excluded Middle, in the double-negative translation.

So, programming languages can help in the study of logic.

## Recent comments

11 hours 22 min ago

15 hours 17 min ago

1 day 2 hours ago

1 week 5 days ago

1 week 5 days ago

3 weeks 3 days ago

6 weeks 5 days ago

6 weeks 6 days ago

6 weeks 6 days ago

7 weeks 1 day ago