Opened 3 years ago

Last modified 8 days ago

#8583 new feature request

Associated pattern synonyms

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

Description (last modified by bgamari)

The PatternSynonyms wiki page has a section on (typeclass-)associated pattern synonyms:

class ListLike l where
      pattern Nil :: l a
      pattern Cons :: a -> l a -> a
      isNil :: l a -> Bool
      isNil Nil = True
      isNil (Cons _ _) = False
      append :: l a -> l a -> l a

instance ListLike [] where
      pattern Nil = []
      pattern Cons x xs = x:xs
      append = (++)

headOf :: (ListLike l) => l a -> Maybe a
headOf Nil = Nothing
headOf (Cons x _) = Just x

Change History (13)

comment:1 Changed 3 years ago by cactus

Type: bugfeature request

comment:2 Changed 2 years ago by cactus

Cc: cactus added
Keywords: pattern synonyms added

comment:3 Changed 2 years ago by cactus

Keywords: PatternSynonyms added; pattern synonyms removed

comment:4 Changed 20 months ago by bgamari

Description: modified (diff)

comment:5 Changed 20 months ago by bgamari

Description: modified (diff)

comment:6 Changed 17 months ago by rwbarton

Cc: carter added

Definitely would be useful, but this might require a new implementation strategy since it gives pattern synonyms essentially first-class status, right?

comment:7 Changed 17 months ago by goldfire

Yes yes yes. I want this!

But it's tricky, even forgetting about implementation for the moment. Let's pretend that all types have to be explicit for a sec, and I'll continue the example from the original post:

headOfList :: forall a. [a] -> Maybe a
headOfList (Nil @[] @a) = Nothing @a
headOfList (Cons @[] @a x _) = Just x

There's something very strange going on here. It looks, in those patterns, that we're pattern-matching on a type. This, of course, is not allowed, because types are erased. Upon further inspection, we're not really doing this. The first type parameter to Nil and Cons are inputs. Contrast to the second type parameter and the term parameters (to Cons), which are outputs.

Another way to see this is to think about how Nil @[] @a and Nil @Seq @a are both valid patterns, but Nil @l @Int would be terrible, as it requires doing a type check at runtime.

So I wonder if implementing this without terrible hacks might depend on PatternFamilies which (despite its name) allows for a mix of inputs and outputs in pattern synonyms.

comment:8 Changed 17 months ago by nomeata

Upon further inspection, we're not really doing this. The first type parameter to Nil and Cons are inputs

This seems to be #9671 in disguise.

comment:9 Changed 14 months ago by Iceland_jack

This can also be faked using prisms and pattern synonyms: reddit comment.

For visible type application in patterns per Richard's comment see #11350.

comment:10 Changed 13 months ago by rwbarton

See #11461 for how to approximate this feature in current GHC.

Richard, how does your comment:7 apply here? Or to the example in #11224? The status quo seems to be that type arguments are "inputs", rather than "outputs", of the pattern synonym.

comment:11 Changed 13 months ago by goldfire

I retract comment:7. I have no idea what I was thinking.

comment:12 Changed 5 months ago by RyanGlScott

Cc: RyanGlScott added

comment:13 Changed 8 days ago by Iceland_jack

If this gets implement, please consider default associated patterns

class HasZero n where 
  pattern Zero :: n

  default pattern Zero :: (Num n, Eq n) => n
  pattern Zero = 0
Note: See TracTickets for help on using tickets.