如何从类型中重构Haskell表达式

Question

我正在编写一个程序，为给定的类型签名重构Haskell表达式，例如：对于a -> b -> a，它将返回\x -> \_ -> x。我已经阅读了这个问题背后的理论，并且我知道有这个Howard-Curry同构。我想象我的程序会解析输入并将其表示为术语。然后我会触发SLD-resolution，它会告诉我是否可以构造给定类型的术语（对于Pierce的情况是不可能的）。我还不知道如何在这个解析过程中实际创建Haskell表达式。我看过djinn的代码，但它有点复杂，我想掌握一些关于如何工作的一般性思路。

- k_wisniewski

---

在人们投票关闭之前，请注意，理解Dijnn的概念非常具体，而Dijnn的作者经常访问SO（可能不是其他更合适的网站）。 - Thomas M. DuBuisson

你想构建实际的Haskell值还是可以打印出来的语法树？如果是后者，只需为表达式定义一个类型。最少包括变量、抽象、应用。SLD解析不是获取计算内容的简单方法。你需要一个直觉逻辑的证明过程。 - augustss

@augustss - 在基本情况下，我可以只打印生成的函数，但如果这不会增加太多复杂性，那么能够生成实际的Haskell值将是很好的。除了SLD-resolution之外，您推荐什么程序？我以前没有处理过直觉逻辑，我知道的唯一一件事就是我刚在维基百科上读到的:)我看到您在Djinn中使用了一些称为LJT的东西-您能概述一下它的工作原理以及为什么这是更好的选择（如果是的话）吗？ - k_wisniewski

也许可以看看Djinn，并就您不理解的具体问题或其结构提出一些一般性问题。 - misterbee

可能是如何使用Djinn？的重复问题。 - SamB

Answer 1

如果你使用Curry-Howard将Haskell的一个子集连接到某个直觉逻辑上，那么从证明项中提取Haskell程序应该非常容易。实际上，证明项应该已经具有与Haskell程序完全相同的结构，只是使用不同的构造函数名称。如果你在脑海中适当地翻译构造函数名称，甚至可以为证明项和Haskell项使用相同的代数数据类型。例如：

type Name = String

data Type                  -- aka. Formula
  = Function Type Type     -- aka. Implication
  | TypeVar Name           -- aka. PropositionalVar

data Term                  -- aka. Proof
  = Lambda Name Type Term  -- aka. ImplicationIntroduction
  | Apply Term Term        -- aka. ImplicationElimination
  | TermVar Name           -- aka. Start / Identity / Axiom / Copy

你需要在作用域内使用变量上下文（也称为你可以假定的假设）。

type TypingContext = Map Name Type -- aka. Hypotheses

有了这样的类型，您只需编写一个函数：

termOf :: Type -> TypingContext -> Maybe Term

但是作为第一步，最好先编写反函数作为练习：

typeOf :: Term -> TypingContext -> Maybe Type

这两个函数的基本结构应该是相似的：在你拥有的东西上进行模式匹配，确定适用的类型规则（也称证明规则），递归调用自己以构造部分结果，通过包装对应于类型规则（也称证明规则）的构造函数来完成部分结果。一个区别是typeOf可以遍历整个术语并找出所有内容，而termOf可能需要猜测并回溯，如果猜测不成功。因此，你实际上可能想要使用termOf的列表单子句。

编写typeOf的好处是：

1. 它应该更容易，因为术语往往包含比类型更多的信息，所以termOf可以利用那些额外的信息，而typeOf需要创建那些额外的信息。
2. 有更多的帮助可用，因为许多人将typeOf作为练习实现，但很少有人将termOf作为练习实现。

- Toxaris