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
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:
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:
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 – I imagine the Explicit Bidir encoding gets quite annoying for newtypes:
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.)