Opened 4 years ago

Last modified 5 months ago

#8581 new feature request

Pattern synonym used in an expression context could have different constraints to pattern used in a pattern context

Reported by: cactus Owned by:
Priority: normal Milestone:
Component: Compiler Version:
Keywords: PatternSynonyms Cc: lelf, mpickering, liyang
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description (last modified by mpickering)

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 constraints CR, and provides constraints CP
  • Constructor P (used in an expression) requires constraints CE

Then I think the only required relationship is this: CP must be provable from CE (since CP is packaged up in a P-object).

Currently, CE := CP + CR.

Change History (50)

comment:1 Changed 4 years ago by ntc2

I've often wished that _ in expressions was a shorthand for undefined.

comment:2 Changed 3 years ago by Iceland_jack

This would be very nice to have, +1.

The possibility of _ being a shorthand for undefined is intriguing. It allows _ to be a run-of-the-mill pattern exported by Prelude that may be redefined by users! The regular wildcard meaning where the expression is undefined could be defined as such with the proposed syntax:

pattern _ <- a where
  _ = undefined

failure :: a -> b
failure _ = _

comment:3 Changed 3 years ago by dfranke

_ in expressions is already in use for typed holes (http://www.haskell.org/ghc/docs/latest/html/users_guide/typed-holes.html).

comment:4 Changed 3 years ago by cactus

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]

comment:5 Changed 3 years ago by cactus

Status: newpatch

Pushed 576f461 to wip/pattern-synonyms, please review for HEAD. It validates and has a test case for bidirectional pattern synonyms.

comment:6 Changed 3 years ago by cactus

Milestone: 7.10.1

comment:7 Changed 3 years ago by cactus

Resolution: fixed
Status: patchclosed

comment:8 Changed 3 years ago by hvr

For the record: the commit-range 12644c3c0216edfcff33266f4f250e0c52004352 to 535b37cbb5a11dd4c9d8260d1d00f4cb993af0e9 seems to be what was merged to address this ticket.

comment:9 Changed 3 years ago by mpickering

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 for Holey which makes sense but we can still define a Construct 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))

Last edited 3 years ago by mpickering (previous) (diff)

comment:10 Changed 3 years ago by simonpj

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 constraints CR, and provides constraints CP
  • Constructor P (used in an expression) requires constraints CE

