Opened 4 years ago

Last modified 2 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, RyanGlScott, Shayan-Najd
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 (18)

comment:1 Changed 4 years ago by cactus

Type: bugfeature request

comment:2 Changed 3 years ago by cactus

Cc: cactus added
Keywords: pattern synonyms added

comment:3 Changed 3 years ago by cactus

Keywords: PatternSynonyms added; pattern synonyms removed

comment:4 Changed 2 years ago by bgamari

Description: modified (diff)

comment:5 Changed 2 years ago by bgamari

Description: modified (diff)

comment:6 Changed 2 years 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 2 years 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 2 years 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 23 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 22 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 22 months ago by goldfire

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

comment:12 Changed 14 months ago by RyanGlScott

Cc: RyanGlScott added

comment:13 Changed 9 months 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

comment:14 Changed 3 months ago by carter

I too would like this. My goal/motivation would be to use data families to have smart strict unboxed datatypes with uniform syntax.

comment:15 Changed 3 months ago by Shayan-Najd

Cc: Shayan-Najd added

comment:16 Changed 3 months ago by Shayan-Najd

I am writing to resurrect this ticket!

Nowadays, we can use COMPLETE pragmas to group together an arbitrary collection of synonyms.

Why not also grouping the so called polymorphic pattern synonyms under type classes and having the totality condition derived from the association?

Last edited 3 months ago by Shayan-Najd (previous) (diff)

comment:17 Changed 3 months ago by goldfire

Given our new ghc-proposals process, I think this should go via that route. The process seems to working well, and I know I have benefited through submitting my own proposals there and getting helpful feedback.

comment:18 Changed 2 months ago by Iceland_jack

Quick reminder: I need this to work with GND. Using an Int instance of the above class

deriving anyclass instance HasZero Int

I want to be able to derive (newtype, not anyclass)

newtype USD = USD Int
  deriving newtype
-- instance HasZero USD where
--   pattern Zero :: USD
--   pattern Zero <- (coerce -> Zero::Int)
--     where Zero = coerce (Zero::Int)

Unboxed values as well.

Last edited 2 months ago by Iceland_jack (previous) (diff)
Note: See TracTickets for help on using tickets.