Take the 2-minute tour ×

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

share|improve this question
The rest of your life?! It's not so bad, is it? D: –  BoltClock Apr 18 '12 at 21:12
It's finding proofs for the theorems that the types represent. Any program with the correct type is an example. So, thanks to Curry-Howard, you can adopt proof search tactics from theorem proving to instead hunt for programs of a given type. –  Don Stewart Apr 18 '12 at 21:13
@DonStewart: I can kind of see how a type is a theorem and a program is a proof. I can sort of see how you can compare a proof against LJ to see if the proof is valid. What I don't get is how you search for a proof if you don't already have one - i.e., how you can generate a proof from nothing. –  MathematicalOrchid Apr 19 '12 at 8:36

3 Answers 3

up vote 25 down vote accepted

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


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


And introduction

\a b -> (a,b)

And elimination



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.

share|improve this answer
I sort-of comprehend CHI. My real question is "if I have a chain of reasoning that proves my type theorem, how do I translate that into executable code?" And also "how is automatic theorem proving physically possible?" Perhaps the paper you mention will explain the latter... I'll get back to you when I've read it. –  MathematicalOrchid Apr 19 '12 at 8:52
@MathematicalOrchid, but, according to CHI, a chain of reasoning is executable code! –  Rotsor Apr 19 '12 at 10:06
+1 for an interesting paper, even if it hasn't actually answered my main question yet. –  MathematicalOrchid Apr 19 '12 at 10:49
The paper didn't completely answer the question, but it gave me some of the key insights, so I'm accepting this answer. –  MathematicalOrchid Apr 20 '12 at 8:52

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.

share|improve this answer
"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." Because Peirce is equivalent to LEM? –  SCombinator Apr 12 '13 at 5:43
Secondly, how do you show that "any propositional statement can be proven or disproven in constructive propositional logic"? –  SCombinator Apr 12 '13 at 5:45
Yes, Peirce's Law is equivalent to LEM, but the constructive proof of this is also interesting. –  augustss Apr 20 '13 at 10:03
The meta-theorem that any propositional statement is decidable was proven by logicians long ago. Sorry, I have no reference right now. –  augustss Apr 20 '13 at 10:05

Perhaps I'm looking at this all wrong. Perhaps all this formal logic stuff is just a distraction. Rather than staring at the deduction rules for LJT or whatever, maybe the thing I should be doing is looking at Haskell.

There are, what, 6 possible kinds of expression in Haskell? And each one places different type constraints on the variables it uses, right? So, maybe I just generate one new variable for each argument in the function's type, and start seeing what expressions I can construct.

It's not even like you have to generate all possible expressions in a brute-force search. If none of your arguments have function types, there's no point trying function applications. If all of your arguments are polymorphic type variables, case expressions aren't going to help you. And so on. The types available tell you which sorts of expressions might work.

Things get a bit more interesting if you're allowing your code to call existing top-level functions. Aside from the amusing scoping problems with polymorphic types, there's the question of figuring out which functions will or won't help you.

Clearly I will have to go away and think about this for a while...

share|improve this answer
You can certainly do it this way. You have to be a bit careful if you want to make sure your search terminates. Both for the case when there is an term and for the case when there isn't one. For instance (a->a)->a->a has infinitely many (different) ways of of constructing a term with this type. –  augustss Apr 19 '12 at 12:59
Yeah, clearly some types have no implementation, and others have infinity. I'd want some way to control how much searching to do. (Although I haven't yet worked out where the chioces come in... I'm sure I will.) –  MathematicalOrchid Apr 19 '12 at 19:18
And doing it that way isn't really any different from theorem proving. The reason I used a theorem prover in Djinn was that I knew there were sound and complete theorem provers for constructive logic, so I didn't have to ivent a new one. –  augustss Apr 19 '12 at 22:38

Your Answer


