基于 Haskell 中的字符串映射证明打印函数的穷举性

Posted 2023-05-08

【中文标题】基于 Haskell 中的字符串映射证明打印函数的穷举性

【英文标题】：Prove exhaustivity of print function based on a string map in Haskell

【发布时间】：2019-05-07 16:51:45

【问题描述】：

当我有一个“枚举”类型时，即一个代数数据类型，其中没有任何案例包含任何其他数据，我通常喜欢将解析器/打印机投影到字符串的映射中，以确保解析器当我更改代码时，打印机保持同步。例如，在伊德里斯：

data RPS = Rock | Paper | Scissors

Eq RPS where
  Rock == Rock = True
  Paper == Paper = True
  Scissors == Scissors = True
  _ == _ = False

StrMap : List (RPS, String)
StrMap =
  [ (Rock, "rock")
  , (Paper, "paper")
  , (Scissors, "scissors")
  ]

我可能会实现一个打印功能如下：

print' : RPS -> Maybe String
print' rps = lookup rps StrMap

问题是，我不想要 Maybe 这里。我想在编译时保证我已经涵盖了我的所有案例，就像我可以通过在RPS 上的大小写拆分来编写这个函数一样，其中穷举检查器将启动并且我可以只拥有@987654325 @。在 Idris 中，我知道如何通过证明来恢复这一点（你不只是喜欢 Idris！）：

print_exhaustive : (rps : RPS) -> IsJust (print' rps)
print_exhaustive Rock = ItIsJust
print_exhaustive Paper = ItIsJust
print_exhaustive Scissors = ItIsJust

justGetIt : (m : Maybe a) -> IsJust m -> a
justGetIt (Just y) ItIsJust = y

print : RPS -> String
print rps with (isItJust (print' rps))
  | Yes itIs = justGetIt (print' rps) itIs
  | No itsNot = absurd $ itsNot $ print_exhaustive rps

现在在我看来这太棒了。我可以在我的代码中的一个地方声明枚举大小写与其关联字符串之间的相关性是什么，并且我可以有一个print 函数和一个parse 函数都用它编写（parse 函数此处省略，因为与问题无关，但实施起来很简单）。不仅如此，我还能够让类型检查器相信我想要的 print : RPS -> String 签名不是伪造的，并且避免使用任何偏函数！这就是我喜欢的工作方式。

但是，在工作中，我的大部分代码都在 F# 中，而不是在 Idris 中，所以我最终要做的是使用 FsCheck 通过基于属性的测试来准证明穷举性。这还不算太糟糕，但是

基于属性的测试未与StrMap 搭配使用；它在不同的程序集中。我喜欢尽可能将我的不变量与它们所指的内容搭配在一起。 在遇到失败之前，您可以在构建过程中走得更远，例如：添加了一个案例，忘记更改StrMap；如果您只是坐在那里重新编译，就像我经常做的那样，您会错过它，直到您真正运行测试。 由于类型系统较弱，我必须使用非详尽的函数来实现它。这使我试图教给我的同事的东西变得模糊不清；我一直在努力让他们相信全函数式编程的荣耀。

我们刚刚在 Haskell 中启动了一个新项目，我遇到了这样的场景。当然我可以使用 QuickCheck 和fromJust 并实现 F# 策略，应该没问题。

但我想知道的是：由于 Haskell 社区和生态系统以 F# 社区和生态系统所没有的方式强调 Curry-Howard 对应关系，并且由于最近几天添加了各种花哨的扩展来启用使用依赖类型，我不应该为此遵循我的 Idris 策略吗？有人告诉我，如果我打开了足够多的扩展（并且愿意引入足够的冗长等），我应该能够将我可以在 Idris 中编写的任何内容翻译成 Haskell，而不会失去类型安全性。我不知道这是否属实，但如果是真的，我想知道要打开哪些扩展，以及编写什么样的代码，以便在 Haskell 中遵循我的 Idris 策略。另外值得注意的是：我可以相信我的 Idris 策略不是用那种语言最简单/优雅的方式。

如何将这个 Idris 代码翻译成 Haskell，以便在不调用任何部分函数的情况下实现 print :: RPS -> String？

【问题讨论】：

对于低技术的解决方案，您愿意相信派生的Enum 和Bounded 实例用于枚举类型吗？因为如果是，您可以将print 写为直接函数，对于parse，使用可以通过[ (a, print a) | a <- [minBound..maxBound] ] 构建的地图

@cactus 嗯，没想到。我以前听说过这些类型类，但从未使用过它们（我写的主要是 F# 和 Idris，没有那么多 Haskell，而且 Idris 还没有 deriving，等等......）所以他们在我的雷达上并不多。是否愿意将其充实为完整的答案？

我认为您可以使用一些 TH 生成 Show 和 Read 实例（或仅打印和解析函数）。这不是一个理想的解决方案，但它也可以与枚举以外的东西一起使用。

@n.m.我已经阅读了有关可逆语法描述的论文，实际上能够在 F# 中实现足够多的内容，以在 CLI 参数和代数数据类型之间生成解析器/打印机。他们确实使用了 Template Haskell。不过，我对 Template Haskell 知之甚少。我的 F# 版本的样板比他们的多。

@n.m.然而，这确实需要的不仅仅是模板 Haskell：它们需要伴随的类型类、语法代数等。枚举是退化的情况，但它更容易。

【参考方案1】：

如果您愿意为您的枚举类型信任派生的 Enum 和 Bounded 实例，那么这为您提供了一种使用 [minBound..maxBound] 枚举“RPS Universe”的方法.这意味着您可以开始从一个总函数 print :: RPS -> String，并将其制成表格以从中计算 parse：

print :: RPS -> String

parse :: String -> Maybe RPS
parse = \s -> lookup s tab
  where 
    tab = [(print x, x) | x <- [minBound..maxBound]]

【讨论】：

不同的攻击方式，但据我所知，实现了相同的目标。将不得不尝试一下。谢谢！

终于有机会试用了，看起来效果不错。我不会接受答案，因为即使它解决了我的问题，我仍然对 Haskell 中更直接提出的定理证明问题感兴趣。但是我做了 +1，我很欣赏惯用的 Haskell 方法（使这个定理证明的特殊示例变得不那么有趣）。