summaryrefslogtreecommitdiff
path: root/docs/users_guide/exts/pattern_synonyms.rst
blob: fbdd50d0830c33c45d8aae26db39f5ae897bd9e3 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
.. _pattern-synonyms:

Pattern synonyms
================

.. extension:: PatternSynonyms
    :shortdesc: Enable pattern synonyms.

    :since: 7.8.1

    Allow the definition of pattern synonyms.

Pattern synonyms are enabled by the language extension :extension:`PatternSynonyms`, which is
required for defining them, but *not* for using them. More information and
examples of pattern synonyms can be found on the :ghc-wiki:`Wiki page <pattern-synonyms>`.

Pattern synonyms enable giving names to parametrized pattern schemes.
They can also be thought of as abstract constructors that don't have a
bearing on data representation. For example, in a programming language
implementation, we might represent types of the language as follows: ::

    data Type = App String [Type]

Here are some examples of using said representation. Consider a few
types of the ``Type`` universe encoded like this: ::

      App "->" [t1, t2]          -- t1 -> t2
      App "Int" []               -- Int
      App "Maybe" [App "Int" []] -- Maybe Int

This representation is very generic in that no types are given special
treatment. However, some functions might need to handle some known types
specially, for example the following two functions collect all argument
types of (nested) arrow types, and recognize the ``Int`` type,
respectively: ::

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

      isInt :: Type -> Bool
      isInt (App "Int" []) = True
      isInt _              = False

Matching on ``App`` directly is both hard to read and error prone to
write. And the situation is even worse when the matching is nested: ::

      isIntEndo :: Type -> Bool
      isIntEndo (App "->" [App "Int" [], App "Int" []]) = True
      isIntEndo _                                       = False

