[GHC] #12203: Allow constructors on LHS of (implicit) bidirectional pattern synonym
#12203: Allow constructors on LHS of (implicit) bidirectional pattern synonym -------------------------------------+------------------------------------- Reporter: ezyang | Owner: Type: feature | Status: new request | Priority: low | Milestone: Component: Compiler | Version: 8.0.1 (Type checker) | Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12203 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12203: Allow constructors on LHS of (implicit) bidirectional pattern synonym -------------------------------------+------------------------------------- Reporter: ezyang | Owner: Type: feature request | Status: new Priority: low | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (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) }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12203#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12203: Allow constructors on LHS of (implicit) bidirectional pattern synonym -------------------------------------+------------------------------------- Reporter: ezyang | Owner: Type: feature request | Status: new Priority: low | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Keywords: Resolution: | PatternSynonyms Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * keywords: => PatternSynonyms -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12203#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12203: Allow constructors on LHS of (implicit) bidirectional pattern synonym -------------------------------------+------------------------------------- Reporter: ezyang | Owner: Type: feature request | Status: new Priority: low | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Keywords: Resolution: | PatternSynonyms Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (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? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12203#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12203: Allow constructors on LHS of (implicit) bidirectional pattern synonym -------------------------------------+------------------------------------- Reporter: ezyang | Owner: Type: feature request | Status: new Priority: low | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Keywords: Resolution: | PatternSynonyms Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by ekmett): * cc: ekmett (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12203#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12203: Allow constructors on LHS of (implicit) bidirectional pattern synonym -------------------------------------+------------------------------------- Reporter: ezyang | Owner: Type: feature request | Status: new Priority: low | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Keywords: Resolution: | PatternSynonyms Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by Iceland_jack): * cc: Iceland_jack (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12203#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12203: Allow constructors on LHS of (implicit) bidirectional pattern synonym -------------------------------------+------------------------------------- Reporter: ezyang | Owner: Type: feature request | Status: new Priority: low | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Keywords: Resolution: | PatternSynonyms Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * cc: RyanGlScott (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12203#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12203: Allow constructors on LHS of (implicit) bidirectional pattern synonym -------------------------------------+------------------------------------- Reporter: ezyang | Owner: Type: feature request | Status: new Priority: low | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Keywords: Resolution: | PatternSynonyms Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12203#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12203: Allow constructors on LHS of (implicit) bidirectional pattern synonym -------------------------------------+------------------------------------- Reporter: ezyang | Owner: Type: feature request | Status: new Priority: low | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Keywords: Resolution: | PatternSynonyms Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (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)`. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12203#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12203: Allow constructors on LHS of (implicit) bidirectional pattern synonym -------------------------------------+------------------------------------- Reporter: ezyang | Owner: Type: feature request | Status: new Priority: low | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Keywords: Resolution: | PatternSynonyms Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (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! -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12203#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12203: Allow constructors on LHS of (implicit) bidirectional pattern synonym -------------------------------------+------------------------------------- Reporter: ezyang | Owner: Type: feature request | Status: new Priority: low | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Keywords: Resolution: | PatternSynonyms Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by dfeuer): * cc: dfeuer (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12203#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12203: Allow constructors on LHS of (implicit) bidirectional pattern synonym -------------------------------------+------------------------------------- Reporter: ezyang | Owner: (none) Type: feature request | Status: new Priority: low | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Keywords: Resolution: | PatternSynonyms 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: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * related: => #13672 Comment: Another example from #13672 which requires this functionality: {{{#!hs 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)))) }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12203#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12203: Allow constructors on LHS of (implicit) bidirectional pattern synonym -------------------------------------+------------------------------------- Reporter: ezyang | Owner: (none) Type: feature request | Status: new Priority: low | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Keywords: Resolution: | PatternSynonyms 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: | -------------------------------------+------------------------------------- Comment (by Iceland_jack): Use case {{{#!hs 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' }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12203#comment:12 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC