13

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

4

1 回答 1

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如果猜测不成功，则可能必须猜测并回溯。所以很可能，你实际上想要 list monad for termOf.

先写的好处typeOf是：

  1. 它应该更容易，因为术语往往包含比类型更多的信息，因此termOf可以在typeOf需要创建额外信息时使用这些额外信息。
  2. 有更多可用的帮助，因为许多人typeOf将其作为练习来实施，但很少有人termOf将其作为练习来实施。
于 2013-09-09T06:46:33.470 回答