Opened 18 months ago

Last modified 6 months ago

#12203 new feature request

Allow constructors on LHS of (implicit) bidirectional pattern synonym

Reported by: ezyang Owned by:
Priority: low Milestone:
Component: Compiler (Type checker) Version: 8.0.1
Keywords: PatternSynonyms Cc: ekmett, Iceland_jack, RyanGlScott, dfeuer
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: #13672 Differential Rev(s):
Wiki Page:

Description

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.

Change History (12)

comment:1 Changed 18 months ago by ezyang

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.)

Last edited 18 months ago by ezyang (previous) (diff)

comment:2 Changed 18 months ago by simonpj

Keywords: PatternSynonyms added

comment:3 Changed 16 months ago by simonpj

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.

Last edited 16 months ago by simonpj (previous) (diff)

comment:4 Changed 16 months ago by ekmett

Cc: ekmett added

comment:5 Changed 16 months ago by Iceland_jack

Cc: Iceland_jack added

comment:6 Changed 16 months ago by RyanGlScott

Cc: RyanGlScott added

comment:7 Changed 16 months ago by mpickering

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.

comment:8 Changed 16 months ago by simonpj

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).

comment:9 Changed 16 months ago by mpickering

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!

comment:10 Changed 16 months ago by dfeuer

Cc: dfeuer added

comment:11 Changed 7 months ago by RyanGlScott

Another example from #13672 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))))

comment:12 Changed 6 months ago by Iceland_jack

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'
Note: See TracTickets for help on using tickets.