Parting hair when separating strands
I tried to make a function in Idris like this:
strSplit : String -> Maybe (Char, String)
This will "un-cons" the string into its first Char
and rest of the string, and return Nothing
if it was empty.
So I wrote this, which failed:
strSplit x = case strM of
StrNil => Nothing
StrCons c cd => Just (c, cs)
So, I tried this, a little like in Prelude.Strings
:
strSplit x with (strM x)
strSplit "" | StrNil = Nothing
strSplit (strCons c cs) | (StrCons c cs) = Just (c, cs)
Compiled and works seamlessly.
My question is, why would I use this rule with
to split the string this way and why my original method doesn't work?
Note. Unfortunately, I cannot access the interpreter at the moment, so I cannot write an error message here.
source to share
There are two problems here. First, the "case" block is the argument strM
, not strM x
like the "c" block, so you are checking different things.
There is an even more interesting problem, which is that if you try to fix the first one:
strSplit : String -> Maybe (Char, String)
strSplit x = case strM x of
StrNil => Nothing
StrCons c cd => Just (c, cs)
You will get another error (this is from the current master who reformulated the error messages):
Type mismatch between
StrM "" (Type of StrNil)
and
StrM x (Expected type)
So the difference between "case" and "c" is that "c" takes into account that the thing you are checking can affect the types and values on the left side. In the "case", matching strM x means that x must be ", but" case "can appear anywhere and does not take into account the effect on the types of other arguments (developing appropriate type checking rules for this would be rather difficult ...).
On the other hand, "c" can only appear at the top level: effectively what it does is add another top-level thing to match on which, being the top-level, can affect the types and values of other templates.
So the short answer is that "c" supports dependent pattern matching, but "case" does not.
source to share