Allow constructors on LHS of (implicit) bidirectional pattern synonym

Inspired by the recent Ghostbuster paper http://www.cs.ox.ac.uk/people/timothy.zakian/ghostbuster.pdf , I was experimenting with using pattern synonyms to simulate GADTs. In the process, I noticed that we should be able to generalize the implicit bidirectional synonyms to allow constructors on the LHS.

Consider this program:

{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE TypeOperators #-}
{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
module GhostBuster where

import GHC.TypeLits

newtype Vec a (n :: Nat) = Vec { unVec :: [a] }

pattern VNil :: Vec a 0
pattern VNil = Vec []

pattern VCons :: a -> Vec a n -> Vec a (n + 1)
pattern VCons x xs <- Vec (x : (Vec -> xs)) where
    VCons x (Vec xs) = Vec (x : xs)

headVec :: Vec a (n + 1) -> a
headVec (VCons x _) = x

In effect, we simulate a vector GADT using pattern synonyms to handle the newtype Vec.

I would like it if I could specify the VCons pattern more simply, as just:

pattern VCons :: a -> Vec a n -> Vec a (n + 1)
pattern VCons x (Vec xs) = Vec (x : xs)

And GHC would infer the correct pattern (the constructor can be read off immediately), automatically replacing occurrences of xs with a view pattern that reconstructs the constructors that were stripped off on the LHS.

Trac metadata

Trac field	Value
Version	8.0.1
Type	FeatureRequest
TypeOfFailure	OtherFailure
Priority	low
Resolution	Unresolved
Component	Compiler (Type checker)
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture

changed weight to 3

added Tfeature request Trac import typechecker labels

Actually, it turns out the example above is not a great one because no type refinement happens with pattern synonym (with good reason!) Here's my actual use case:

newtype D k a = D a

data Stream a = Cons a (Stream a)

newtype StreamK k a = StreamK { unStreamK :: Stream a }

{-
-- Pattern synonyms are to give this "virtual interface"
data StreamK (k :: Clock) a = Cons a (StreamK (D k a))
newtype Stream a = Stream { unStream :: forall k. StreamK k a }
-}

unStream :: Stream a -> (forall k. StreamK k a)
unStream t = StreamK t

pattern Stream :: (forall k. StreamK k a) -> Stream a
pattern Stream t <- (unStream -> t) where
    Stream (StreamK t) = t

pattern ConsK :: a -> D k (StreamK k a) -> StreamK k a
pattern ConsK x xs <- StreamK (Cons x ((UnsafeD . StreamK) -> xs)) where
    ConsK x (UnsafeD (StreamK xs)) = StreamK (Cons x xs)

To get "true" GADTs, you need to unsafeCoerce to something with a GADT, as I have done in this email message: https://mail.haskell.org/pipermail/ghc-devs/2016-June/012284.html (but here you really do need the view pattern.)

Edward and I discussed this. What if we wrote this:

pattern VCons :: a -> Vec a n -> Vec a (n + 1)
pattern VCons x xs = Vec (x : unVec xs)

What makes it OK to use bidirectional "=" is that the RHS is invertible. Constructors are invertible. But so is unVec, because it's inverse is just Vec.

So maybe we should just expand the class of invertible RHSs a little? It would be the first time we'd treated the record selector of a newtype specially, but that might be OK.

Before long someone is going to want to write this

pattern P x xs = coerce (x : coerce xs)

where the coerce does a genuine long-distance coercion eg between [Age] and [Int]. Ha ha.

I don't think this is a great idea. The specification about what can appear on the RHS is currently very simple, it just has to be a pattern. The rules for turning this pattern into an expression are also very simple and rely on the fact that a lot of pattern syntax looks like the corresponding expression.

Allowing this change complicates things, firstly in the parser, Vec (x : unVec xs) is not valid pattern syntax currently. Secondly, the rules for how to perform the inversion require more thought. Looking at Simon's example, I have to think a bit about what should happen.. it seems the corresponding expression should be Vec (x : Vec xs) but I'm still not sure that is right! Perhaps the rule is as simple as replace the function with it's inverse but it seems ad-hoc to me.

I do have other lingering concerns that the way we designed the feature, the most useful constructs are the least supported. I'm referring to the fact that all interesting uses are explicitly bidirectional pattern synonyms which require view patterns. Such definitions tend to be quite noisy to define -- something more like views would have made things cleaner.

Great or not, it's pretty simple. Adding newtype patterns on the left is really quite tricky. It took me 15 mins to grok.

As to the parser, it parses patterns as expressions, and then converts them to patterns. Then the patsyn code converst it back (for bidirectional). So maybe we should leave it as an expression! The rule is still simple: to use it as an expression, just use the exression. To use it as a pattern, just treat unVec e as the view pattern (Vec -> e).

It seems like quite a big change to me to specify the expression rather than the pattern. It also raises questions in the case of explicitly bidirectional pattern synonyms, do you specify two expressions? One which gets actually converted to a pattern and one which actually gets used in expressions? What about for implicitly bidirectional pattern synonyms do we still specify an expression on the RHS?

Still quite tricky with some details to be worked out!

mentioned in issue #13672 (closed)

Another example from #13672 (closed) which requires this functionality:

newtype Tannen f p a b = Tannen { runTannen :: f (p a b) }
newtype Fix p a = In { out :: p (Fix p a) a }

newtype ZipList a = ZL (Fix (Tannen Maybe (,)) a)

pattern Nil :: ZipList a
pattern Nil = ZL (In (Tannen Nothing))

pattern (:::) :: a -> ZipList a -> ZipList a
pattern a:::ZL as = ZL (In (Tannen (Just (as, a))))

Trac metadata

Trac field	Value
Related	- → #13672 (closed)

Use case

data Pair a = a :# a

pattern Pair1 :: Pair a -> (Bool -> a)
pattern Pair1 (a :# a') <- (($ False) &&& ($ True) -> (a, a'))
  where Pair1 (a :# _)  False = a
        Pair1 (_ :# a') True  = a'

added Plow label

Another example: https://stackoverflow.com/questions/65808951/no-fun-puzzlement-with-pattern-synonyms-as-functions

There's a danger here of letting the perfect get in the way of the somewhat-better:

• dream up a load of more-complex examples that weren't in the O.P.;
• conclude it's now too hard; so
• do nothing.

With the simple examples, from the 'underneath' line of the pattern decl, it's blimmin' obvious what's going on. Why can't I write that line alone as a (implicitly) bidirectional synonym and have GHC figure out the constructor-to-pattern mapping, inserting a ViewPattern if it must?

I can see in general the 'underneath' line(s) might be more complex, with guards and arbitrary logic on RHS, possibly even generating different data constructors in different points in the logic. Then don't try to tackle 'invertible' stuff in general.

The characteristic of the simple examples is the underneath line can be seen as injective purely from its syntax:

• a single line with =;
• no guards;
• RHS of the = mentions variables all and only from LHS, plus constructors;
• that is, no function calls on RHS, not even newtype field selectors;
• no record syntax.

IOW what a bidirectional line would look like anyway.

If you'd like to suggest a change to the language, an excellent path is to write a GHC proposal. I've spent 10 mins staring at this ticket and I can't figure out exactly what you are proposing. I think it is something like: liberalise the ways in which you can specify a bidirectional synonym, rather than specifying the two directions separately. But I'm not sure.

Another 20 mins might do it, but even that would only enlighten me. A GHC proposal would solve all that.

Thank you @simonpj

I can't figure out exactly what you are proposing

Then either there's some complexity I don't understand, or some simplicity you're overlooking. Either way, the effort of writing then critiquing a GHC proposal is not an effective way to elucidate. I'll propose if the following makes sense ...

I don't think I can improve on Edward's "Allow constructors on LHS of (implicit) bidirectional pattern synonym" . Note he says 'constructors', not 'invertible functions'. Also I agree with his original StackOverflow post wanting to avoid "an extremely ugly, ViewPatternsed pattern synonym."

In the keep-it-simple examples I can see, what's proposed has the effect of generating a ViewPattern, so the programmer isn't faced with that ugliness.

To take my example first. I write:

data Nat = Zero | Succ Nat       -- not a newtype, more than one constructor
pattern Pred (Succ n) = n        -- constructor on LHS

That pattern equation is to become the 'underneath' line of an explicitly bidirectional pattern decl. From it, the compiler infers

pattern Pred :: Nat -> Nat

The compiler also infers the top line:

pattern Pred n <-  (Succ -> n)          where ...

The semantics to deliver for Pred is such that idPred is identity.

idPred (Pred n) = Pred n

The top line is generated via purely syntactic manipulation: take the constructor from LHS of the 'underneath' equation, insert it on RHS of the top line <-, as a ViewPattern call. No need to call a field selector function, indeed no field selector defined for Succ.

Edward's first example is a little trickier, because of the phantom type for Vec. It'll need a programmer-supplied signature for the pattern. Edward wants to write (copied from his O.P., his Nat is from GHC.TypeNats, not the one I declared above):

   newtype Vec a (n :: Nat) = Vec { unVec :: [a] }
   pattern VCons :: a -> Vec a n -> Vec a (n + 1)
   pattern VCons x (Vec xs) = Vec (x : xs)

The compiler-inferred top line again inserts the LHS constructor from the to-be 'underneath' line as a ViewPattern call, prefixed to whatever var it appeared against on LHS, as Edward shows:

   pattern VCons x xs <- Vec (x : (Vec -> xs)) where ...

I'll work through his other examples as a separate post -- that is, if this makes sense so far.

To reject a couple of the complications up-ticket

It seems like quite a big change to me to specify the expression rather than the pattern. ... What about for implicitly bidirectional pattern synonyms do we still specify an expression on the RHS?

No, no expressions. This only applies if both sides of the (implicitly) bidirectional equation contain only constructors and variables, and the variables all and only appear both sides.

@Icelandjack's use case is too complex -- unless he can figure a way to write it as a single bidirectional line without function calls.

Ah, for @RyanGlScott's example from #13672 (closed), the 'insert ViewPattern call, prefixed to whatever var it appeared against on LHS' rule works a treat. From programmer-supplied bidirectional decl

   pattern a:::ZL as = ZL (In (Tannen (Just (as, a))))

compiler generates

   pattern a:::as   <- ZL (In (Tannen (Just (ZL -> as, a))))
     where a:::ZL as = ZL (In (Tannen (Just (as, a))))

Ah, I see what's gone wrong with Edward's second post. He's thrown a spanner in the works by trying to use a field selector function in the ViewPattern. No, this needs only constructors, and for that reason we don't care if there are field labels. I'll rework it.

   newtype D k a = D a

   data Stream a = Cons a (Stream a)

   newtype StreamK k a = StreamK { unStreamK :: Stream a }

   -- unStream :: Stream a -> (forall k. StreamK k a)    -- not needed
   -- unStream t = StreamK t

Pattern 1: Programmer supplies a bidirectional equation, plus the signature below to handle the phantom

pattern Stream (StreamK t) = t

   pattern Stream :: (forall k. StreamK k a) -> Stream a
   pattern Stream t <- (unStream -> t) where               -- wrong
       Stream (StreamK t) = t

Edit: Now, although we don't need unStream, we do need its signature for the phantom. I'm putting it as an annotation. Compiler to generate

pattern Stream t <- ((StreamK :: Stream a' -> (forall k. StreamK k a')) -> t) where
    Stream (StreamK t) = t

Pattern 2: Programmer supplies a bidirectional equation, plus the signature below to handle the phantom, and Edward got the right ViewPattern to generate

pattern ConsK x (UnsafeD (StreamK xs)) = StreamK (Cons x xs)

   pattern ConsK :: a -> D k (StreamK k a) -> StreamK k a
   pattern ConsK x xs <- StreamK (Cons x ((UnsafeD . StreamK) -> xs)) where
       ConsK x (UnsafeD (StreamK xs)) = StreamK (Cons x xs)

Perhaps would be clearer to use a lambda expr as the ViewPattern? Edward's code is the eta-reduced form

pattern ConsK x xs <- StreamK (Cons x ((\xs' -> (UnsafeD (StreamK xs'))) -> xs)) where ...

Caveat: Edward doesn't reveal what is UnsafeD. I've presumed

pattern UnsafeD a = D a

Trickier example here, not using constructors.

I can avoid the ViewPattern using a LambdaCase

(\case p@Positive | p>0 -> p) 

But syntax like that isn't allowed within patterns

pattern Positive <- ((>0) -> True)  where
  p@Positive | p>0 = p

-- * pattern synonym 'where' clause must contain a single binding:

(Hmm that is a single binding: it's an as-pattern, not binding vars additional to the pattern.)

I'm exploring a hypothesis that by liberalising the LHS of PatternSynonyms, which can see both sides of the equation, you can express the mapping without ViewPatterns.

Thanks for the explanations. It's clearer to me now.

In a pattern synonym

pattern P :: t1 -> t2 -> t3
pattern P x y <- pat

we generate a "matcher" like this (see the pattern synonym paper Section 7):

$mP :: t3 -> (t2 -> t2 -> r) -> r -> r
$mP s cont fail
  = case s of
      pat -> cont x y
      _   -> fail

The idea is that the matcher matches the scrutinee s against the pattern pat (the RHS of the pattern synonym). If the match succeeds, the variables it binds (here x and y) are passed to the continuation cont; if not, we call fail.

---

In the extension proposed here, I believe the idea is to allow patterns on the lhs of the pattern synonym, thus:

pattern P :: t1 -> t2 -> t3
pattern P pat1 pat2 <- pat3

I think that we simply adjust the matcher like this:

$mP :: t3 -> (t1 -> t2 -> r) -> r -> r
$mP s cont fail
  = case s of
      pat3 -> cont pat1 pat2
      _   -> fail

Easy! Here we are using pat1 and pat2 as expressions, which we pass to cont. But that's fine; we already convert the RHS pattern to an expression in bidirectional synonyms.

---

We'd have to adjust the definition of matching for pattern synonyms in the user manual, thus:

If the pattern is a constructor pattern (P p1 ... pn), where P is a pattern synonym defined by P q1 ... qn = q or P q1 ... qn <- q, where the qi are patterns, then:

• Match the value v against q. If this match fails or diverges, so does the whole (pattern synonym) match. Otherwise the match against p must bind variables x1 ... xn to values v1 ... vn. These variables xi may be mentioned in the patterns qi.
• Define substitution S to map x1 :-> v1 ... xn :-> xn.
• Match S(q1) against p1, S(v2) against p2 and so on. If any of these matches fail or diverge, so does the whole match.
• If all the matches against the pi succeed, the match succeeds, binding the variables bound by the pi . (The xi are not bound; they remain local to the pattern synonym declaration.)

---

That does indeed all look quite plausible, and the above gets pretty close to a decent specfication.

In an example like

data Nat = Zero | Succ Nat       -- not a newtype, more than one constructor
pattern Pred (Succ n) = n        -- constructor on LHS

the builder is partial -- it does not cover all cases. That is a call of Pred like

f x = Pred (Pred x)

might fail with a pattern-match failure. E.g. f Zero or f (Succ Zero) would both fail. Is what you intend? Presumaly you'd expect a warning from the pattern synonym definition?

---

I have not worked out the consequences for GADTs etc. It might be fiddly but I doubt there'd be a problem.

Extending this thought to definitions with multiple matcher lines:

pattern P :: t1 -> t2 -> t3
pattern { P pat1 pat2 <- pat3             -- first line could have `=` instead of `<-`
        ; P pat4 pat5 <- pat6
        }
  where ...

@simonpj I think that we simply adjust the matcher like this:

$mP :: t3 -> (t1 -> t2 -> r) -> r -> r
$mP s cont fail
  = case s of
      pat3 -> cont pat1 pat2
      pat6 -> cont pat4 pat5              -- extra to Simon's spec
      _    -> fail

(I'm being careful to quote the "simply" -- I'm not in a position to judge how simple.)

The types work out. I'm worried about the free vars in the patterns, and their bindings. We stipulate

fv(pat1) U fv(pat2) ≤ fv(pat3)
fv(pat4) U fv(pat5) ≤ fv(pat6)

But don't require fv(pat3) = fv(pat6). Does that cause trouble when calling cont?

Example adapted from the "(sic) extension" 1996 discussion ref'd from the 2016 paper:

pattern Last :: a -> [a]
pattern { Last x <- [x]
        ; Last x <- (_hd: Last x)
        }

$mLast s cont fail
  = case s of
      [x]           -> cont x
      (_hd: (\xs -> $mLast xs id fail) -> x) -> cont x
{- or? -}
      (_hd: xs)     -> $mLast xs cont fail
      _             -> fail

(There's plenty of examples in that discussion of multi-equation matchers, including Wadler's beloved Snoc/backwards access to a List. I've got a queasy feeling there's something not "Easy!" here, or it would have been included in the 2016 extension.)

Wadler's beloved Snoc/backwards access to a List.

The (proposed) pattern definition seems too easy:

pattern Snoc :: [a] -> a -> [a]
pattern Snoc []     x = [x]
        Snoc (y:ys) x = y: Snoc ys x
        Snoc []     (error "Snoc pattern match failure on empty list") <- []

Using:

• A data constructor [] instead of all vars on the lhs of an implicit bi-dir equation. (Also : on lhs of the second equation.)
• Multiple matcher equations -- indeed multiple bi-directional equations.
• Recursive call to the synonym being defined (appearing only on the matcher side, but not on the top line, not as outermost constructor).

Contrast defining Snoc currently, needing a ViewPattern:

pattern Snoc xs     x <- (snoc -> Just (xs, x))
  where -- Snoc xs     x = xs ++ [x]              -- shorter, but no more efficient
        Snoc []     x = [x]
        Snoc (y:ys) x = y: Snoc ys x

snoc :: [a] -> Maybe ([a], a)
snoc []      = Nothing
snoc [x]     = Just ([], x)
snoc (x: xs) = Just (x: xs', x')
               where Just (xs', x') = snoc xs 

Too much machinery/unnecessary complexity

• The builder equations following where are just the same as the proposed equations.
• ViewPattern function snoc wraps its result in Maybe so that it signals success of the match; and
• has to build a pair for its result.

(Arguably the Maybe wrapper could be omitted with the equation for snoc [] = ... returning error.)

added PatternSynonyms label

Thank you @simonpj for the detailed technical workings out. To put it more naievely, I'm not trying to change the semantics or behaviour, just clothe that behaviour in less obtuse syntax. So if the implementation can be expressed using existing artefacts ("matchers"), that's terrific.

the builder is partial -- it does not cover all cases. That is a call of Pred like

   f x = Pred (Pred x)

might fail with a pattern-match failure. E.g. f Zero ...

Yes, I'd similarly expect pattern-match failure in a more simple case:

f2 x = Pred x

f2 Zero to pattern-match fail just as much as if Pred were defined

pattern Pred n <-  Succ -> n
  Pred (Succ n') = n'

Presumaly you'd expect a warning from the pattern synonym definition?

For that latter definition of Pred using the ViewPattern, GHC warns

Pattern match(es) are non-exhaustive
In an equation for `$bPred': Patterns not matched: Zero

So yes I'd expect similar.

Addit: BTW I think you have your types wrong for the "matcher":

   $mP :: t3 -> (t2 -> t2 -> r) -> r -> r

should be mentioning t1, not repeating t2:

$mP :: t3 -> (t1 -> t2 -> r) -> r -> r

To give the rationale/motivation here:

PatternSynonyms and ViewPatterns together are a great implementation of Wadler's ideas. But ViewPatterns syntax is:

• "ugly" -- I'd say Edward's example is not "extreme", compared to some I've seen; but beauty is in the eye of the beholder I guess, so less emotively
• that -> arrow-from-nowhere with the invisible argument I find very difficult to parse mentally. I need to stop and figure out what the types are. In Richard's example, there's a value to the right of the -> whose type does not appear in the pattern synonym's signature.
• Avoiding ViewPatterns would allow more PatternSynonyms to be written as (implicitly) bidirectional, therefore easier to verify visually as being identity on inversion.

So

1. I do not use ViewPatterns in the language-at-large, preferring to bury them inside PatternSynonyms;
2. Never the less I'd rather avoid ViewPatterns altogether;
3. ViewPatterns were released before PatternSynonyms, so it was natural to build on previous work; but
4. If PatternSynonyms had been developed first, I wonder if some other syntactic mechanism for invoking "matchers" would have come to mind?
5. That is, a mechanism more like allowing on LHS constructors and other pattern-y syntax.

BTW I think you have your types wrong for the "matcher":

Correct, thank you. I fixed it.

TL;DR. I think there is material for a good GHC Proposal here.

Is this related? https://github.com/ghc-proposals/ghc-proposals/pull/138

Is this related? https://github.com/ghc-proposals/ghc-proposals/pull/138

It is indeed! Essentially the same idea. I see I had responded to it, only two years ago, and yet I had 100.0% forgotten about it.

It's a bit more ambitious that the suggestion in this thread; the proposal suggests allowing a pattern synonym to be defined by multiple equations. But maybe that is over-reach, and it'd be better do go one step at a time.

It would need an active proposal author to carry it forward, but the existing proposal text makes a good starting point.

Good catch @rae, thank you!

Both there and here are motivated by liberalising pattern decls to look more like ordinary function equations (spelled upper-case -- per Richard's Aug 2018 comment [**]); and avoiding the non-intuitive ViewPatterns syntax.

But maybe that is over-reach, and it'd be better do go one step at a time.

Indeed, the O.P. here is a relatively conservative liberal ;-). I can foresee a whole progression of steps, each separately justifiable, but with diminishing returns of numbers of use cases. (The 'Unresolved Questions' in the Proposal have some more out-there ideas.)

I like @simonpj's approach of implementing as extra features translating to 'matchers' and 'builders'.

The ultimate objective IMO is to remove ViewPatterns from the language altogether. If that's not achievable, we've made the situation more complex:

• PatternSynonyms allow more liberal/complex forms; so
• ViewPatterns become more of a rarity; but
• If ViewPatterns are unavoidable in some cases, they'll be so rare nobody can remember how they work, and they'll have to be grokking really gnarly code.

Is it worth starting the journey?

[**] I do indeed think of PatternSynonyms as functions spelled upper-case. What entitles using upper-case? That the resulting value is invertible in a liberal sense: if we know which PatternSynonym was used to build the value, we can infer/reverse-engineer the synonym's arguments. (That's why I object to spelling TypeFamilies upper case, because they're not usually invertible even in that liberal sense.)

It would need an active proposal author to carry it forward, ...

OK I'll have a crack at an initial/modest proposal, sketching/linking to the further ideas as future steps.

The ultimate objective IMO is to remove ViewPatterns from the language altogether.

Hmm that's looking like a tall order. Here's a stretch example. (If anybody's still listening here ...) is this beyond possible?

2016 Pattern Synonyms Paper, Section 2.3 'Polymorphic Pattern Synonyms'. That title is a little misleading: it's not the Synonyms that are polymorphic; rather, the Synonyms are built from methods (including ViewPatterns) that are polymorphic. Ok ... to avoid those methods will need overloadable Pattern Synonyms. The example is Nil, Cons Synonyms overloaded for a variety of datatypes:

class ListLike f where                    -- constructor class
    pattern Nil  :: f a                   -- overloaded
    pattern Cons :: a -> f a -> f a       -- overloaded
{-  nil :: f a                            -- from Paper, builders not needed
    cons :: a -> f a -> f a
    nilMatch :: f a -> Bool               -- matchers/ViewPatterns not needed
    consMatch :: f a -> Maybe (a, f a)
-}

For most datatypes, the overloading for the Pattern Synonyms is obvious, but here's a tricky one:

data JoinList a = JNil | Unit a | JoinList a `JoinTree` JoinList a

instance ListLike JoinList  where
    pattern Nil  = JNil                   -- builder, matcher
            Nil <- Nil `JoinTree` Nil     -- matcher only, recursive, PatSyns allowed on rhs

-- The implicitly bi-directional top line needs no extension (beyond overloading the Synonym).
-- As currently, that can't be recursive, so provides a base case for recursion.
-- Putting an extra matcher line is an extension;
-- it's recursive in this case, so same effect as a recursive `ViewPattern`;
-- on rhs at outermost scope must be a data constructor, not a Pattern Synonym.

    pattern Cons x JNil                 = (Unit x)                 -- constructor on lhs
            Cons x xs                  <- (Unit x) `JoinTree` xs   -- line 2, see bullet 4
            Cons x xs                  <- Nil      `JoinTree` (Cons x xs)
            Cons x (xs `JoinTree` ys)  <- (Cons x xs) `JoinTree` ys
      where Cons x Nil                  = (Unit x)                 -- PatSyn on lhs
            Cons x (Nil `JoinTree` ys)  = (Unit x) `JoinTree` ys   -- line 6 } see bullet 4
            Cons x xs                   = (Unit x) `JoinTree` xs   -- line 7 }

(This may not be the 'best' definition; it's aimed more to show off innovations; also to show modest optimisation by squishing out redundant Nils. There's no attempt to balance the tree; that'll need guards on the builder equations.)

• The top (implicitly bi-dir) line has a data constructor on lhs -- that's an extension per the request in this ticket. It's providing a base case, so no Pattern Synonyms allowed.
• The matcher-only lines (with <-) allow PatSyns, including recursion, on rhs only, at outermost scope must be a data constructor. Implemented per @simonpj's sketched spec at "we simply adjust the matcher".
• PatSyns are allowed on lhs of builder-only lines, following where.
• Line 2 is the same as line 7, but a little sadly, we can't make anything bi-directional: for building, line 6's lhs must apply before line 7's; whereas if line 6 appeared as a matcher, it would introduce a redundant Nil.

OK I'll have a crack at an initial/modest proposal, sketching/linking to the further ideas as future steps.

I'm abandoning that idea. I hadn't understood enough about how PatSyns work (or don't, depending what you're trying to do)/ I don't think PatSyns in their present form are the right place to start from, so no point burdening them with more complexity.

I'm happy to support if someone else wants to have a crack.

I think you might find https://gitlab.haskell.org/ghc/ghc/-/wikis/view-patterns-alternative interesting. It proposes an alternative to view patterns, but short of full-on pattern synonyms. To me it seems a much nicer design than our current view patterns which are, as you say, clumsy. I like the idea of being able to write

f (Just (x | x>0)) = ...

where the | x>0 acts as a nested, compositional guard.

I think this design might be part of the journey you describe.

Revisiting this idea ... not so much because I like it any more than 3 years ago, but because I've been scratching around; there's nothing I like more. My initial reaction was perhaps a bit hasty:

@AntC3 TBH I find that syntax almost as clumsy as ViewPatterns ...

• It turns out that page had/has several downright wrong examples in which the critical calls to view functions are ill-typed. (I guess caused by editting the ViewPattern examples in a rush: the -> in those represents a 'missing' argument; swizzling the arrow round but failing to put back the argument makes for worse perplexity. Some of those have been corrected in the past few months, I've identified/messaged about a further two. [18-Apr-2024 now all fixed, thank you.])
• The inside-out nesting of the 'Erlang-style' parsePacket is just too hard to follow. AFAICT, the following comma-list of guards would be accepted with the proposal, and is much clearer to my mind:

  bits :: Int -> ByteString -> Maybe (Word, ByteString)
  -- (bits n bs) parses n bits from the front of bs, returning
  -- the n-bit Word, and the remainder of bs

  parsePacket :: ByteString -> ...
  --  parsePacket (p1 |  Just (n, (p2 | Just (val, bs) <- bits n p2)) <- bits 3 p1) = ...
  --  ^^ as was                  ^^   ^^                           ^^  -- too many nested parens

  parsePacket (p1 | Just (n, p2) <- bits 3 p1, Just (val, bs) <- bits n p2) = ...

I presume the deeply-nested form is there to compete against the ViewPatterns form in an obfuscated code contest. I've both produced less terse code, and reduced the number of tokens, without introducing any further dummy names. (I could even remove the outer parens, and arrive at valid H2010.)

But the critical question here is how this syntax would go in a PatternSynonym definition. (That feature was only a gleam in the eye at the time of writing up.) I'll try to figure that out in a later reply.

   f (Just (x | x>0)) = ...

I can see why you'd want to write something like that. TBH I find that syntax almost as clumsy as ViewPatterns, especially if I imagine nesting those. As I said before, I'd rather keep the clumsiness out of the language-at-large, and limit fancy pattern stuff to being inside pattern decls -- where they can at least get a meaningful name (compare the earlier Positive):

pattern JustPos x | x>0 = Just x         -- implicitly bi-dir

f (JustPos x) = ...

• The guard applies for both the "matcher" and "builder" in this case.
• We'd need to support explicitly bi-dir forms with guards, in case the guard is to apply only for the "matcher" or only for the "builder".
• That equation follows current function LHS syntax, no need to introduce nested guards. (No clumsiness needed here.)
• Guards are not currently allowed in patterns; "the journey" needs to add that capability.
• So that implicitly bi-dir decl follows what we're already discussing here: allow the form for 'underneath line's to appear as the only/top equation.
• For nesting, allow pattern synonyms with these liberal forms to appear on LHS of pattern decls.

(We're agreeing on expressivity; differing on aesthetics only.)

Addit: I guess the feature of ViewPatterns I'm not trying to mimic is introducing fresh variables and making them available to the right for more pattern-matching. Again aesthetically, I find those examples almost unreadable. I'd rather allow as-patterns within pattern decls -- which again follows current function LHS syntax.

It might be we allow an as-pattern to support two patterns (including two pattern synonym destructurings), by putting a pattern to the left of the @. (I think there's already an idea like that?)

This from that patterns-alternative page makes my stomach churn

   f (x | xs <- x, h : t <- x) = h : (xs ++ t)

Is it trying to say this?

f x@(xs@(h : t)) = h : (xs ++ t)

In what way is the obfuscated form 'better'? What is the x other than noise?

I'd also prefer to avoid "view patterns can do arbitrary computation, perhaps expensive,". More liberal "matcher"s (per the 'journey') will indeed need to do some computation; but if it's only of the forms of destructuring/restructuring and guard-checking, that's no worse than pattern matching currently, and should be more scrutable.

"The requisite join-list example:". That is, requisite from the view patterns alternatives discussions. It's a long way into the future from the proposal here, but the fuller #138 doesn't seem to demonstrate it. It does need

the proposal suggests allowing a pattern synonym to be defined by multiple equations.

   data JList a = Empty 
                | Single a
                | Join (JList a) (JList a)

pattern { Nil = Empty                                     -- base case, bi-dir
        ; Nil <- Join Nil Nil                             -- recursive, matcher only
        }
pattern { Cons x Empty        =  Single x                 -- bi-dir
        ; Cons y ys           <- Join Nil         (Cons y ys)
        ; Cons x (Join xs ys) <- Join (Cons x xs) ys
        }
  where   Cons x xs           =  Join (Single x)  xs      -- builder only

The generated "matcher"s also need multiple equations (case branches). I've followed the sequence in the pattern decl.

$mNil :: JList a -> r -> r -> r
$mNil s cont fail
  = case s of
      Empty        -> cont
      Join Nil Nil -> cont
      _            -> fail
$mCons :: JList a -> (a -> JList a -> r) -> r -> r
$mCons s cont fail
  = case s of
      Single x             -> cont x Empty
      Join Nil (Cons y ys) -> cont y ys
      Join (Cons x xs) ys  -> cont x (Join xs ys)
      _                    -> fail

(I think this gives total functions; but the compiler won't be able to see that. It doesn't, for example, know that Nil vs Cons are mutually exclusive.)

A stray thought with Dependent Haskell going ahead ...

• Unifying the term language and the type language will make type synonyms syntactically very like pattern synonyms(?)
• So we could get bidirectional type synonyms? Useful in instance heads, for example, or as arguments to type functions.
• As opposed to type familys/functions that are not injective/not pattern-matchable, so the family name should be spelled lower-case(?)

Side-by-side compare the O.P.

newtype Vec a (n :: Nat) = Vec { unVec :: [a] }

currently	to be
pattern VNil :: Vec a 0	pattern VNil :: Vec a 0
pattern VNil = Vec []	VNil = Vec []
	-- pattern not repeated, use layout or { ; }
pattern VCons :: a -> Vec a n -> Vec a (n + 1)	pattern VCons :: a -> Vec a n -> Vec a (n + 1)
pattern VCons x xs <- Vec (x : (Vec -> xs)) where	VCons x (Vec xs) = Vec (x : xs)
VCons x (Vec xs) = Vec (x : xs)	-- note above implic bi-dir line same as current 'build'

I think the eventual goal here is, for implicitly bi-directional equations:

• The lhs allows anything allowed in a pattern binding, including guards and @s-patterns;

  (Currently all that's allowed is vars; that's the restriction that forces putting View Patterns on rhs, to match against the nested type. Ah 'anything' except View Pattern calls. ?not wildcards -- maybe needed to avoid introducing a var that won't appear on rhs because it's already captured in an @s-pattern.)

• In lhs outermost constructor position must be the type synonym being defined.

• The rhs must contain only constructors, vars and other pattern synonyms (incl possibly a recursive call);

• In rhs outermost constructor position must be a constructor from the datatype to which they 'belong'.

• The free vars must be the same on each side.

• The two sides must be of the same type.

  (Possibly that needs a signature given for the pattern synonym, to fix type params for the datatype which aren't grounded in arguments to the synonym.)

Then the implicitly bi-directional equation can be the same as the 'underneath' equation of the explicitly bi-dir form -- assuming the top and bottom lines are intended to be inverses.

Allowing pattern decl inside classes/instances would give cleaner code:

• supporting bi-directional decls;
• needing only constructors/avoiding ViewPatterns and additional methods.

instance Ord a => Collection [] a  where
  empty = []
  singleton x = [x]
  pattern PEmpty = []
  pattern PSingleton x = [x]

... or we might be able to declare more patterns as bi-directional/avoiding ViewPatterns if we could make the lhs of pattern synonym decls look more like the lhs of patterns:

pattern PEmpty :: (Eq (c a), Collection c a) => c a
pattern xs@PEmpty | xs == empty = xs

pattern x@Zero | x == 0 = x

(Zero example adapted from here.)

Those work as bi-dir because the free vars are the same on each side of =. The guard mentions only those free vars/doesn't introduce more vars with let or <-, so the guard is really 'shared' between the two sides/can be taken in either direction.

mentioned in issue #22145

Another request here in the same ball park. That is, not to put constructors on LHS, but to allow multiple unidirectional <- equations, with different data constructors on RHS.

The example in the User's Guide of an explicitly bidir Pattern Syn seems tantalisingly close to being written as implicitly bidir:

   pattern HeadC x <- x:xs where
     HeadC x = [x]

• True that the top line alone can't be turned into implicit bidir -- " it wouldn’t specify a value for the ⟨xs⟩ on the right-hand side.", as the Guide says.

• But that xs is just clutter, we're never going to use it, so a wildcard works just as well:

    pattern HeadC x <- x:_ where ...

• What's more, a lazy pattern also works just as well:

    pattern HeadC x <- x: ~[] where ...
  
    > (\(HeadC x1) -> x1) "hello"  -- ===> 'h'

• The PattSyn just isn't interested in the tail of the list.

• So if only I could go bidirectional:

    pattern HeadC x = x: ~[]

• With the rule that when converting the PattSyn to a builder, drop the lazy ~.

possible syntax

pattern (Find_in env) val <- _v  | Just val <- lookup env _v

Historical note/clarification: this example is based on the poster child lookup of the ViewPatterns docos

the function clunky from Pattern guards can be written using view patterns as follows:

```
clunky env (lookup env -> Just val1) (lookup env -> Just val2) = val1 + val2
...other equations for clunky...
```

The ultra-clunky version of that is wrt what you'd need in H98/was presented as a justification for multi-guards that were adopted in the H2010 standard. The form for lookup with guards isn't too shabby (I'll also give the form using view patterns alternative: a matter of taste, I think.)

clunky env var1 var2 | Just val1 <- lookup env var1, Just val2 <- lookup env var2 = val1 + val2

--  or  --
clunky env (var1 | Just val1 <- lookup env var1) (var2 | Just val2 <- lookup env var2) = val1 + val2

Ok, that's more verbose than the ViewPatterns form, because of the need to explicitly name the arguments then pass them as args to the lookup. And superfluous because (presumably) var1, var2 aren't needed on RHS.

For a more succinct Pattern Synonym approach I was hoping to achieve even less clunkiness:

clunky env (Find_in env val1) (Find_in env val2) = val1 + val2

Although val1, val2 are fresh bindings as usual for a PattSyn in matcher position, the appearances of env mustn't be fresh/must be a use of the env already bound.

Can the 'macro-expansion'[**] of PattSyn Find_in (appearing in a matcher position) be given as (and making up syntax on the fly):

pattern _varn@(Find_in env valn) <- (_varn | Just valn <- lookup env _varn)

Where _varn is to be treated as fresh in each appearance. Otherwise the 'less clunkiness' example would get macro-expanded[**] to:

clunky env (_varn | Just val1 <- lookup env _varn) (_varn | Just val2 <- lookup env _varn) = val1 + val2

===> ERROR - Repeated variable "_varn" in pattern / * Conflicting definitions for '_varn'

[**] PostThought: 'macro-expansion' is not how the implementation approaches the appearance of a PattSyn in matcher position. See 'Pattern Synonyms' paper 2016 §5 point 5 and discussion following. "subtly different from macro-substitution". Then names passed as parameters to PattSyns are treated only as patterns, not arguments that can be evaluated. So see next comment declaring a local PattSyn, to capture an in-scope value.

---

Hmm, hmm this discussion is explicitly wrt bidirectional PattSyns, and I especially wanted to avoid the unidirectional form, not least because IMO the arrow in pattern Blah x y <- ... is pointing in the wrong direction for how I think of it. In the example of a lookup, there's no corresponding 'builder', let alone a way to express the two in one equation.

the appearances of env mustn't be fresh/must be a use of the env already bound.

And it's kinda cheating to claim Find_in is a view on a var when it's a view on a var-within-env. Then maybe:

clunky env (Find_in_env val1) (Find_in_env val2) = val1 + val2
    where
        pattern Find_in_env val <- (_var | Just val <- lookup env _var)

Using the pattern decl form that with unidirectionals, you can introduce RHS vars not appearing on LHS.

There'd presumably be other equations for clunky within scope of the where, to cover cases of one but not both vars are found.

This also fits with my feeling PattSyns are just functions that can also be used for matching, so declarable everywhere a function is.

But the critical question here is how this syntax would go in a PatternSynonym definition.

"this syntax" meaning View Patterns alternative, to be used for defining Pattern Synonyms. What I still like about the o.p. here [**] is its succinctness, and how clearly it connects the semantics of the builder and the matcher:

newtype Vec a (n :: Nat) = Vec { unVec :: [a] }

pattern VCons :: a -> Vec a n -> Vec a (n + 1)
pattern VCons x (Vec xs) = Vec (x : xs)                  -- proposed bidirectional syntax

To turn that equation into a matcher, we notionally go through an intermediate

pattern VCons x (_vxs | (Vec xs) <- _vxs) = Vec (x : xs) -- not proposed syntax for pattern decl [***]

pattern VCons x _vxs = ( Vec (x : xs) | _vxs <- Vec xs ) -- final form, also part of this proposal [****]

In swizzling the guard/binding to RHS, need also to swizzle its arguments. I've embracketed the RHS, to anticipate it appearing as VPa style.

We now have LHS of the pattern decl using only bare vars as dummy args. _vxs is a fresh local var. At a matcher usage site:

headVec :: Vec a (n + 1) -> a
headVec (VCons x _) = x

--  compiles to  --                              -- 'desugar' the VCons to RHS of its (final form) equation
headVec (Vec (x: _xs1) | _ <- Vec _xs1 ) = x 

tailVec :: Vec a n -> Vec a (n - 1)
tailVec (VCons _ vxs) = vxs

--  compiles to  --                              -- 'desugar' the VCons to RHS of its (final form) equation
tailVec (Vec (_: _xs1) | vxs <- Vec _xs1 ) = vxs 

[**] What I'm not so happy about with the o.p. is using varname xs in different equations at two different types. Throughout here, xs, _xs :: [a]; vxs, _vxs :: Vec a n.

[***] It might seem cute to allow guards-in-general on LHS of PattSyn decl (see also [****]):

• Booleans would be nice; but
• lets aren't swizzleable; nor
• pattern guard <-s in general aren't swizzleable.

[****] A nice-to-have/future would be guards-in-general on RHS of PattSyn decl.

• Any pattern guard <-s arising from the PattSyn LHS should be inserted before those guards.

The summing-up/for discussion.

@simonpj I think you might find View Patterns alternative interesting. It proposes an alternative to view patterns,

I did lean quite heavily on that work, thank you. OTOH, I think this claim might be overstated:

There are straightforward translations between old and new style view patterns

At my summing-up see the translation for the Polar rho phi | ... = Cart x y | ... example. 'Translating' from that to current ViewPatts made my head hurt. I think the rules you give are not adequate in case of mapping two vars (x, y) to two vars (rho, phi) where each on one side derives from both on the other side.