string - 分裂头发，同时分裂字符串

Question

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

strSplit : String -> Maybe (Char, String)

这会将字符串“取消”到它的第一个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规则以这种方式拆分字符串，为什么我的原始方法会失败？

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

score 4 · Accepted Answer

这里有两个问题。首先，在“case”块中，参数与“with”块中的参数strM不同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”不支持。

1 回答 1