Pattern synonym used in an expression context could have different constraints to pattern used in a pattern context
The two directions of an explicitly-bidirectional pattern might have utterly different class constraints. After all, the two directions are specified by quite different code. Suppose that
- Pattern
P
(used in a pattern) requires constraintsCR
, and provides constraintsCP
- Constructor
P
(used in an expression) requires constraintsCE
Then I think the only required relationship is this:
CP
must be provable fromCE
(since CP is packaged up in a P-object).
Currently, CE := CP + CR
.
No child items are currently assigned. Use child items to break down this issue into smaller parts.
Relates to
- #124268.2.15
Activity
- Gergő Érdi mentioned in issue #5144 (closed)
mentioned in issue #5144 (closed)
- Gergő Érdi changed weight to 5
changed weight to 5
- Gergő Érdi added Tfeature request Trac import labels
added Tfeature request Trac import labels
- Gergő Érdi mentioned in issue #8584 (closed)
mentioned in issue #8584 (closed)
I've often wished that
_
in expressions was a shorthand forundefined
.- Joachim Breitner mentioned in issue #8779 (closed)
mentioned in issue #8779 (closed)
- Gergő Érdi mentioned in issue #8961 (closed)
mentioned in issue #8961 (closed)
- Reporter
This would be very nice to have, +1.
The possibility of
_
being a shorthand forundefined
is intriguing. It allows_
to be a run-of-the-mill pattern exported byPrelude
that may be redefined by users! The regular wildcard meaning where the expression isundefined
could be defined as such with the proposed syntax:pattern _ <- a where _ = undefined failure :: a -> b failure _ = _
_
in expressions is already in use for typed holes (http://www.haskell.org/ghc/docs/latest/html/users_guide/typed-holes.html).- Author Developer
I have a working version of this in the
wip/pattern-synonyms
branch. It still needs some finishing (mostly, adding tests).The only difficult part of this work was ensuring that the following works (and is not regarded as a recursive pattern synonym):
pattern P x <- (x:_) where P x = foo [x] foo (P x) = [x, x]
- Author Developer
Pushed
576f461
towip/pattern-synonyms
, please review forHEAD
. It validates and has a test case for bidirectional pattern synonyms. - Gergő Érdi changed milestone to %7.10.1
changed milestone to %7.10.1
- Gergő Érdi closed
closed
- Author Developer
Trac metadata
Trac field Value Resolution Unresolved → ResolvedFixed - Maintainer
- Developer
I just tried out this patch and it seems strange to me that the constructor synonym has the same class constraints as the pattern. Is this by design? Here is an example which would have worked really nicely if not for this restriction. I know you can get around this by defining your own constructors with the right types.
Note that there is no
View
instance forHoley
which makes sense but we can still define aConstruct
instance.{-# LANGUAGE PatternSynonyms, ViewPatterns #-} data ExpF a = AddF a a | NumF Int deriving Show class Construct a where construct :: ExpF a -> a class View a where view :: a -> ExpF a newtype Exp = Exp (ExpF Exp) deriving (Show) instance Construct Exp where construct e = Exp e instance View Exp where view (Exp e) = e data Holey = Hole | NonHole (ExpF Holey) instance Construct Holey where construct = NonHole pattern Add a b <- (view -> AddF a b) where Add a b = (construct (AddF a b)) pattern Num n <- (view -> NumF n) where Num n = (construct (NumF n))
- Developer
It's a bit hard to understand your example because you don't give any types, or any code that you think should work, but doesn't.
But I think you mean this: the two directions of an explicitly-bidirectional pattern might have utterly different class constraints. After all, the two directions are specified by quite different code. Suppose that
- Pattern
P
(used in a pattern) requires constraintsCR
, and provides constraintsCP
- Constructor
P
(used in an expression) requires constraintsCE
Then I think the only required relationship is this:
CP
must be provable fromCE
(sinceCP
is packaged up in a P-object).Is this what you meant? Then indeed I think that we have not really discussed this possibility at all.
There is a tricky UI issue, which is how to say when you ask
:info P
. And, worse still, what it would mean to give a type signature toP
.So it looks to me, on first impression, that what you want is do-able and sensible. But there are some design issues to work out first. Let's see what Gergo has to say.
Simon
- Pattern
- Developer
That is exactly what I mean, thank you for taking the time to clarify my comment. To once again be more specific, the code example I posted fails to type check with the following error message.
fix.hs:27:14: Could not deduce (Construct a) arising from a use of ‘construct’ from the context (View a) bound by the type signature for Main.$WAdd :: View a => a -> a -> a at fix.hs:1:1 Possible fix: add (Construct a) to the context of the type signature for Main.$WAdd :: View a => a -> a -> a In the expression: (construct (AddF a b)) In an equation for ‘$WAdd’: $WAdd a b = (construct (AddF a b)) fix.hs:30:12: Could not deduce (Construct a) arising from a use of ‘construct’ from the context (View a) bound by the type signature for Main.$WNum :: View a => Int -> a at fix.hs:1:1 Possible fix: add (Construct a) to the context of the type signature for Main.$WNum :: View a => Int -> a In the expression: (construct (NumF n)) In an equation for ‘$WNum’: $WNum n = (construct (NumF n))
- Developer
Re-opening because of ticket:8581#comment:87342 and following.
Simon
- Simon Peyton Jones reopened
reopened
- Simon Peyton Jones unassigned @trac-cactus
unassigned @trac-cactus
- Developer
Trac metadata
Trac field Value Resolution ResolvedFixed → Unresolved - Author Developer
Hmm. Implementation-wise, there's no reason why
P
-as-an-expression andP
-as-a-pattern has to have the same constraints -- in fact, they could even have completely different types... But we check that they do have the same type so that they behave more like a real constructor. The reasonCE := CP + CR
at the moment is that this is how a GADT constructor is typed.So, ummm, how far do we want to let pattern synonym types wander from regular constructor types? That is the question here.
- Developer
Ideally, as far as the programer wants, provided CP is provable from CE.
- Developer
Question for mpickering. How would it be if the pattern synonym had just ONE type, but it was the most constraining of the two directions. Thus in your example,
pattern type Add a a :: (View a, Construct a) => a
rather than
pattern type Add a a :: (View a) => a
which is what we get from the pattern side, but which doesn't work on the expression side.
The down-side is that pattern-matching would need a
(Construct a)
constraint that is not strictly necessary. How bad would that be?Simon
- Gergő Érdi added PatternSynonyms label
added PatternSynonyms label
- Developer
It does feel unnecessary to insist on the extra constraint. That being said, it does match up better with the original semantics of the constructor.
- Author Developer
I think I like the
CE => CP
suggestion. Implementing it will be a bit tricky, because currently we typecheck pattern synonyms in two passes:- First we typecheck the pattern part, and build an internal representation
PatSyn
, which contains (among other things) the builder'sId
, so it has to know its type. But currently that's not a problem, since the type is exactly known from the pattern part. - Then at a later point, the builder is typechecked against this type stored in
PatSyn
.
So if we want to have any leeway in the builder type compared to the matcher type, we have to either typecheck the builder in the first stage as well, or not store its type in the
PatSyn
.To see why the first solution doesn't work, we need to look at the reason builders are typechecked in a separate pass: to support explicitly-bidirectional pattern synonyms where the builder refers to something which refers to the matcher, e.g. see
testsuite/tests/patsyn/should_run/bidir-explicit-scope.hs
:pattern First x <- x:_ where First x = foo [x, x, x] foo :: [a] -> [a] foo xs@(First x) = replicate (length xs + 1) x
However, we also can't omit the type of the builder from the
PatSyn
representation for the same reason: supposeFirst
occured in the right-hand side offoo
; how would we know what type to give it, if all we have at hand is thePatSyn
forFirst
?Maybe there's a way out of all this if the builder type is initialized to a fresh skolem tyvar which is filled in when the builder is typechecked; but someone more knowledgeable about the typechecker's internals will have to chime in on that. I'm worried that, at the very least, it would lead to horrible error messages when something goes wrong, since the use sites of a pattern synonym builder could now influence the typechecking of the definition of said builder.
- First we typecheck the pattern part, and build an internal representation
- Gergő Érdi mentioned in issue #9867 (closed)
mentioned in issue #9867 (closed)
- Gergő Érdi removed PatternSynonyms label
removed PatternSynonyms label
- thoughtpolice removed milestone
removed milestone
Moving to 7.12.1 milestone; if you feel this is an error and should be addressed sooner, please move it back to the 7.10.1 milestone.
Is it true that support for this didn't make it into 7.10?
That looks to be the case, although it also looks to be the case that it did sneak in to the documentation:
https://downloads.haskell.org/~ghc/7.10.1/docs/html/users_guide/syntax-extns.html#pattern-synonyms
But my attempt to use the bidirectional syntax:
{-# LANGUAGE PatternSynonyms #-} data AugmentedRational = Exact' Integer Rational | Approximate (forall a.Floating a => a) pattern Exact z q <- Exact' z q where Exact z q | q == 0 = Exact' 0 0 | otherwise = Exact' z q
is rejected with
parse error on input `where'
By contrast, the 7.8.4 docs don't list this syntax, see https://downloads.haskell.org/~ghc/7.8.4/docs/html/users_guide/syntax-extns.html#pattern-synonyms.
Trac metadata
Trac field Value CC → douglas.mcclean@gmail.com dmcclean, I was able to compile your program with ghc-7.10.0.20150123, though I had to add the RankNTypes language extension as well; can you double check?
- Developer
There is definitely support in GHC 7.10 for bidirectional pattern synonyms. Unfortunately I can't reproduce your problem, can you post a larger example?
So sorry guys. min-ghc made some changes to my path that didn't survive a reboot. So I was trying to use this feature for the first time, but at the same time I was unwittingly using 7.8.3 thinking it was 7.10.1.
I'll endeavor to be more careful in the future.
- Developer
Interesting. Gergo, what's the status on this ticket? Done, or incomplete?
Simon
- thoughtpolice changed milestone to %8.0.1
changed milestone to %8.0.1
Milestone renamed
- Developer
OK, I'm coming back to this ticket 16 months later with a much better understanding of the conversation.
Gergo's last comment (:19) is informative. I still think that this restriction should be removed in line with what Simon suggests (
CE => CP
).I can't add much to Gergo's worries about the implementation but
- I hope this two stage type checking could be simplified, it's something I want to eventually look at.
- One obvious stop-gap solution would be allow a user to provide a separate type signature for the builder. This gets around the whole "not being able to infer the type" problem.
This ticket is probably a long way out of cache by now Simon but do you have any thoughts about my first bullet point? do you think it would be possible to refactor the pattern synonym type checking so the type of the builder can be inferred?
- Matthew Pickering changed title from Add support for explicitly-bidirectional pattern synonyms to Pattern synonym used in an expression context could have different constraints to pattern used in a pattern context
changed title from Add support for explicitly-bidirectional pattern synonyms to Pattern synonym used in an expression context could have different constraints to pattern used in a pattern context
- Developer
Trac metadata
Trac field Value BlockedBy #5144 (closed) → - CC douglas.mcclean@gmail.com → - - Matthew Pickering changed the description
changed the description
- Developer
- Developer
I've looked a bit now. It seems like the correct thing to do is disassemble the
PatSyns
so that the builder/matcher can be handled separately. The way to do this seems to be to modifyValBindsOut
to use a new datatype instead ofHsBinds
, split apart the pat syn when calculating sccs and then stitch it back together after typechecking if that is still necessary. - Developer
This plan runs into problems as we can't given the matcher and builder different
Name
s as they are both in the same namespace so there is no way to disambiguate which one we should choose. As a result, the dependency analysis is still too coarse, all occurrences point to the same thing which is not what we want. - Developer
Let's not think about implementation before we have a design. I have not read the entire thread again, but I'm pretty convinced that
- We can't have two different types, one for construction and one for pattern matching
I think it'll just be too confusing to have two types. It's bad enough to have this provided/required stuff without, in addition, having a completely separate type for construction. Are you seriously proposing to have two signatures for each pattern synonym? (Optionally, I assume.)
So: if you give a pattern signature, I think it has to work for both construction and pattern matching. If you need extra constraints for construction, define a smart constructor (that can happen today with regular data constructors).
Let's not over-elaborate until we have more experience. There are plenty of open tickets to tackle on the pattern-synonym front.
- Icelandjack mentioned in issue #11658
mentioned in issue #11658