Opened 3 years ago
Last modified 20 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:2 Changed 3 years ago by
Keywords: | PatternSynonyms added |
---|
comment:3 Changed 2 years ago by
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.
comment:4 Changed 2 years ago by
Cc: | ekmett added |
---|
comment:5 Changed 2 years ago by
Cc: | Iceland_jack added |
---|
comment:6 Changed 2 years ago by
Cc: | RyanGlScott added |
---|
comment:7 Changed 2 years ago by
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 2 years ago by
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 2 years ago by
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 2 years ago by
Cc: | dfeuer added |
---|
comment:11 Changed 22 months ago by
Related Tickets: | → #13672 |
---|
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 20 months ago by
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'
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:
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.)