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

Question

当我有一个"enum“类型，即没有任何情况包装任何其他数据的代数数据类型时，我通常喜欢将解析器/打印机从映射映射到字符串，以确保解析器和打印机在我更改代码时保持同步。例如，在Idris：

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上用案例拆分编写了这个函数一样，在这个函数中，穷竭性检查器会启动，而我只需要print : RPS -> string。在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来使用基于属性的测试来证明其耗尽性。还不算太糟，但是

1. 基于属性的测试不是与StrMap配置的；它位于不同的程序集中。我喜欢把我的不变量和它们所指的搭配起来。
2. 如果您添加了一个案例并忘记了更改StrMap，那么您可以在构建过程中更进一步，然后遇到一个失败；如果您只是坐在那里重新编译，就像我经常做的那样，您可能会错过它，直到实际运行测试为止。
3. 由于系统类型较弱，我不得不使用非详尽的函数来实现它.这使我试图教同事的东西变得模糊不清；我一直试图让他们相信全函数式编程的荣耀。

我们刚刚在Haskell启动了一个新项目，我遇到了这样的情况。当然，我可以使用QuickCheck和fromJust并实现F#策略，这应该很好。

但我想知道的是:既然Haskell社区和生态系统以F#的社区和生态系统所没有的方式强调Curry-Howard之间的对应关系，而且由于最近几天添加了各种花哨的扩展来支持依赖类型的使用，难道我不应该为此遵循我的Idris策略吗？有人告诉我，如果我打开了足够多的扩展(并且愿意引入足够多的扩展等等)，我应该能够将Idris中的任何东西翻译成Haskell，而不会放松类型安全性。我不知道这是否是真的，但如果是真的，我想知道打开哪些扩展，以及编写什么样的代码，以便遵循我在Haskell中的Idris策略。同样值得注意的是:我可以相信，我的Idris策略并不是用这种语言最简单、最优雅的方式。

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

Answer 1

如果您愿意信任派生的Enum和Bounded实例作为枚举类型，那么就可以使用[minBound..maxBound]枚举您的"RPS宇宙“。这意味着您可以从一个总函数print :: RPS -> String开始，并将其表化以计算parse：

print :: RPS -> String

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