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...
See Question&Answers more detail:os