1

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

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这里。我想保证在编译时我已经涵盖了所有的案例，就像我通过 case-splitting on 编写这个函数一样RPS，穷举检查器将启动并且我可以只拥有print : RPS -> string. 在伊德里斯，我知道如何用证明来恢复它（你不只是爱伊德里斯吗！）：

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 代码转换为 Haskell 以便在print :: RPS -> String不调用任何部分函数的情况下实现？

4

1 回答 1

4

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

print :: RPS -> String

parse :: String -> Maybe RPS
parse = \s -> lookup s tab
  where 
    tab = [(print x, x) | x <- [minBound..maxBound]]
于 2018-12-06T06:03:04.473 回答