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

[cactus]

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.

[ntc2]

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

[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 _ = _

[dfranke]

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

[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]

[cactus]

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

[hvr]

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

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

[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

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

[simonpj]

Re-opening because of comment:9 and following.

Simon

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

[simonpj]

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

[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

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

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

[thoughtpolice]

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.

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

[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?

[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?

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

[simonpj]

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

Simon

[thoughtpolice]

Milestone renamed

[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?

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

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

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

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

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

2. <Pat> :: Type can be written to set the second component of a pattern synonym type.

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

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

[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?

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

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

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

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

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

2. Unidirectional pattern synonyms remain unchanged.

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

4. A pattern synonym signature in a -boot file declares only the pattern synonym, not the capitalized identifier.

5. Export and import of capitalized identifiers will need a new keyword prefix in export/import lists. I propose constructor, analogous to pattern today.

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

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

[dmcclean]

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

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