当我有一个“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
函数和a
parse
函数都是用它编写的(
作语法分析
函数在这里被省略,因为它与问题无关,但实现起来并不重要)。不仅如此,我还说服了打字员
print : RPS -> String
我想要的签名不是假的,并且避免了使用任何部分函数!这就是我喜欢的工作方式。
然而,在工作中,我的大部分代码都在F#中,而不是在Idris中,所以我最终要做的是使用FsCheck通过基于属性的测试来准证明穷举性。这还不算太糟,但是
-
基于属性的测试没有与
StrMap
; 它在另一个组件中。我喜欢尽可能多地将我的不变量与它们所指的搭配起来。
-
如果您添加了一个案例,但忘记了更改案例,那么在遇到失败之前,您可以在构建过程中取得更大进展
StrMap
; 如果你只是坐在那里重新编译,就像我经常做的那样,你会错过它,直到你真正运行测试。
-
我必须使用非穷举函数来实现它,因为类型系统较弱。这混淆了我试图教给同事的东西的清晰性;我一直在努力让他们相信全功能编程的荣耀。
我们刚刚在Haskell启动了一个新项目,我遇到了这样的情况。当然我可以使用快速检查和
fromJust
实施F#战略,这应该没问题。
但我想知道的是:既然Haskell社区和生态系统以F#的社区和生态系统所没有的方式强调了Curry Howard通信,既然最近添加了各种新奇的扩展来支持依赖类型的使用,那么我就不能改为遵循Idris策略吗?有人告诉我,如果我启用了足够多的扩展(并且愿意引入足够多的冗长内容等),我应该能够将我在Idris中编写的任何内容翻译成Haskell,而不会失去类型安全性。我不知道这是不是真的,但如果是真的,我想知道打开什么扩展,编写什么样的代码,以便在Haskell中遵循我的Idris策略。同样值得注意的是:我可以相信我的Idris策略并不是用这种语言实现它的最简单/优雅的方式。
如何将此Idris代码翻译为Haskell以实现
print :: RPS -> String
不调用任何部分函数?