Then I think the only required relationship is this: CP must be provable from CE (since CP 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 to P.

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

comment:11 Changed 3 years ago by mpickering

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

comment:12 Changed 3 years ago by simonpj

Re-opening because of comment:9 and following.

Simon

comment:13 Changed 3 years ago by simonpj

Owner: cactus deleted
Resolution: fixed
Status: closednew

comment:14 Changed 3 years ago by cactus

Hmm. Implementation-wise, there's no reason why P-as-an-expression and P-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 reason CE := 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.

comment:15 Changed 3 years ago by simonpj

Ideally, as far as the programer wants, provided CP is provable from CE.

comment:16 Changed 3 years ago by simonpj

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

comment:17 Changed 3 years ago by cactus

Keywords: pattern synonyms added

comment:18 Changed 3 years ago by mpickering

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.

comment:19 Changed 3 years ago by cactus

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's Id, 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: suppose First occured in the right-hand side of foo; how would we know what type to give it, if all we have at hand is the PatSyn for First?

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.

comment:20 Changed 3 years ago by cactus

Keywords: PatternSynonyms added; pattern synonyms removed

comment:21 Changed 3 years ago by thoughtpolice

Milestone: 7.10.17.12.1

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.

comment:22 Changed 3 years ago by dmcclean

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.

comment:23 Changed 3 years ago by dmcclean

Cc: douglas.mcclean@… added

comment:24 Changed 3 years ago by rwbarton

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?

comment:25 Changed 3 years ago by mpickering

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?

comment:26 Changed 3 years ago by dmcclean

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.

comment:27 Changed 3 years ago by simonpj

Interesting. Gergo, what's the status on this ticket? Done, or incomplete?

Simon

comment:28 Changed 2 years ago by thoughtpolice

Milestone: 7.12.18.0.1

Milestone renamed

comment:29 Changed 22 months ago by mpickering

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

  1. I hope this two stage type checking could be simplified, it's something I want to eventually look at.
  2. 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?

comment:30 Changed 22 months ago by mpickering

Blocked By: 5144 removed
Cc: douglas.mcclean@… removed
Description: modified (diff)
Summary: Add support for explicitly-bidirectional pattern synonymsPattern synonym used in an expression context could have different constraints to pattern used in a pattern context

comment:31 Changed 22 months ago by mpickering

Description: modified (diff)

comment:32 Changed 22 months ago by mpickering

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 modify ValBindsOut to use a new datatype instead of HsBinds, split apart the pat syn when calculating sccs and then stitch it back together after typechecking if that is still necessary.

comment:33 Changed 22 months ago by mpickering

This plan runs into problems as we can't given the matcher and builder different Names 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.

comment:34 Changed 22 months ago by simonpj

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.

comment:35 Changed 21 months ago by thomie

Milestone: 8.0.1

comment:36 Changed 20 months ago by mpickering

Cc: mpickering added

comment:37 in reply to:  34 Changed 15 months ago by dfeuer

Replying to simonpj:

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

I respectfully disagree. Pattern synonyms are not, and likely will never be, written by many beginners. And very few programmers are likely to need to write terribly many of them. I think, therefore, that making the type checker enforce some sort of "reasonableness" on them is a considerably lower priority than making them powerful enough to do what librarians need them to do. I ran into this yesterday writing a pattern synonym for Edward Yang's NF type (in the nf package), which needs a constraint on construction but not on matching.

comment:38 Changed 15 months ago by goldfire

While we're at this, there is another outstanding issue: a pattern synonym type should give some indication of the synonym's directionality.

I think there are two quite separable questions here:

  1. What features do we want GHC to support?
  2. What concrete syntax will support those features?

Let's tackle these design questions in order.

For (1) the fundamental question seems to be:

1a. What relationship between the expression-type and the pattern-type do we wish to require?

Possible answers:

  1. None at all.
  2. The types have the same structure, but perhaps different constraints.
  3. Something in between. For example, both have to have the same arity and/or the same head of the result type.

Personally, I think only A or B is defensible here. Furthermore, I favor A. History has shown that Haskellers like as much freedom to explore as possible. There is no type safety issue at hand. So let's give people more rope. I wager the idea of one symbol having two different types (in two very-easy-to-distinguish contexts) is less confusing than, say, kind polymorphism.

Now, onto design point (2). I wonder if it's helpful to think of pattern synonym types as a (PatternType, Maybe Type). The first component is a pattern-type, with its separate provided and required contexts, etc. It classifies the pattern synonym when used as a pattern. The second component is (perhaps) the type of the pattern synonym when used as an expression. This component is missing, naturally, when the synonym is unidirectional. Note that this component (when it exists) is just a normal type.

Typically, the second component can be constructed in a straightforward manner from the first (if the synonym is bidirectional). But it need not be.

Thinking along these lines, I propose the following rules for syntax:

  1. pattern <Pat> :: <PatternType>, when written outside of a -boot file, sets the first component of the type. It also sets the second component of the type when there is no separate type signature for <Pat> and when the pattern is declared to be bidirectional.
  1. <Pat> :: Type can be written to set the second component of a pattern synonym type.
  1. In a -boot file, a pattern <Pat> :: <PatternType> sets only the first component of a pattern synonym type. If you want a bidirectional pattern synonym, write two signatures.

Note that point (2) creates something like a top-level signature (the kind we use all the time when defining functions) but for a capitalized (or :-prefixed) identifier. As far as I can tell, this is a new spot in the grammar (ignoring "naked" top-level declaration splices that consist of one identifier followed by a type annotation, which conflict with normal type signatures, anyway).

What do we think? Please consider addressing design point (1) separately from design point (2), as I think that will simplify the discussion.

comment:39 in reply to:  38 ; Changed 15 months ago by dfeuer

Replying to goldfire:

  1. None at all.

I'm very much in favor of A. See also #11646.

Now, onto design point (2). I wonder if it's helpful to think of pattern synonym types as a (PatternType, Maybe Type).

I think what we actually want (borrowing from the these package) is These PatternType Type. That is, either just the pattern, just the constructor, or both.

comment:40 in reply to:  39 ; Changed 15 months ago by goldfire

Replying to dfeuer:

I think what we actually want (borrowing from the these package) is These PatternType Type. That is, either just the pattern, just the constructor, or both.

But this idea opens up a new, heretofore undiscussed possibility, that of a pattern synonym that cannot be used as a pattern. In other words, it would just be a normal Haskell variable, except with a capitalized identifier. I personally think this is one bridge too far, encouraging people to use a capitalized word for ordinary functions. I think this would be confusing, and for what benefit?

comment:41 in reply to:  40 ; Changed 15 months ago by dfeuer

Replying to goldfire:

But this idea opens up a new, heretofore undiscussed possibility, that of a pattern synonym that cannot be used as a pattern. In other words, it would just be a normal Haskell variable, except with a capitalized identifier. I personally think this is one bridge too far, encouraging people to use a capitalized word for ordinary functions. I think this would be confusing, and for what benefit?

It emphasizes the orthogonality of pattern synonyms and constructor synonyms; I tend to find orthogonal features easier to understand. The current reuse of the where keyword to add a constructor synonym is also troubling. It would feel cleaner to me to let these be completely separate declarations.

BTW, what ever happened to the idea of letting a module re-export a type and associate pattern synonyms with it? I lost track of that and haven't had a chance to upgrade to 8.0 yet.

comment:42 in reply to:  41 Changed 15 months ago by goldfire

Replying to dfeuer:

[Allowing an expression-only "pattern synonym"] emphasizes the orthogonality of pattern synonyms and constructor synonyms; I tend to find orthogonal features easier to understand. The current reuse of the where keyword to add a constructor synonym is also troubling. It would feel cleaner to me to let these be completely separate declarations.

OK. I still don't want this feature, but I understand your reason.

BTW, what ever happened to the idea of letting a module re-export a type and associate pattern synonyms with it? I lost track of that and haven't had a chance to upgrade to 8.0 yet.

This is implemented, as described (very briefly) in the second half of this section of the user manual.

comment:43 in reply to:  38 ; Changed 15 months ago by dfeuer

If we let the constructor have its own signature, can we drop the whole required constraints bit? If so, I think that would make things considerably less confusing.

comment:44 in reply to:  43 Changed 15 months ago by cactus

Replying to dfeuer:

If we let the constructor have its own signature, can we drop the whole required constraints bit? If so, I think that would make things considerably less confusing.

But the required constraints don't come from builders; a unidirectional pattern synonym can have just as much of a required context. The simplest example I can think of is

pattern P x <- (f -> x)

Here, any constraint of f on its argument's type will be a required constraint in P's type.

(Note that a special case of this is matching against overloaded literals, e.g. pattern Z = 0, which requires (Num a, Eq a).)

comment:45 Changed 14 months ago by goldfire

The idea in comment:39 has grown on me. So let me turn this into a concrete proposal:

  1. Relax Haskell's current restriction around capitalized identifiers. That is, any old variable can now begin with a capitalized letter or a colon. Capitalized variables can be defined only by function-definition syntax, never by patterns. That is, Foo = 5 is OK, as is Bar x = x + 2. On the other hand, Just Quux = listToMaybe blurgh would not be OK.
  1. Unidirectional pattern synonyms remain unchanged.
  1. If a bidirectional (whether implicitly bidirectional or explicitly bidirectional) pattern synonym is defined in a module, and that module defines no variable of the same (capitalized) name as the pattern, then the pattern synonym declaration also serves as a declaration of the capitalized identifier. The type of the capitalized identifier will be derived from the type of the pattern synonym, concatenating the required and provided contexts.
  1. A pattern synonym signature in a -boot file declares only the pattern synonym, not the capitalized identifier.
  1. Export and import of capitalized identifiers will need a new keyword prefix in export/import lists. I propose constructor, analogous to pattern today.
  1. Exporting/importing a pattern synonym with an implicitly-declared capitalized identifier associated with it will also export/import that capitalized identifier. This is mostly for backward compatibility, but it also seems quite convenient.

What do we think? Some of this design is motivated by backward compatibility with existing pattern synonyms -- we could imagine having pattern synonyms always be unidirectional and asking users to declare both ways explicitly. But this is also inconvenient for the common case. I think this proposal balances the different needs nicely. It also suggests that we can do away entirely with "builders" in the implementation, as a capitalized identifier is just a normal variable.

comment:46 in reply to:  45 Changed 14 months ago by dfeuer

Replying to goldfire:

The idea in comment:39 has grown on me. So let me turn this into a concrete proposal:

  1. Relax Haskell's current restriction around capitalized identifiers. That is, any old variable can now begin with a capitalized letter or a colon. Capitalized variables can be defined only by function-definition syntax, never by patterns. That is, Foo = 5 is OK, as is Bar x = x + 2. On the other hand, Just Quux = listToMaybe blurgh would not be OK.

I like the general theme very much, but I think we use the constructor keyword to introduce capitalized identifiers as well as to export them unbundled. This distinguishes them syntactically from pattern bindings and makes it immediately obvious that something strange is happening. I agree that we don't need to allow them to be defined using pattern bindings; that would complicate things with little benefit.

comment:47 Changed 14 months ago by dmcclean

Does this proposed use of constructor as a keyword conflict with the use proposed in #11080?

comment:48 in reply to:  47 Changed 14 months ago by dfeuer

Replying to dmcclean:

Does this proposed use of constructor as a keyword conflict with the use proposed in #11080?

I doubt it. This use would never come after data.

comment:49 Changed 11 months ago by lelf

Cc: lelf added

comment:50 Changed 5 months ago by liyang

Cc: liyang added
Note: See TracTickets for help on using tickets.