Providence Salumu PatternSynonyms – GHC
wiki:PatternSynonyms

Pattern Synonyms

Most language entities in Haskell can be named so that they can be abbreviated instead of written out in full. This proposal provides the same power for patterns. See the implementation page for implementation details.

Tickets should include PatternSynonyms in their Keywords to appear in these summary lists.

Open Tickets:

#8581
Pattern synonym used in an expression context could have different constraints to pattern used in a pattern context
#8583
Associated pattern synonyms
#8779
Exhaustiveness checks for pattern synonyms
#9671
Allow expressions in patterns
#9793
Some as-patterns could be accepted in pattern synonyms
#10783
Partial type signatures should work in pattern synonym signatures
#11212
Should be more liberal parsing pattern synonyms with view patterns
#11228
Interaction between ORF and record pattern synonyms needs to be resolved.
#11350
Allow visible type application in patterns
#11368
Pattern synonym name is mangled when patterns are non-exhaustive
#11461
Allow pattern synonyms to be bundled with type classes?
#11646
Make pattern synonym export type mismatch a warning
#11655
Ambiguous types in pattern synonym not determined by functional dependencies
#11955
Haddock documentation for pattern synonyms printed with explicit forall quantifiers
#11959
Importing doubly exported pattern synonym and associated pattern synonym panics
#11993
RFC, allow local bindings in pattern synonyms
#12006
Can't infer constraint of pattern synonyms
#12025
Order of constraints forced (in pattern synonyms, type classes in comments)
#12178
Allow inline pragmas on pattern synonyms
#12179
Incorrect parsing of a pattern synonym type
#12187
Clarify the scoping of existentials for pattern synonym signatures
#12203
Allow constructors on LHS of (implicit) bidirectional pattern synonym
#12426
Allow smart constructors their own types
#12429
Pattern synonym parse error should recommend enabling extension
#12448
Allow partial application of bidirectional pattern synonyms
#12975
Suggested type signature for a pattern synonym causes program to fail to type check
#13018
TH-spliced pattern synonym declaration fails to typecheck
#13042
Allow type annotations / visible type application in pattern synonyms

There is a list of closed tickets at the bottom of the page.

Motivating example

Here is a simple representation of types

    data Type = App String [Type]

Using this representations the arrow type looks like App "->" [t1, t2]. Here are functions that collect all argument types of nested arrows and recognize the Int type:

   collectArgs :: Type -> [Type]
   collectArgs (App "->" [t1, t2]) = t1 : collectArgs t2
   collectArgs _ = []

   isInt (App "Int" []) = True
   isInt _ = False

Matching on App directly is both hard to read and error prone to write.

The proposal is to introduce a way to give patterns names:

   pattern Arrow t1 t2 = App "->" [t1, t2]
   pattern Int = App "Int" []

And now we can write

   collectArgs :: Type -> [Type]
   collectArgs (Arrow t1 t2) = t1 : collectArgs t2
   collectArgs _ = []

   isInt Int = True
   isInt _ = False

Here is a second example from pigworker on Reddit. Your basic sums-of-products functors can be built from this kit.

newtype K a        x  = K a
newtype I          x  = I x
newtype (:+:) f g  x  = Sum (Either (f x) (g x))
newtype (:*:) f g  x  = Prod (f x, g x)

and then you can make recursive datatypes via

newtype Fix f = In (f (Fix f))

e.g.,

type Tree = Fix (K () :+: (I :*: I))

and you can get useful generic operations cheaply because the functors in the kit are all Traversable, admit a partial zip operation, etc.

You can define friendly constructors for use in expressions

leaf :: Tree
leaf = In (Sum (Left (K ())))
node :: Tree -> Tree -> Tree
node l r = In (Sum (Right (Prod (I l, I r))))

but any Tree-specific pattern matching code you write will be wide and obscure. Turning these definitions into pattern synonyms means you can have both readable type-specific programs and handy generics without marshalling your data between views.

Uni-directional (pattern-only) synonyms

The simplest form of pattern synonyms is the one from the examples above. The grammar rule is:

pattern conid varid1 ... varidn <- pat

