Why are recursive pattern synonyms accepted?

Question

This question (from 5 years ago) asks 'Why are all recursive pattern synonyms rejected?' and its example is still rejected. The User Guide says "Pattern synonyms cannot be defined recursively."

I have a recursive pattern synonym that's accepted (GHC 8.10.2). I can call it, and it loops -- no surprise. So why does it compile?/Is there a plausible use-case for something like this?

Code based on an example in Section 2.3 'Polymorphic pattern synonyms' of the 2016 paper.

data JoinList a = JNil | Unit a | JoinList a `JoinTree` JoinList a    deriving (Eq, Read, Show)

I'm trying to define a pattern synonym Nil. Obviously JNil is a match. But also JNil ``JoinTree`` JNil, and any arbitrary nestings of JoinTree providing all the leafs are JNil.

pattern Nil :: JoinList a
pattern Nil <- JNil
  where Nil = Nil `JoinTree` Nil      -- huh?

wot = Nil `JoinTree` Nil              -- these all compile
wotwot Nil = ()
wotwotwot = wotwot Nil
wotwotwotwot = wotwot wot

Trying to call wot loops, no surprise. Trying to call wotwotwot complains Non-exhaustive patterns in function wotwot.

Full disclosure: what I was playing with/I know this doesn't work [see also below] is:

pattern Nil = JNil                     -- base case matcher, and builder
  where Nil <- Nil `JoinTree` Nil      -- recursion on the matcher, not the builder
                                       -- but can't put `<-` equations after where

The following rejected Recursive pattern synonym definition -- which is what I expect

pattern NilRec <- NilRec `JoinTree` NilRec 
  where NilRec = JNil

And anyway that wouldn't work: it needs to match NilRec = JNil first as the base case.

To answer @Noughtmare's q "how would you suggest ..." comment to his answer, I'd like to write the decl per above 'what I was playing with' (yes I know that's currently illegal syntax); and get that desugarred to a matcher with two cases, tried sequentially:

case arg of
  { JNil -> ...
  ; Nil `JoinTree` Nil -> ...
  }

Note each of those cases has outermost a data constructor from type JoinList. So the recursive use of Nil is guarded/intermediated, as would be any approach via a ViewPattern. (Which is what the q 5 years ago was asking.) Put it another way: I think the compiler could generate a ViewPattern from the pattern ... = ... where ... <- ....

Note that the `pattern ... <- ... where ... = ...` notation defines the matcher (with the arrow) and the builder (with the equality sign) separately, it is not a base case recursive case split as you seem to suggest. — Noughtmare, Jul 24 '21 at 10:35
"get that desugared to a matcher with two cases" -- but your proposed desugaring still contains sugar! — Daniel Wagner, Jul 24 '21 at 15:01
@Daniel "your [my] proposed desugaring" I've made a stab at here https://gitlab.haskell.org/ghc/ghc/-/issues/12203#note_366851 — AntC, Jul 26 '21 at 07:00

Noughtmare · Answer 1 · 2021-07-24T10:44:50.263

4

Only the matcher cannot be recursive, because that could lead to infinite pattern matching (infinitely large programs). The desugaring of case x of Nil -> y would be:

  case x of
    JNil -> y
    JoinTree x2 x3 -> case x2 of
      JNil -> case x3 of
        JNil -> y
      JoinTree x4 x5 -> case x4 of
        ...

Going on infinitely.

Having a recursive builder is fine, because they can contain arbitrary functions. Here is perhaps a simpler example that shows this without the confusion of constructors:

pattern Foo <- ()
  where Foo = let loop = loop in loop

You can allow arbitrary functions in patterns by using ViewPatterns:

normJoinList (JoinTree (normJoinList -> JNil) (normJoinList -> JNil)) = JNil
normJoinList x = x

pattern Nil <- (normJoinList -> JNil)
  where Nil = JNil

I think that does what you want:

> case Nil `JoinTree` Nil of Nil -> True; _ -> False
True

edited Jul 24 '21 at 10:44

answered Jul 24 '21 at 10:15

Noughtmare

9,410
1
12
38

Thanks, the paper already has a solution using `ViewPattern`s. I hate them. I'm trying to avoid them. – AntC Jul 24 '21 at 10:24
@AntC I have added an example of how the desugaring would be infinitely long. How would you suggest to avoid that without using a recursive function (which requires `ViewPatterns`)? – Noughtmare Jul 24 '21 at 10:49
I guess one could imagine something like `let f ts x0 = case x0 of { JNil -> g 0 ts; JoinTree x1 x2 -> f (x2:ts) x1 }; g n [] = z; g n (t:ts) = h n t (g (n+1) ts); h 0 JNil k = k; h n (JoinTree x0 x1) = h (n-1) x0 (h (n-1) x1 k); h _ _ k = z in f [] x` (where `z` is the term that does the rest of the matches in the original case). Intuition: `f` checks if its argument is a perfectly balanced tree of `JNil`s of any depth; `g` checks if its argument is a list of perfectly balanced trees of increasing depth; `h` checks if its argument is a perfectly balanced tree of a given depth. – Daniel Wagner Jul 24 '21 at 15:29
Do note that the actual implementation of pattern synonyms *would* handle recursive matching just fine (presumably with a little fiddling). It's just that no one bothered to specify it properly and relied on a desugaring which can't quite handle it. ``pattern Nil <- JNil; pattern Nil <- Nil `JoinTree` Nil``, if it worked, should produce ``matchNil :: forall rep (r :: TYPE rep) a. JoinList a -> (Void# -> r) -> (Void# -> r) -> r; matchNil JNil y n = y void#; matchNil (l `JoinTree` r) y n = matchNil l (\_ -> matchNil r y n) n; matchNil _ y n = n void#``. – HTNW Jul 24 '21 at 17:44

Why are recursive pattern synonyms accepted?

1 Answers1