string - 一边劈头发，一边劈绳子

Question

我尝试在 Idris 中创建一个函数，如下所示:

strSplit : String -> Maybe (Char, String)

这会将字符串“un-cons”到其第一个 Char 和字符串的其余部分，如果为空，则返回 Nothing。

所以我写了这个，但失败了:

strSplit x = case strM of
    StrNil       => Nothing
    StrCons c cd => Just (c, cs)

然后我尝试了这个，有点像Prelude.Strings:

strSplit x with (strM x)
    strSplit ""             | StrNil         = Nothing
    strSplit (strCons c cs) | (StrCons c cs) = Just (c, cs)

编译并运行没有任何问题。

我的问题是，为什么我必须使用 with 规则以这种方式分割字符串，为什么我原来的方法会失败？

注意:抱歉，我目前无法访问解释器，因此还无法在此处写入错误消息。

Answer 1

这里有两个问题。首先，在“case” block 中，参数是 strM 而不是“with” block 中的 strM x，因此您正在检查不同的东西。

不过，还有一个更有趣的问题，那就是如果您尝试修复第一个问题:

strSplit : String -> Maybe (Char, String)
strSplit x = case strM x of
    StrNil       => Nothing
    StrCons c cd => Just (c, cs)

您将得到一个不同的错误(这是来自当前主控，它已重写错误消息):

Type mismatch between
    StrM "" (Type of StrNil)
and
    StrM x (Expected type)

因此，“case”和“with”之间的区别在于，“with”考虑到您正在检查的内容可能会影响左侧的类型和值。在“case”中，匹配 strM x 意味着 x必须 为“”，但“case”可以出现在任何地方，并且不考虑对其他参数类型的影响(计算出适当的值)对此的类型检查规则将是一个相当大的挑战......)。

另一方面，“with”只能出现在顶层:实际上，它所做的是添加另一个顶层事物来匹配，作为顶层，可以影响类型和其他模式的值。

所以，简短的回答是“with”支持依赖模式匹配，但“case”不支持。