Opened 3 years ago

Last modified 7 months ago

#8583 new feature request

Associated pattern synonyms

Reported by: cactus Owned by:
Priority: normal Milestone:
Component: Compiler Version:
Keywords: PatternSynonyms Cc: cactus, carter
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 (11)

comment:1 Changed 3 years ago by cactus

  • Type changed from bug to feature request

comment:2 Changed 22 months ago by cactus

  • Cc cactus added
  • Keywords pattern synonyms added

comment:3 Changed 21 months ago by cactus

  • Keywords PatternSynonyms added; pattern synonyms removed

comment:4 Changed 14 months ago by bgamari

  • Description modified (diff)

comment:5 Changed 14 months ago by bgamari

  • Description modified (diff)

comment:6 Changed 11 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 11 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 11 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 8 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 7 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 7 months ago by goldfire

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

Note: See TracTickets for help on using tickets.