如何从类型重建 Haskell 表达式

Question

我正在编写一个程序，对于给定的类型签名重建这种类型的Haskell表达式，例如：对于a -> b -> a它返回x -> _ -> x。我读过这个问题背后的理论，我知道有霍华德-库里同构。我想象我的程序来解析输入并将其表示为术语。然后我会触发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可能不得不猜测和回溯。所以很可能，你真的想要列表 monad 用于termOf.

首先编写typeOf的好处是：

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