好吧，所以我意识到我可能会后悔一辈子，但是......精灵实际上是如何工作的？
该文档说它使用了一种算法，该算法是"LJ的扩展"，并指向一篇关于LJT的冗长令人困惑的论文。据我所知，这是一个高度形式化规则的大型复杂系统，用于弄清楚哪些逻辑陈述是真的或错误的。但这甚至没有开始解释如何将类型签名转换为可执行表达式。大概所有复杂的形式推理都以某种方式涉及，但情况至关重要。
这有点像我尝试用BASIC编写Pascal解释器的时候。（别笑！我只有十二岁...我花了几个小时试图弄清楚，最后我不得不放弃。我只是想不通你是如何从一个包含整个程序的巨大字符串中得到的，到你可以与已知的程序片段进行比较以决定实际做什么的东西。
答案当然是你需要写一个叫做"解析器"的东西。一旦你理解了这是什么以及它做了什么，突然间一切都变得显而易见。哦，编写代码仍然不是一件容易的事，但想法很简单。你只需要编写实际的代码。如果我在十二岁时就知道解析器，那么也许我就不会花两个小时盯着空白屏幕。
我怀疑 Djinn 正在做的事情从根本上很简单，但我错过了一些重要的细节来解释所有这些复杂的逻辑体操与 Haskell 源代码的关系......
Djinn 是一个定理证明者。 看来你的问题是：定理证明与编程有什么关系？
强类型编程与逻辑有着非常密切的关系。 特别是，ML传统中的传统函数式语言与直觉主义命题逻辑密切相关。
口号是"程序是证明，程序证明的命题是它的类型"。
一般来说你可以想到
foo :: Foo
就像说foo是公式Foo的证明. 例如类型
a -> b
对应于从a到b的函数，所以如果你有a证明和a -> b证明，你就有b证明。 因此，函数完全符合逻辑中的蕴涵。 同样地
(a,b)
对应于合取（逻辑和）。因此，逻辑重言式a -> b -> a & b对应于Haskell类型a -> b -> (a,b)并有证据：
a b -> (a,b)
这是"和引入规则"而，fst :: (a,b) -> a和snd :: (a,b) -> b对应2"和淘汰规则"
同样，a OR b对应于Haskell类型Either a b。
对应"，以哈斯克尔·库里和威廉·阿尔文·霍华德的名字命名
这个故事因哈斯克尔的非整体性而变得复杂。
Djinn"只是"一个定理证明者。
如果你有兴趣尝试编写克隆，谷歌搜索结果"简单定理证明器"的第一页有这篇论文，描述了为LK编写一个似乎是用SML编写的定理证明器。
编辑：至于"定理如何证明可能？ 答案是，从某种意义上说，这并不难。 这只是一个搜索问题：
考虑这个问题重述为：我们有一组我们知道如何证明S的命题，以及一个我们想要证明P的命题。 我们该怎么办？首先，我们问：我们已经在 S 中有了 P 的证明吗？ 如果是这样，我们可以使用它，如果不是，我们可以在 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)
如果这些都不起作用
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)
实定理证明者有一些智慧，但想法是一样的。 "决策程序"的研究领域考察了寻找某些保证有效的公式证明的策略。 另一方面，"策略"着眼于如何对证明搜索进行最佳排序。
至于："如何将证明翻译成哈斯克尔？
形式系统中的每条推理规则都对应着一些简单的Haskell构造，所以如果你有一个推理规则树，你可以构造一个对应的程序——Haskell毕竟是一种证明语言。
含义介绍：
s -> ?
或介绍
Left
Right
和介绍
a b -> (a,b)
和消除
fst
snd
等
奥古斯特斯在他的回答中说，他们在 Djinn 中实现这一点的方式对于 SO 答案来说有点乏味。 不过我敢打赌，你可以自己弄清楚如何实现它。
在最一般的术语中，根据库里-霍华德同构，类型和命题之间以及值和证明之间存在对应关系。 Djinn使用这种通信。
更具体一点，说你想找到一个(a, b) -> (b, a)类型的Haskell术语。 首先，您将类型转换为逻辑中的语句（Djinn使用命题逻辑，即没有量词）。 逻辑语句(A and B) is true implies (B and A) is true. 下一步是证明这一点。 对于命题逻辑，总是可以机械地证明或反驳一个陈述。 如果我们能反驳它，那么这意味着在（终止）哈斯克尔中不可能有相应的术语。 如果我们能证明它，那么就有一个这种类型的Haskell项，此外，Haskell项与证明具有完全相同的结构。
最后一句话必须是限定的。 您可以选择使用不同的公理和推理规则集来证明语句。 如果你选择一个建设性的逻辑，证明和Haskell项之间只有对应关系。 "正常"，即经典逻辑将A or (not A)之类的东西作为公理。 这对应于Haskell类型Either a (a -> Void)，但是没有这种类型的Haskell项，所以我们不能使用经典逻辑。任何命题陈述都可以在建构命题逻辑中被证明或反驳，这仍然是事实，但它比经典逻辑要复杂得多。
因此，回顾一下，Djinn的工作原理是将类型转换为逻辑中的命题，然后使用构造逻辑的决策过程来证明命题（如果可能的话），最后将证明翻译回Haskell术语。
（在这里说明这是如何工作的太痛苦了，但是给我10分钟的白板，你会很清楚。
作为最后的评论供您思考：如果您有 Scheme 的call/cc，则可以实施Either a (a -> Void)。 选择一个更具体的类型，如Either a (a -> Int)并弄清楚如何。
也许我看错了。也许所有这些形式逻辑的东西只是分散注意力。与其盯着LJT的演绎规则或其他什么，也许我应该做的是看哈斯克尔。
哈斯克尔有6种可能的表达方式？每个人都对它使用的变量施加了不同的类型约束，对吧？所以，也许我只是为函数类型中的每个参数生成一个新变量，然后开始查看我可以构造的表达式。
这甚至不像你必须在暴力搜索中生成所有可能的表达式。如果所有参数都没有函数类型，则尝试函数应用程序是没有意义的。如果所有参数都是多态类型变量，则case表达式对您没有帮助。等等。可用的类型告诉您哪种类型的表达式可能有效。
如果您允许代码调用现有的顶级函数，事情会变得更加有趣。除了多态类型的有趣范围问题之外，还有一个问题是弄清楚哪些函数会或不会帮助你。
显然，我将不得不离开并考虑一段时间......