Opened 3 years ago

Last modified 10 months ago

#9793 new feature request

Some as-patterns could be accepted in pattern synonyms

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

Description

Currently all as-patterns are rejected in pattern synonym definitions, to avoid situations like

pattern P x y <- x@(y:_)

since there's no valid reason to be able to then write something like

f [True] False = ...

this would just lead to confusion.

However, I think we could accept as-patterns where the body of the as-pattern doesn't contain any variable bindings that are accessible via the pattern synonym. In other words, this should be OK:

pattern P x <- x@(y:_)

since it's exactly equivalent to

pattern P x <- x@(_:_)

which I don't think is as confusing as the other example.

I haven't really made up my mind yet if these should be bidirectional; but they certainly could be, by just ignoring the body of the as-pattern in the wrapper; so the following two would be equivalent:

pattern P1 x = [x@(y:_)]
pattern P2 x <- [x@(y:_)]
  where
    P2 x = [x]

Change History (11)

comment:1 Changed 3 years ago by cactus

Keywords: PatternSynonyms added; pattern synonyms removed

comment:2 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:3 Changed 2 years ago by thoughtpolice

Milestone: 7.12.18.0.1

Milestone renamed

comment:4 Changed 2 years ago by mpickering

Differential Rev(s): Phab:D1666
Status: newpatch

comment:5 Changed 2 years ago by simonpj

Hang on. What is the design here? Specifically, what is the semantics of matching?

To put it another way, suppose I have

pattern P x <- x@(Right _)

What does it mean to match against that?

Well, to a first approximation, in a pattern, P pat means the same as <rhs of P> with pat instead of x. So

f (P (Left y)) = e

means

f ((Left y)@(Right _)) = e

And what does that mean?

Perhaps we could expand the semantics of as-patterns to be p1 @ p2, meaning match against both p1 and p1. An "and-pattern" if you like. Now everything would be well-specified. And I suppose you could say things like

f ((\xs -> length xs < 10) -> True)@(y:_) = ...

which would match against a list of length shorter than 10, and then bind 'y' to the head of that list.

But this is a bigger change, and not directly related to pattern synonyms.

So far I'm unconvinced.

Simon

comment:6 Changed 2 years ago by Simon Peyton Jones <simonpj@…>

In 48e0634/ghc:

Revert "Allow as-patterns in pattern synonym declarations."

I'm reverting this until we agree a design.
See comment:5 in Trac #9793.

Incidentally the reference to Trac #9739 in the reverted
patch is bogus; it shold have said #9793.

This reverts commit 44640af7afa1a01ff2e2357f7c1436b4804866fc.

comment:7 Changed 2 years ago by simonpj

Milestone: 8.0.18.2.1

comment:8 Changed 20 months ago by mpickering

Owner: cactus deleted

comment:9 Changed 20 months ago by mpickering

Keywords: newcomer added

comment:10 Changed 13 months ago by bgamari

Status: patchnew

comment:11 Changed 10 months ago by rwbarton

Keywords: newcomer removed
Milestone: 8.2.18.4.1
Note: See TracTickets for help on using tickets.