Opened 2 years ago

Last modified 8 weeks 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 (8)

comment:1 Changed 2 years ago by cactus

  • Type changed from bug to feature request

comment:2 Changed 13 months ago by cactus

  • Cc cactus added
  • Keywords pattern synonyms added

comment:3 Changed 12 months ago by cactus

  • Keywords PatternSynonyms added; pattern synonyms removed

comment:4 Changed 5 months ago by bgamari

  • Description modified (diff)

comment:5 Changed 5 months ago by bgamari

  • Description modified (diff)

comment:6 Changed 8 weeks 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 8 weeks 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 8 weeks 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.

Note: See TracTickets for help on using tickets.