feature request: constructor only/wildcard pattern matches

[edwinb]

Issue by MarcelineVQ
Saturday Apr 25, 2020 at 00:09 GMT
Originally opened as edwinb/Idris2-boot#320

---

It would be useful to have a way, in patterns, to check for the presence of a constructor without regard to its arguments.
Currently given

data Tree : Type -> Type where
  Tip : Tree a
  Node : (v : a) -> (l : Tree a) -> (r : Tree a) -> Tree a

in a pattern match in Idris where we don't use the values in Node we would write (Node _ _ _) to match the Node constructor.
In Haskell one can do the same, but can also write Node{}.
(Node _ _ _) and Node{} are equivalent but the latter more strongly expresses a complete disinterest for any information other than that we have a Node.

This is particularly useful for places where you just want to satisfy some NonEmpty property for your value. For example given

data NonEmpty : Tree a -> Type where
  IsNonEmpty : NonEmpty (Node v l r)

maxView : (t : Tree a) -> {auto ok : NonEmpty t} -> (a, Tree a)
maxView (Node v l Tip) = (v,l)
maxView (Node v l r@(Node _ _ _)) =
  let (x,r') = maxView r in (x, Node v l r')

Currently if we want idris to infer a NonEmpty where we need it we might write

case t of
  Tip => ?foo
  n@(Node _ _ _) => maxView n

compared to

case t of
  Tip => ?foo
  n@Node{} => maxView n

and even maxView could make use of this since it also only needs to know that it has a Node, not what the Node contains

maxView (Node v l r@Node{}) =

It doesn't seem like a big addition but these savings add up due to making for more direct code, you are stating just one time to the reader and compiler "I don't make use of Node's values here" instead of stating it once for each field of Node.

edwin mentions on irc:
<edwinb> I thought about that [this feature] a while ago, and the reason I didn't is that, in Haskell, it's consistent with the record syntax, but in Idris there's nothing for it to be consistent with
<edwinb> it might still be a reasonable special case. It is useful.

With that in mind I'd love to hear some syntax suggestions (and opinions) for this feature, e.g. matching a Node without regard to its contents and calling it n could look like:

n@Node{}
n@Node(..)
n@Node()
n@Node#
n&Node

[gallais]

This was fixed by #607. You can now write

nat : Tree a -> Nat
nat Tip = 0
nat (Node{}) = 1

Note the extra parens to indicate {} applies to Node and not nat
as the same notation is used to eagerly introduce all of a function's
arguments (e.g. nat {} = 0 for the constant function).