How does Djinn work?

Question

OK, so I realise that I will probably regret this for the rest of my life, but... How does Djinn actually work?

The documentation says that it uses an algorithm which is "an extension of LJ" and points to a long confusing paper about LJT. As best as I can tell, this is a big complicated system of highly formalised rules for figuring out which logical statements are true or false. But this doesn't even begin to explain how you turn a type signature into an executable expression. Presumably all the complicated formal reasoning is involved somehow, but the picture is crucially incomplete.

---

It's a bit like that time I tried to write a Pascal interpretter in BASIC. (Don't laugh! I was only twelve...) I spent hours trying to figure it out, and in the end I had to give up. I just couldn't figure out how the heck you get from a giant string containing an entire program, to something you can compare against known program fragments in order to decide what to actually do.

The answer, of course, is that you need to write a thing called a "parser". Once you comprehend what this is and what it does, suddenly everything becomes obvious. Oh, it's still not trivial to code it, but the idea is simple. You just have to write the actual code. If I'd known about parsers when I was twelve, then maybe I wouldn't have spent two hours just staring at a blank screen.

I suspect that what Djinn is doing is fundamentally simple, but I'm missing some important detail which explains how all this complicated logical gymnastics relates to Haskell source code...

Answer 1

Djinn is a theorem prover. It seems your question is: what does theorem proving have to do with programming?

Strongly typed programming has a very close relationship to logic. In particular, traditional functional languages in the ML tradition are closely related to Intuitionist Propositional Logic.

The slogan is "programs are proofs, the proposition that a program proves is its type."
In general you can think of

 foo :: Foo 

as saying that foo is a proof of the formula Foo. For example the type

 a -> b   

corresponds to functions from a to b, so if you have a proof of a and a proof of a -> b you have a proof of b. So, function correspond perfectly to implication in logic. Similarly

(a,b) 

Corresponds to conjunction (logic and). So the logic tautology a -> b -> a & b corresponds to the Haskell type a -> b -> (a,b) and has the proof:

\a b -> (a,b) 

this is the "and introduction rule" While, fst :: (a,b) -> a and snd :: (a,b) -> b correspond to the 2 "and elimination rules"

similarly, a OR b corresponds to the Haskell type Either a b.

This correspondence is sometimes referred to as the "Curry-Howard Isomorphism" or "Curry-Howard Correspondence" after Haskell Curry and William Alvin Howard

This story is complicated by non-totality in Haskell.

Djinn is "just" a theorem prover.

If you are interested in trying to write a clone, the first page of google results for "Simple Theorem Prover" has this paper which describes writing a theorem prover for LK that appears to be written in SML.

Edit: as to "how is theorem proving possible?" The answer is that in some sense it isn't hard. It is just a search problem:

Consider the problem restated as this: we have a set of propositions we know how to prove S, and a proposition we want to prove P. What do we do? First of all, we ask: do we already have a proof of P in S? If so, we can use that, if not we can pattern match on P

case P of    (a -> b) -> add a to S, and prove b (-> introduction)    (a ^ b)  -> prove a, then prove b (and introduction)    (a v b)  -> try to prove a, if that doesn't work prove b (or introduction) 

if none of those work

for each conjunction `a ^ b` in S, add a and b to S (and elimination) for each disjunction `a v b` in S, try proving `(a -> P) ^ (b -> P)` (or elimination) for each implication `a -> P` is S, try proving `a` (-> elimination) 

Real theorem provers have some smarts, but the idea is the same. The research area of "Decision Procedures" examines strategy for finding proofs to certain kinds of formula that are guaranteed to work. On the other hand "Tactics" looks at how to optimally order the proof search.

As to: "How can proofs be translated into Haskell?"

Each inference rule in a formal system corresponds to some simple Haskell construct, so if you have a tree of inference rules, you can construct a corresponding program--Haskell is a proof language after all.

Implication introduction:

\s -> ? 

Or introduction

Left Right 

And introduction

\a b -> (a,b) 

And elimination

fst snd 

etc

augustss says in his answer that they way he implemented this in Djinn is a little tedious for an SO answer. I bet though, that you can figure it how to implement it on your own.

Answer 2

In the most general terms, according to the Curry-Howard isomorphism there is a correspondence between types and propositions and also values and proofs. Djinn uses this correspondence.

Do be more concrete, say that you want to find a Haskell term of type (a, b) -> (b, a). First you translate the type to a statement in logic (Djinn uses propositional logic, i.e., no quantifiers). The logic statement goes (A and B) is true implies (B and A) is true. The next step is to prove this. For propositional logic it is always possible to mechanically prove or disprove a statement. If we can disprove it, then that means that there can be no corresponding term in (terminating) Haskell. If we can prove it, then there is a Haskell term of that type, and furthermore, the Haskell term has the exact same structure as the proof.

The last statement has to be qualified. There are different sets of axioms and inference rules you can choose use to prove the statement. There is only a correspondence between the proof and the Haskell term if you pick a constructive logic. The "normal", i.e., classical logic has things like A or (not A) as an axiom. That would correspond to the Haskell type Either a (a -> Void), but there's no Haskell term of this type so we can't use classical logic. It is still true that any propositional statement can be proven or disproven in constructive propositional logic, but it's considerably more involved doing so than in classical logic.

So to recap, Djinn works by translating the type to a proposition in logic, then it uses a decision procedure for constructive logic to prove the proposition (if possible), and finally the proof is translated back to a Haskell term.

(It's too painful to illustrate how this works here, but give me 10 minutes at a white board and it will be crystal clear to you.)

As a final comment for you to ponder: Either a (a -> Void) can be implemented if you have Scheme's call/cc. Pick a more concrete type like Either a (a -> Int) and figure out how.