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