pattern varid1 consym varid2 <- pat

  • Each of the variables on the left hand side must occur exactly once on the right hand side
  • Pattern synonyms are not allowed to be recursive. Cf. type synonyms.

There have been several proposals for the syntax of defining pattern-only synonyms:

  • pattern conid varid1 ... varidn ~ pat
  • pattern conid varid1 ... varidn := pat
  • pattern conid varid1 ... varidn -> pat
  • pattern conid varid1 ... varidn <- pat

Pattern synonyms can be exported and imported by prefixing the conid with the keyword pattern:

   module Foo (pattern Arrow) where ...

This is required because pattern synonyms are in the namespace of constructors, so it's perfectly valid to have

   data P = C
   pattern P = 42

You may also give a type signature for a pattern, but as with most other type signatures in Haskell it is optional:

pattern conid :: type

E.g.

   pattern Arrow :: Type -> Type -> Type
   pattern Arrow t1 t2 <- App "->" [t1, t2]

Together with ViewPatterns we can now create patterns that look like regular patterns to match on existing (perhaps abstract) types in new ways:

import qualified Data.Sequence as Seq

pattern Empty <- (Seq.viewl -> Seq.EmptyL)
pattern x :< xs <- (Seq.viewl -> x Seq.:< xs)
pattern xs :> x <- (Seq.viewr -> xs Seq.:> x)

Simply-bidirectional pattern synonyms

In cases where pat is in the intersection of the grammars for patterns and expressions (i.e. is valid both as an expression and a pattern), the pattern synonym can be made bidirectional, and can be used in expression contexts as well. Bidirectional pattern synonyms have the following syntax:

pattern conid varid1 ... varidn = pat

pattern varid1 consym varid2 = pat

For example, the following two pattern synonym definitions are rejected, because they are not bidirectional (but they would be valid as pattern-only synonyms)

   pattern ThirdElem x = _:_:x:_
   pattern Snd y = (x, y)

since the right-hand side is not a closed expression of {x} and {y} respectively.

In contrast, the pattern synonyms for Arrow and Int above are bidirectional, so you can e.g. write:

   arrows :: [Type] -> Type -> Type
   arrows = flip $ foldr Arrow

Explicitly-bidirectional pattern synonyms

What if you want to use Succ in an expression:

    pattern Succ n <- n1 | let n = n1 -1, n >= 0

It's clearly impossible since its expansion is a pattern that has no meaning as an expression. Nevertheless, if we want to make what looks like a constructor for a type we will often want to use it in both patterns and expressions. This is the rationale for the most complicated synonyms, the bidirectional ones. They provide two expansions, one for patterns and one for expressions.

pattern conid varid1 ... varidn <- pat where cfunlhs rhs

where cfunlhs is like funlhs, except that the functions symbol is a conid instead of a varid.

Example:

   pattern Succ n <- n1 | let n = n1-1, n >= 0 where
      Succ n = n + 1

TODO: Rewrite this example to not use ViewPatternsAlternative

The first part as is before and describes the expansion of the synonym in patterns. The second part describes the expansion in expressions.

   fac 0 = 0
   fac (Succ n) = Succ n * fac n 

Associated pattern synonyms

Just like data types and type synonyms can be part of a class declaration, it would be possible to have pattern synonyms as well.

Example:

   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

One could go one step further and leave out the pattern keyword to obtain associated constructors, which are required to be bidirectional. The capitalized identifier would indicate that a pattern synonym is being defined. For complicated cases one could resort to the where syntax (shown above).

TODO: Syntax for associated pattern synonym declarations to discern between pattern-only and bidirectional pattern synonyms

Static semantics

A unidirectional pattern synonym declaration has the form

pattern P var1 var2 ... varN <- pat

The formal pattern synonym arguments var1, var2, ..., varN are brought into scope by the pattern pat on the right-hand side. The declaration brings the name P as a pattern synonym into the module-level scope.

The pattern synonym P is assigned a pattern type of the form

pattern P :: CProv => CReq => t1 -> t2 -> ... -> tN -> t 

where t1, ..., tN are the types of the parameters var1, ..., varN, t is the simple type (with no context) of the thing getting matched, and CReq and CProv are type contexts.

