haskell - 如何从类型重建 Haskell 表达式

Question

我正在编写一个程序，对于给定的类型签名重建这种类型的 Haskell 表达式，例如:对于 a -> b -> a它返回 \x -> \_ -> x .我已经阅读了这个问题背后的理论，并且我知道存在这种 Howard-Curry 同构。我想象我的程序可以解析输入并将其表示为术语。然后我会触发 SLD 解析，它会告诉我是否可以构造给定类型的术语(例如，对于 Pierce 来说，这是不可能的)。我还不知道如何在此解决方案期间实际创建 Haskell 表达式。我看过 djinn 的代码，但它有点复杂，我想大致了解它是如何工作的。

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 的列表单子(monad)。 .

写作的好处typeOf首先是:

它应该更容易，因为术语往往包含比类型更多的信息，所以 termOf可以在 typeOf 时使用该额外信息需要创建额外的信息。

有更多帮助可用，因为许多人实现 typeOf作为练习，但很少有人实现termOf作为练习。