Pattern synonyms permit abstracting from the representation to expose
matchers that behave in a constructor-like manner with respect to
pattern matching. We can create pattern synonyms for the known types we
care about, without committing the representation to them (note that
these don't have to be defined in the same module as the ``Type`` type): ::

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

Which enables us to rewrite our functions in a much cleaner style: ::

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

      isInt :: Type -> Bool
      isInt Int = True
      isInt _   = False

      isIntEndo :: Type -> Bool
      isIntEndo (Arrow Int Int) = True
      isIntEndo _               = False

In general there are three kinds of pattern synonyms. Unidirectional,
bidirectional and explicitly bidirectional. The examples given so far are
examples of bidirectional pattern synonyms. A bidirectional synonym
behaves the same as an ordinary data constructor. We can use it in a pattern
context to deconstruct values and in an expression context to construct values.
For example, we can construct the value `intEndo` using the pattern synonyms
`Arrow` and `Int` as defined previously. ::

      intEndo :: Type
      intEndo = Arrow Int Int

This example is equivalent to the much more complicated construction if we had
directly used the `Type` constructors. ::

      intEndo :: Type
      intEndo = App "->" [App "Int" [], App "Int" []]


Unidirectional synonyms can only be used in a pattern context and are
defined as follows:


::

      pattern Head x <- x:xs

In this case, ``Head`` ⟨x⟩ cannot be used in expressions, only patterns,
since it wouldn't specify a value for the ⟨xs⟩ on the right-hand side. However,
we can define an explicitly bidirectional pattern synonym by separately
specifying how to construct and deconstruct a type. The syntax for
doing this is as follows:

::

      pattern HeadC x <- x:xs where
        HeadC x = [x]

We can then use ``HeadC`` in both expression and pattern contexts. In a pattern
context it will match the head of any list with length at least one. In an
expression context it will construct a singleton list.

Explicitly bidirectional pattern synonyms offer greater flexibility than
implicitly bidirectional ones in terms of the syntax that is permitted. For
instance, the following is not a legal implicitly bidirectional pattern
synonym: ::

      pattern StrictJust a = Just !a

This is illegal because the use of :extension:`BangPatterns` on the right-hand
sides prevents it from being a well formed expression. However, constructing a
strict pattern synonym is quite possible with an explicitly bidirectional
pattern synonym: ::

      pattern StrictJust a <- Just !a where
        StrictJust !a = Just a

Constructing an explicitly bidirectional pattern synonym also:

- can create different data constructors from the underlying data type,
  not just the one appearing in the pattern match;

- can call any functions or conditional logic, especially validation,
  of course providing it constructs a result of the right type;

- can use guards on the lhs of the ``=``;

- can have multiple equations.

For example: ::

      data PosNeg = Pos Int | Neg Int
      pattern Smarter{ nonneg } <- Pos nonneg  where
        Smarter x = if x >= 0 then (Pos x) else (Neg x)

Or using guards: ::

      pattern Smarter{ nonneg } <- Pos nonneg  where
        Smarter x | x >= 0    = (Pos x)
                  | otherwise = (Neg x)

There is an extensive Haskell folk art of `smart constructors
<https://wiki.haskell.org/Smart_constructor>`_,
essentially functions that wrap validation around a constructor,
and avoid exposing its representation.
The downside is that the underlying constructor can't be used as a matcher.
Pattern synonyms can be used as genuinely smart constructors, for both validation and matching.

The table below summarises where each kind of pattern synonym can be used.

+---------------+----------------+---------------+---------------------------+
| Context       | Unidirectional | Bidirectional | Explicitly Bidirectional  |
+===============+================+===============+===========================+
| Pattern       | Yes            | Yes           | Yes                       |
+---------------+----------------+---------------+---------------------------+
| Expression    | No             | Yes (Inferred)| Yes (Explicit)            |
+---------------+----------------+---------------+---------------------------+

.. _record-patsyn:

Record Pattern Synonyms
-----------------------

It is also possible to define pattern synonyms which behave just like record
constructors. The syntax for doing this is as follows:

::

      pattern Point :: Int -> Int -> (Int, Int)
      pattern Point{x, y} = (x, y)

The idea is that we can then use ``Point`` just as if we had defined a new
datatype ``MyPoint`` with two fields ``x`` and ``y``.

::

    data MyPoint = Point { x :: Int, y :: Int }

Whilst a normal pattern synonym can be used in two ways, there are then seven
ways in which to use ``Point``. Precisely the ways in which a normal record
constructor can be used.

=======================================   ==================================
Usage                                     Example
=======================================   ==================================
As a constructor                          ``zero = Point 0 0``
As a constructor with record syntax       ``zero = Point { x = 0, y = 0}``
In a pattern context                      ``isZero (Point 0 0) = True``
In a pattern context with record syntax   ``isZero (Point { x = 0, y = 0 }``
In a pattern context with field puns      ``getX (Point {x}) = x``
In a record update                        ``(0, 0) { x = 1 } == (1,0)``
Using record selectors                    ``x (0,0) == 0``
=======================================   ==================================

For a unidirectional record pattern synonym we define record selectors but do
not allow record updates or construction.

The syntax and semantics of pattern synonyms are elaborated in the
following subsections.
There are also lots more details in the `paper
<https://www.microsoft.com/en-us/research/wp-content/uploads/2016/08/pattern-synonyms-Haskell16.pdf>`_.

See the :ghc-wiki:`Wiki page <pattern-synonyms>` for more
details.

Syntax and scoping of pattern synonyms
--------------------------------------

A pattern synonym declaration can be either unidirectional,
bidirectional or explicitly bidirectional.
The syntax for unidirectional pattern synonyms is: ::

      pattern pat_lhs <- pat

the syntax for bidirectional pattern synonyms is: ::

      pattern pat_lhs = pat

and the syntax for explicitly bidirectional pattern synonyms is: ::

      pattern pat_lhs <- pat where
        pat_lhs = expr                      -- lhs restricted, see below

We can define either prefix, infix or record pattern synonyms by modifying
the form of `pat_lhs`. The syntax for these is as follows:

======= ============================
Prefix  ``Name args``
------- ----------------------------
Infix   ``arg1 `Name` arg2``
        or ``arg1 op arg2``
------- ----------------------------
Record  ``Name{arg1,arg2,...,argn}``
======= ============================

The `pat_lhs` for explicitly bidirectional construction cannot use Record syntax.
(Because the rhs *expr* might be constructing different data constructors.)
It can use guards with multiple equations.

Pattern synonym declarations can only occur in the top level of a
module. In particular, they are not allowed as local definitions.

The variables in the left-hand side of the definition are bound by the
pattern on the right-hand side. For bidirectional pattern
synonyms, all the variables of the right-hand side must also occur on
the left-hand side; also, wildcard patterns and view patterns are not
allowed. For unidirectional and explicitly bidirectional pattern
synonyms, there is no restriction on the right-hand side pattern.

Pattern synonyms cannot be defined recursively.

:ref:`complete-pragma` can be specified in order to tell
the pattern match exhaustiveness checker that a set of pattern synonyms is
complete.

.. _patsyn-impexp:

Import and export of pattern synonyms
-------------------------------------

The name of the pattern synonym is in the same namespace as proper data
constructors. Like normal data constructors, pattern synonyms can be imported
and exported through association with a type constructor or independently.

To export them on their own, in an export or import specification, you must
prefix pattern names with the ``pattern`` keyword, e.g.: ::

      module Example (pattern Zero) where

      data MyNum = MkNum Int

      pattern Zero :: MyNum
      pattern Zero = MkNum 0

Without the ``pattern`` prefix, ``Zero`` would be interpreted as a
type constructor in the export list.

You may also use the ``pattern`` keyword in an import/export
specification to import or export an ordinary data constructor. For
example: ::

      import Data.Maybe( pattern Just )

would bring into scope the data constructor ``Just`` from the ``Maybe``
type, without also bringing the type constructor ``Maybe`` into scope.

To bundle a pattern synonym with a type constructor, we list the pattern
synonym in the export list of a module which exports the type constructor.
For example, to bundle ``Zero`` with ``MyNum`` we could write the following: ::

      module Example ( MyNum(Zero) ) where

If a module was then to import ``MyNum`` from ``Example``, it would also import
the pattern synonym ``Zero``.

It is also possible to use the special token ``..`` in an export list to mean
all currently bundled constructors. For example, we could write: ::

      module Example ( MyNum(.., Zero) ) where

in which case, ``Example`` would export the type constructor ``MyNum`` with
the data constructor ``MkNum`` and also the pattern synonym ``Zero``.

Bundled pattern synonyms are type checked to ensure that they are of the same
type as the type constructor which they are bundled with. A pattern synonym
``P`` can not be bundled with a type constructor ``T`` if ``P``\'s type is visibly
incompatible with ``T``.

A module which imports ``MyNum(..)`` from ``Example`` and then re-exports
``MyNum(..)`` will also export any pattern synonyms bundled with ``MyNum`` in
``Example``. A more complete specification can be found on the
:ghc-wiki:`wiki. <pattern-synonyms/associating-synonyms>`


.. _patsyn-typing:

Typing of pattern synonyms
--------------------------

Given a pattern synonym definition of the form ::

      pattern P var1 var2 ... varN <- pat

it is assigned a *pattern type* of the form ::

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

where ⟨CReq⟩ and ⟨CProv⟩ are type contexts, and ⟨t1⟩, ⟨t2⟩, ..., ⟨tN⟩
and ⟨t⟩ are types. Notice the unusual form of the type, with two
contexts ⟨CReq⟩ and ⟨CProv⟩:

-  ⟨CReq⟩ are the constraints *required* to match the pattern.

-  ⟨CProv⟩ are the constraints *made available (provided)* by a
   successful pattern match.

For example, consider ::

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

    f1 :: (Num a, Eq a) => T a -> String
    f1 (MkT 42 x) = show x

    pattern ExNumPat :: (Num a, Eq a) => (Show b) => b -> T a
    pattern ExNumPat x = MkT 42 x

    f2 :: (Eq a, Num a) => T a -> String
    f2 (ExNumPat x) = show x

Here ``f1`` does not use pattern synonyms. To match against the numeric
pattern ``42`` *requires* the caller to satisfy the constraints
``(Num a, Eq a)``, so they appear in ``f1``'s type. The call to ``show``
generates a ``(Show b)`` constraint, where ``b`` is an existentially
type variable bound by the pattern match on ``MkT``. But the same
pattern match also *provides* the constraint ``(Show b)`` (see ``MkT``'s
type), and so all is well.

Exactly the same reasoning applies to ``ExNumPat``: matching against
``ExNumPat`` *requires* the constraints ``(Num a, Eq a)``, and
*provides* the constraint ``(Show b)``.

Note also the following points

-  In the common case where ``CProv`` is empty, (i.e., ``()``), it can be
   omitted altogether in the above pattern type signature for ``P``.

-  However, if ``CProv`` is non-empty, while ``CReq`` is, the above pattern type
   signature for ``P`` must be specified as ::

     P :: () => CProv => t1 -> t2 -> .. -> tN -> t

-  The GHCi :ghci-cmd:`:info` command shows pattern types in this format.

-  You may specify an explicit *pattern signature*, as we did for
   ``ExNumPat`` above, to specify the type of a pattern, just as you can
   for a function. As usual, the type signature can be less polymorphic
   than the inferred type. For example ::

         -- Inferred type would be 'a -> [a]'
         pattern SinglePair :: (a, a) -> [(a, a)]
         pattern SinglePair x = [x]

   Just like signatures on value-level bindings, pattern synonym signatures can
   apply to more than one pattern. For instance, ::

         pattern Left', Right' :: a -> Either a a
         pattern Left' x  = Left x
         pattern Right' x = Right x

-  The rules for lexically-scoped type variables (see
   :ref:`scoped-type-variables`) apply to pattern-synonym signatures.
   As those rules specify, only the type variables from an explicit,
   syntactically-visible outer `forall` (the universals) scope over
   the definition of the pattern synonym; the existentials, bound by
   the inner forall, do not.  For example ::

         data T a where
            MkT :: Bool -> b -> (b->Int) -> a -> T a

         pattern P :: forall a. forall b. b -> (b->Int) -> a -> T a
         pattern P x y v <- MkT True x y (v::a)

   Here the universal type variable `a` scopes over the definition of `P`,
   but the existential `b` does not.  (c.f. discussion on #14998.)

-  For a bidirectional pattern synonym, a use of the pattern synonym as
   an expression has the type

   ::

         (CReq, CProv) => t1 -> t2 -> ... -> tN -> t

   So in the previous example, when used in an expression, ``ExNumPat``
   has type

   ::

         ExNumPat :: (Num a, Eq a, Show b) => b -> T t

   Notice that this is a tiny bit more restrictive than the expression
   ``MkT 42 x`` which would not require ``(Eq a)``.

-  Consider these two pattern synonyms: ::

       data S a where
          S1 :: Bool -> S Bool

       pattern P1 :: Bool -> Maybe Bool
       pattern P1 b = Just b

       pattern P2 :: () => (b ~ Bool) => Bool -> S b
       pattern P2 b = S1 b

       f :: Maybe a -> String
       f (P1 x) = "no no no"     -- Type-incorrect

       g :: S a -> String
       g (P2 b) = "yes yes yes"  -- Fine

   Pattern ``P1`` can only match against a value of type ``Maybe Bool``,
   so function ``f`` is rejected because the type signature is
   ``Maybe a``. (To see this, imagine expanding the pattern synonym.)

   On the other hand, function ``g`` works fine, because matching
   against ``P2`` (which wraps the GADT ``S``) provides the local
   equality ``(a~Bool)``. If you were to give an explicit pattern
   signature ``P2 :: Bool -> S Bool``, then ``P2`` would become less
   polymorphic, and would behave exactly like ``P1`` so that ``g`` would
   then be rejected.

   In short, if you want GADT-like behaviour for pattern synonyms, then
   (unlike concrete data constructors like ``S1``) you must write
   its type with explicit provided equalities. For a concrete data
   constructor like ``S1`` you can write its type signature as either
   ``S1 :: Bool -> S Bool`` or ``S1 :: (b~Bool) => Bool -> S b``; the
   two are equivalent. Not so for pattern synonyms: the two forms are
   different, in order to distinguish the two cases above. (See
   :ghc-ticket:`9953` for discussion of this choice.)

Matching of pattern synonyms
----------------------------

A pattern synonym occurrence in a pattern is evaluated by first matching
against the pattern synonym itself, and then on the argument patterns.

More precisely, the semantics of pattern matching is given in
`Section 3.17 of the Haskell 2010 report <https://www.haskell.org/onlinereport/haskell2010/haskellch3.html#x8-580003.17>`__.   To the informal semantics in Section 3.17.2 we add this extra rule:

* If the pattern is a constructor pattern ``(P p1 ... pn)``, where ``P`` is
  a pattern synonym defined by ``P x1 ... xn = p`` or ``P x1 ... xn <- p``, then:

  (a) Match the value ``v`` against ``p``. If this match fails or diverges,
      so does the whole (pattern synonym) match.   Otherwise the match
      against ``p`` must bind the variables ``x1 ... xn``; let them be bound to values ``v1 ... vn``.

  (b) Match ``v1`` against ``p1``, ``v2`` against ``p2`` and so on.
      If any of these matches fail or diverge, so does the whole match.

  (c) If all the matches against the ``pi`` succeed, the match succeeds,
      binding the variables bound by the ``pi`` . (The ``xi`` are not
      bound; they remain local to the pattern synonym declaration.)

For example, in the following program, ``f`` and ``f'`` are equivalent: ::

    pattern Pair x y <- [x, y]

    f (Pair True True) = True
    f _                = False

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

Note that the strictness of ``f`` differs from that of ``g`` defined
below:

.. code-block:: none

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

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