CReq can be omitted if it is empty. If CProv is empty, but CReq is not, () is used. The following example shows cases:

data Showable where
    MkShowable :: (Show a) => a -> Showable

-- Required context is empty
pattern Sh :: (Show a) => a -> Showable
pattern Sh x <- MkShowable x

-- Provided context is empty, but required context is not
pattern One :: () => (Num a, Eq a) => a
pattern One <- 1

A pattern synonym can be used in a pattern if the instatiated (monomorphic) type satisfies the constraints of CReq. In this case, it extends the context available in the right-hand side of the match with CProv, just like how an existentially-typed data constructor can extend the context.

As with function and variable types, the pattern type signature can be inferred, or it can be explicitly written out on the program.

Here's a more complex example. Let's look at the following definition:

{-# LANGUAGE PatternSynonyms, GADTs, ViewPatterns #-}
module ShouldCompile where

data T a where
	MkT :: (Eq b) => a -> b -> T a

f :: (Show a) => a -> Bool

pattern P x <- MkT (f -> True) x

Here, the inferred type of P is

pattern P :: (Eq b) => (Show a) => b -> T a

A bidirectional pattern synonym declaration has the form

pattern P var1 var2 ... varN = pat

where both of the following are well-typed declarations:

pattern P1 var1 var2 ... varN <- pat

P2 = \var1 var2 ... varN -> pat

In this case, the pattern type of P is simply the pattern type of P1, and its expression type is the type of P2. The name P is brought into the module-level scope both as a pattern synonym and as an expression.

Dynamic semantics

A pattern synonym occurance in a pattern is evaluated by first matching against the pattern synonym itself, and then on the argument patterns. For example, given the following definitions:

pattern P x y <- [x, y]

f (P True True) = True
f _             = False

g [True, True] = True
g _            = False

the behaviour of f is the same as

f [x, y] | True <- x, True <- y = True
f _                             = False

Because of this, the eagerness of f and g differ:

*Main> f (False:undefined)
*** Exception: Prelude.undefined
*Main> g (False:undefined)
False

This is because we generate the matching function at the definition site.

Typed pattern synonyms

So far patterns only had syntactic meaning. In comparison Ωmega has typed pattern synonyms, so they become first class values. For bidirectional pattern synonyms this seems to be the case

data Nat = Z | S Nat deriving Show
pattern Ess p = S p

And it works:

*Main> map S [Z, Z, S Z]
[S Z,S Z,S (S Z)]
*Main> map Ess [Z, Z, S Z]
[S Z,S Z,S (S Z)]

Branching pattern-only synonyms

N.B. this is a speculative suggestion!

Sometimes you want to match against several summands of an ADT simultaneously. E.g. in a data type of potentially unbounded natural numbers:

data Nat = Zero | Succ Nat
type UNat = Maybe Nat -- Nothing meaning unbounded

Conceptually Nothing means infinite, so it makes sense to interpret it as a successor of something. We wish it to have a predecessor just like Just (Succ Zero)!

I suggest branching pattern synonyms for this purpose:

pattern S pred <- pred@Nothing | pred@(Just a <- Just (Succ a))
pattern Z = Just Zero

Here pred@(Just a <- Just (Succ a)) means that the pattern invocation S pred matches against Just (Succ a) and - if successful - binds Just a to pred.

This means we can syntactically address unbound naturals just like bounded ones:

greetTimes :: UNat -> String -> IO ()
greetTimes Z _ = return ()
greetTimes (S rest) message = putStrLn message >> greetTimes rest message

As a nice collateral win this proposal handles pattern Name name <- Person name workplace | Dog name vet too.

Record Pattern Synonyms

See PatternSynonyms/RecordPatternSynonyms

Associating synonyms with types

See PatternSynonyms/AssociatingSynonyms

Closed Tickets

Closed Tickets:

#5144
Pattern synonyms
#8582
Record syntax for pattern synonyms
#8584
Pattern synonym type signatures
#8749
Pattern synonyms crash GHCi
#8761
Make pattern synonyms work with Template Haskell
#8841
PatternSynonyms error gives wrong source locations
#8968
Pattern synonyms and GADTs
#9161
Pattern synonyms interact badly with data kinds
#9226
Internal error when using equality constraint in pattern synonyms
#9417
Pattern synonyms across modules broken in Haddock
#9514
Haddock panics when exporting a module with pattern synonyms
#9705
Panic on a pattern synonym in a class
#9732
Pattern synonyms and unboxed values
#9783
Pattern synonym matcher is unnecessarily strict on unboxed continuations
#9803
Poor error message for unbound variable in pattern synonym
#9867
PatternSynonyms + ScopedTypeVariables triggers an internal error
#9889
Pattern synonym does not work in top-level pattern bind
#9891
Fixity declarations for pattern synonyms not persisted
#9900
Support pattern synonyms in GHCi
#9911
Pattern synonyms with no signatures should yield warnings
#9953
Pattern synonyms don't work with GADTs
#9954
Required constraints are not inferred for pattern synonyms involving GADTs
#9967
Pattern synonym type signature documentation out of date
#9975
RecordWildcards and PatternSynonyms cause impossible bug
#10339
PatternSynonyms confuse exhaustiveness check
#10404
GHC panic when creating a monomorphised pattern synonym for GADT
#10426
matchGroupArity panic with PatternSynonyms
#10653
PatternSynonyms should be imported/exported as part of the wildcard notation
#10747
Infix pattern synonyms fail to parse (regression)
#10873
Bad error message for incorrect pattern synonym signature
#10897
Incorrect ASSERT for buildPatSyn
#10997
Pattern synonym causes Iface error.
#11039
Panic with incorrect pattern synonym signature
#11213
Incorrect reported pattern synonym signature
#11224
Program doesn't preserve semantics after pattern synonym inlining.
#11225
Unable to provide type signature for pattern synonym
#11227
Interaction between ORF and record pattern synonyms needs to be resolved.
#11233
Improve optimisation of pattern synonym matching
#11283
PatternSynonms and DisambiguateRecordFields causes panic
#11336
GHC craches on this combination of ViewPatterns and PatternSynonyms
#11351
Scoped type variables in pattern synonyms
#11367
[Regression] Only one clause allowed in (explicitly bidirectional) pattern synonyms
#11524
Something is amiss with quantification in pattern synonym type signatures
#11633
Record field order in a bidirectional pattern synonym match is order dependent
#11667
Incorrect pattern synonym types in error messages
#11727
Allow one type signature for multiple pattern synonyms
#11728
Core lint errors
#11977
ghc doesn't agree with its own inferred pattern type
#11985
Core lint error on record syntax update/pattern synonym
#11986
Record fields not defined with pattern synonym in ghci
#11987
Allow record wildcards with pattern synonyms which are defined in GHCi
#12007
Panic when loading file with nested pattern synonyms into ghci
#12017
GHC panics on pattern synonym ‘kindPrimRep’
#12024
GHC leaks GHC.Prim.~# into type
#12061
Allow duplicate record fields in pattern synonyms
#12094
Unlifted types and pattern synonym signatures
#12101
Regression: Pattern synonyms make GHCi 8.0.1 crash
#12108
Function type synonym fails in pattern synonym
#12109
Matching on pattern synonym succeeds compiled with ghc, fails with ghci
#12153
Bug in pattern synonyms with template haskell
#12165
Multiple pattern type signatures accepted
#12166
Pattern synonym existential variable confusion
#12366
Use TypeOperators for pattern synonyms?
#12456
Panics when making a quotation as pattern synonym
#12489
undefined in view pattern inside pattern synonym causes GHC to panic
#12548
Exported pattern synonyms does not mark top-level bindings in RHS as used
#12615
Record pattern synonyms cause spurious name shadowing warnings
#12697
Improve output of pattern synonym info
#12698
GHC panic on pattern synonym
#12746
Assertion failed with BuildFlavour = devel2 (one more)
#12767
Pattern synonyms for Cont, Writer, Reader, State, ...
#12872
Pattern synonyms allow multiple type signatures but only use the first
#13022
Pattern Synonyms using other synonyms causes ghc panic

Last modified 7 months ago Last modified on Jun 12, 2016 10:34:36 AM
Providence Salumu