如何从类型重建 Haskell 表达式

Posted 2023-05-08

【中文标题】如何从类型重建 Haskell 表达式

【英文标题】：How to reconstruct Haskell expression from type

【发布时间】：2013-09-12 08:51:51

【问题描述】：

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

【问题讨论】：

在人们投票结束之前，请注意理解 Dijnn 的概念是非常具体的，并且 Dijnn 的作者经常光顾 SO（并且可能不是其他更合适的网站）。

是的，它似乎是一个广为人知的解决这个问题的程序，但我不想复制原作者写的东西，而是想了解它是如何工作的以及为什么。它可能包含一些优化，但为了理解它们的重要性，我需要有一个大致的概念。谢谢托马斯；）

从类型构造 Haskell 表达式就像从 MD5 中找到的字符串 - 是一项艰巨的任务然后反转一个

@wit 这比破解加密哈希要容易得多。 Djinn> ? x :: a -> b -> (d -> c) -> (a -> b) -> (b -> b -> d) -> c --> x a b c d e = c (e (d a) b).

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

【参考方案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 用作练习。