# (Implicitly) Bidirectional Pattern Synonyms: can they be smarter?

**URL:** <https://discourse.haskell.org/t/implicitly-bidirectional-pattern-synonyms-can-they-be-smarter/5816>\
**Category:** Uncategorized\
**Created:** [February 16, 2023, 2:01am UTC](https://discourse.haskell.org/t/implicitly-bidirectional-pattern-synonyms-can-they-be-smarter/5816 "2023-02-16T02:01:47Z")\
**Posts on this page:** 1\
**Page:** 1

<div class="post-metadata">

**Author:** ![AntC2](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/antc2/32/1872_2.png) [@AntC2](https://discourse.haskell.org/u/AntC2)\
**Post date:** [February 16, 2023, 2:01am UTC](https://discourse.haskell.org/t/implicitly-bidirectional-pattern-synonyms-can-they-be-smarter/5816/1 "2023-02-16T02:01:48Z")

</div>

> [A pattern synonym declaration can be either unidirectional, bidirectional or explicitly bidirectional.](https://downloads.haskell.org/~ghc/8.10.7/docs/html/users_guide/glasgow_exts.html#syntax-and-scoping-of-pattern-synonyms)

Am I right in thinking the (Implicitly) Bidirectional form is just a shorthand for writing Explicitly Bidir? For example (adapted from the User Guide), I want to write a bidir

```haskell
pattern HeadC x = x: ~[]

```

That’s accepted as a unidir (with `<-` instead of `=`). And because the `~` makes it irrefutable, it’ll match to anything in the tail, not just a `[]`. That’s rejected as bidir `Pattern '~[]' is not invertible`. Well, oh compiler, just strip off the `~` and it will be invertible. IOW apply a little interpretation in rewriting to Explicitly Bidir:

```haskell
pattern HeadC x <- x : _ where -- convert any irrefut patt ~[] to wildcard _
        HeadC x = x : [] -- strip off the ~

```

Another example from the User Guide wrt strictness annotations , I write:

```haskell
pattern StrictJust !a = Just !a
-- interpreted to
pattern StrictJust a <- Just !a where -- strip off the BangPattern
        StrictJust !a = Just a -- in places it's not valid

```

Or from [this ticket](https://gitlab.haskell.org/ghc/ghc/-/issues/12203#note_121599) – I imagine the Explicit Bidir encoding gets quite annoying for `newtype`s:

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

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

```

Note in that last example, the Implicitly Bidir equation (with `newtype` constrs) is exactly what’s needed for the explicit building equation; the explicit matching equation inverts the constrs using a `ViewPattern` – no need to go via field selectors, contra to the way discussion goes on that ticket.

There’ll need to be some restrictions:

- The free vars must be the same each side of the equation. (Already applies for Implicitly Bidir.)
- Otherwise all that can appear is Constructors; and
- pattern irrefutable or strictness annotations.
- (A free var can’t appear inside a irrefutable `~` binding.)