Patterns and Paradoxes: The Logic of Pattern Synonyms

Introduction

In a previous article, we discussed the limitations of data constructors as provided by Haskell 2010. We also showed why smart constructors as a way to address these limitations are not adequate, before addressing these limitations using quasiquotation. While this certainly works, quasiquotes are a fairly powerful tool, and require the use of Template Haskell, which is a non-starter for many. Additionally, having to parse 'raw' input to the Haskell frontend is itself complicated. While these costs are sometimes justified (as in the article referenced), we would like to avoid those costs if we can.

In other articles, we have also talked about the benefits of packed data, in the context of SWAR, the FFI, SIMD and other kinds of optimizations. When reading all of these articles, however, it quickly becomes apparent just how tedious, error-prone and generally unpleasant it can be to work with packed data. A lot of the time, we are forced to rely on implicit forms of Word8 and similar, which is quite different to the explicit approach taken by Haskell's data representation of choice (namely, ADTs). Being able to combine the best of these two worlds feels like the ideal solution: we not only get the explicit and easy-to-use aspects of pattern matching and data constructors, with all the efficiency that packed encodings can give us.

Luckily for us, a solution to both of these problems exists in the form of pattern synonyms, somewhat helped along by view patterns. These can be thought of as an intermediate capability, between the power (and complexity) of quasiquotation and the simplicity (but limitations) of regular data constructors. Furthermore, they do not require any use of Template Haskell, and can be used not just for types we define ourselves, but for types someone else already defined. Lastly, this solution allows us something neither quasiquotation nor regular data constructors can: read-only patterns, which can be matched on, but not used to make new values.

At the same time, the syntax for both pattern synonyms and view patterns is hard to understand (and the documentation doesn't help much). To help show the use of both pattern synonyms and view patterns, we will consider the use case of many-valued logics. We will progressively increase the complexity of the examples, showing how to use these two features, while also discussing some advantages that they offer which don't exist for either quasiquotation or regular data constructors. Lastly, we will show how we can define pattern synonyms even for types that someone else wrote, allowing us to effectively provide a more convenient interface after the fact.

Anyone familiar with data constructors and pattern matching will be able to enjoy this article. No existing familiarity with other Haskell concepts is needed, but knowing why packed data is better can help. We encourage reading our previous articles working with packed data for context, but none of the concepts described in those articles beyond packed data will be relevant for this article.

Data constructors and their problems

Consider the venerable Maybe data type:

data Maybe a = Nothing | Just a

Maybe has two data constructors, which give us several capabilities. Firstly, we can use them to construct terms of type Maybe a for some choice of a. In some sense, we can think of them as functions like the following:

-- Not Haskell syntax
Nothing :: forall (a :: Type) . Maybe a

Just :: forall (a :: Type) . a -> Maybe a

Secondly, we have the ability to 'handle' a term of type Maybe a in a pattern match, by specifying what we want done for 'arm':

mapMaybe :: (a -> b) -> Maybe a -> Maybe b
mapMaybe f = \case
    Nothing -> Nothing
    Just x -> Just (f x)

Thirdly, and most usefully, GHC has a built-in mechanism to check that our 'handling' code doesn't forget any 'arms'. If we tried to write this:

mapMaybeBadly :: (a -> b) -> Maybe a -> Maybe b
mapMaybeBadly f = \case
    Just x -> Just (f x)

GHC would complain to us that we forgot to handle the Nothing 'arm'. This is known as exhaustiveness checking, and is a convenient and useful feature of Haskell 2010 data constructors.

In this sense, we can think of data constructors as an interface for interacting with a data type's terms. In some sense, this interface is privileged in Haskell 2010, as we cannot use either syntax for anything else. Furthermore, we can see that Haskell 2010 data constructors (in either application) are directly tied to the representation of the data type: if we wanted a different representation, we would have to change the data constructors too. This is a major limitation of Haskell 2010 data constructors: interface and representation are tightly coupled.

Another issue with data constructors is that they are inherently bidirectional. If we have a data constructor, it can be used to both pattern match and (unconditionally) construct new terms. We have no way of providing views (match-only patterns) in Haskell 2010. While we can somewhat avoid this problem using 'destructor' functions, this is always awkward and can be quite inefficient if the view provides access to several terms at once. Furthermore, such 'destructor' functions do not give us access to exhaustiveness checking.

We have already shown in a previous article that some of these limitations can be addressed by the use of quasiquoting. However, quasiquoting is a powerful, and thus complex, feature, allowing us to essentially 'hook into' the GHC parser. While in some cases, there really isn't any other option, a lot of the time, we don't want the complexity of having to parse our own input. Ideally, we would prefer to stay in the realm of Haskell, while generalizing data constructors and pattern matching to separate them from the representation of the data types they work over.

Introducing pattern synonyms

Pattern synonyms are a GHC extension designed as a limited overloading mechanism for data constructor syntax. More precisely, they are a rewrite mechanism which transforms patterns into other patterns, according to some rules. This effectively allows us to provide 'fake' data-constructor-like interfaces for data types, along with a way to inform GHC of which combinations of such interfaces should be seen as exhaustive.

A 'pattern' in this context is essentially one of the following:

• A data constructor application for introducing a term of a data type; or

• A pattern match over one or more data constructors.

Normally, a data type's definition tells us which patterns are available to use with that data type. For instance, a type like this:

data These a b = This a | That b | These a b

provides us with three patterns:

• This, which has one field of type a

• That, which has one field of type b

• These, which has two fields, one of type a and one of type b

We can use these patterns to construct terms of type These a b for any choice of a or b:

let x :: These Int = This 10
    y :: These String = That "dog"
    z :: These Char Float = These 'c' 0.1
 in foo

We can also pattern match on a term of type These:

case (t :: These Int String) of 
    This x -> doSomething
    That y -> doSomethingElse
    These x y -> doYetAnotherThing

Lastly, if we omit any of the patterns when pattern matching, GHC will tell us that our matches are not exhaustive.

These mechanisms are given to us entirely by the definition of These: the only way we can change them is by changing the definition of These somehow. Pattern synonyms allow us to 'decouple' the patterns associated with a data type from its definition (and thus, its representation), which allows us to use the same syntax as we would for 'real' data constructors, both in addition to, and even instead of, said 'real' data constructors. This potentially means we can have multiple different sets of patterns for the same data type, some of which can be marked as exhaustive, or not.

Defining pattern synonyms does not require the use of Template Haskell (unlike quasiquoting), and requires only one extension to be enabled (PatternSynonyms). In some cases, the extension only needs to be enabled where the pattern synonyms are defined, rather than where they're used. This makes them a much easier tool for solving the limitations of data constructors, both for those writing pattern synonyms and those using pattern synonyms written by others.

An example case: many-valued logic

To serve as a starting point for demonstrating pattern synonyms and their various uses, we will use many-valued logic. In brief, a many-valued logic has more than two truth values, unlike Boolean (or 'classical') logic, which has only two. There are many reasons to want such a thing, but a significant reason is the problem of the monotonicity of entailment. We will briefly discuss this idea as a motivating example; a deep understanding of this topic won't be necessary to understand pattern synonyms.

The monotonicity of entailment is a property of inference in classical logic. Formally, it states that for any A,B,C, if A⊢C, then A∧B⊢C as well. Put another way, given some knowledge base (typically seen as a conjunction of 'ground truths' or 'facts'), if that knowledge base is able to demonstrate some other fact, adding more to the knowledge base will never cause it to refute that fact. This is a desirable property, as it means that classical logic is both easier to work with, but also easier to reason about meta-logically.

However, this can pose significant problems if our knowledge base ever contains contradictory information. This leads to what is known as the principle of explosion: A∧¬A⊢B for absolutely any A and B.This is highly destructive, as this contradiction 'infects' everything in the knowledge base, including facts that have nothing to do with the contradiction! The solution classical logic forces on us is to ensure no contradictions arise in any such knowledge base. However, in the presence of human error and distributed systems (both things we at MLabs are quite familiar with), this approach rapidly becomes unsustainable. Instead, we would prefer to handle such possibilities in a more graceful way.

Many-valued logics are one possible solution to this, as they give up monotonicity of entailment. Indeed, many-valued logics have been proposed as solutions to computer-based reasoning from knowledge bases, especially when these could contain contradictory evidence. While this is a fascinating topic in its own right, we will limit ourselves to just a single example of such a logic for the purpose of illustrating pattern synonym use.

3VL: The Logic of Paradox

The many-valued logic we will use in our example is Priest's Logic of Paradox[1]. This is an example of a paraconsistent logic; the goal of such logics is to isolate and confine contradictions, so that they are less 'infectious'. The Logic of Paradox achieves this by adding a third truth value to the two that classical logic gives us: this third value means 'inconsistent' or 'both true and false'. Another way of viewing the Logic of Paradox is that any given sentence is assigned at least one truth value, whereas classical logic would assign exactly one.

We begin by defining the Logic of Paradox equivalent to Bool, which can be thought of as 'the type of truth values'[2]:

data Pierc = OnlyFalse | OnlyTrue | Both
    deriving stock (Eq, Ord, Show)

Viewing this from the 'multi-assignment' point of view from earlier, OnlyFalse and OnlyTrue represent a truth value assignment of False only and True only respectively, while Both would represent a truth value assignment of False and True at the same time. The Ord instance we (indirectly) chose reflects this: the ordering is a combination of the Ord instance for Bool, together with inclusion.

We can use our definition of Pierc to implement the common logical operations of negation ('not'), conjunction ('and') and disjunction ('or'). The Logic of Paradox defines the meaning of these operations from the 'multi-assignment' point of view, by viewing any Pierc as basically a Set Bool. Thus, for negation, we 'map' the classical negation operation over each 'element' of the 'set', giving us the following:

not :: Pierc -> Pierc
not = \case
    OnlyFalse -> OnlyTrue
    OnlyTrue -> OnlyFalse
    x -> x

For conjunction and disjunction, we do something similar. Using the equivalent Boolean operation, we 'map' it (uncurried) over the Cartesian product of both 'sets'. More specifically, given two Piercs x and y, we get the following:

• If x or y is OnlyFalse, then the result of the conjunction is OnlyFalse. This stems from conjunction with the false value in Boolean logic always yielding the false value; thus, even if the other value is Both, the outcome is the same.

• If x and y are both OnlyTrue, then the result of the conjunction is also OnlyTrue. Since in the 'set view' in this case x and y are both singletons, this reduces to the Boolean operation.

• Otherwise, the result of the conjunction is Both.

Disjunction behaves similarly. We can use the data constructors of Pierc once again to define these.

and :: Pierc -> Pierc -> Pierc
and OnlyFalse _ = OnlyFalse
and _ OnlyFalse = OnlyFalse
and OnlyTrue OnlyTrue = OnlyTrue
and _ _ = Both

or :: Pierc -> Pierc -> Pierc
or OnlyTrue _ = OnlyTrue
or _ OnlyTrue = OnlyTrue
or OnlyFalse OnlyFalse = OnlyFalse
or _ _ = Both

Other operations (such as 'if') can be defined using a combination of these three operators.

Checking performance

The definition of Pierc above and its operators are correct, and convenient to work with. In particular, Pierc can be pattern matched on, and its constructors are safe to expose. However, the performance of the Pierc data type, and its operators, leaves a lot to be desired. Even if we put Piercs into a packed collection (such as an Array from massiv), we don't really gain the benefits of a packed collection for performance. This is because ADTs in GHC haskell are always boxed[3].

To demonstrate this phenomenon, we will set up some benchmarks. We will use these same benchmarks later to show how much a packed representation helps. For benchmarking data, we will use an Array from massiv (using the B representation), containing 2²º Piercs. The benchmarks will apply each of negation, conjunction and disjunction to our Array; in the case of conjunction and disjunction, we will use our array twice. We will then use computeS to produce a new array with the results.

Based on our current definition, we get the following:

All
  Not, 3VL, basic:   OK
    3.73 ms ±  71 μs, 8.0 MB allocated, 617 B  copied,  39 MB peak memory
  And, 3VL, basic:   OK
    4.44 ms ±  40 μs, 8.0 MB allocated, 509 B  copied,  55 MB peak memory
  Or, 3VL, basic:    OK
    4.25 ms ±  35 μs, 8.0 MB allocated, 293 B  copied,  55 MB peak memory

We can see that the time taken for 2²0 items for any of these operations is about 4ms. This is definitely slow for such an amount of packed data, based on what we have seen in previous articles working with such. We also see that the amount of allocated data is 8 MiB. This is not surprising, as a boxed Array is essentially full of pointers, with the data of each Pierc at the end of said pointer. As there are only three possible Pierc values, these get shared, but we still end up using a lot of space. Furthermore, this indirection causes the loss of performance we are seeing here: even though the pointers to the data are packed, the data itself isn't, which means every time we do any of these operations, we end up having to follow a pointer.

With these numbers, let us see if we can do better, while keeping the interface unchanged, with the help of pattern synonyms.

3VL: another representation

Knowledgeable readers will no doubt observe that we can represent truth values of the Logic of Paradox in a packed manner with relative ease. We can do this by representing Both as 0, OnlyFalse as -1 and OnlyTrue as 1. This allows efficient translations of all our operations:

• not becomes negate;

• and becomes min; and

• or becomes max.

This would allow packing of each Pierc into an 8-bit value (Int8), which would allow us to gain the benefits of packed data without any loss of functionality.

However, this leads to several problems if done directly:

• Pattern matching becomes awkward, as we now have to always remember that the only valid values are -1, 0 and 1, along with their meaning.

• Construction would need to be guarded to avoid introducing any of the other possible Int8 values.

• A newtype wrapper would either provide no safety (if the constructor was exposed) or be impossible to pattern match on (if the constructor was hidden).

Thus, it seems we are forced to choose between the convenience of data constructors and the efficiency of packed data. Fortunately for us, we can use pattern synonyms to avoid this problem.

First, we define Pierc again, this time as a newtype wrapper:

-- Do not expose this constructor
-- Ord cannot be `via` derived, as it will be different to the original
newtype Peirc = Peirc Int8
    deriving (Eq, Prim) via Int8
    deriving stock (Show)

The Prim derivation is necessary to use packed arrays, such as the P representation in massiv's Array. Next, we want to define some bidirectional patterns for Pierc. We will need the PatternSynonyms extension enabled to define these.

pattern OnlyFalse :: Peirc
pattern OnlyFalse = Peirc (-1)

pattern Both :: Peirc
pattern Both = Peirc 0

pattern OnlyTrue :: Peirc
pattern OnlyTrue = Peirc 1

The syntax of a bidirectional pattern looks similar to a function, aside from the extra pattern keyword. We can see that patterns have a signature, as well as a definition. The signature of a pattern (bidirectional or not) always consists of the following:

1. The keyword pattern; then

2. The name of the pattern, which follows the same rules of naming as data constructors; then

3. A function type, the result of which must be the data type this pattern is being defined for.

Normally, the function type in Item 3 of the above list would contain one argument for each field the pattern is supposed to emulate. However, since Pierc (or at least, our intended view of it) has no fields, the function type is reduced to just the result type.

The definition of a bidirectional pattern also follows a structure:

1. The keyword pattern; then

2. The name of the pattern, as previously; then

3. A definition, which must be a pattern match against the (actual) data constructor of the data type for which the pattern is being defined.

Essentially, by specifying a bidirectional pattern, we are specifying a rewrite: whenever the code sees whatever is on the left-hand-side of =, it gets replaced with whatever is on the right-hand-side of =. However, the benefit of a pattern synonym is that right-hand-sides of definitions can mention constructors which do not have to be visible where the pattern is used. Thus, if we wrote this in a different module:

-- The constructor of `Pierc` is not imported
let x = OnlyFalse
    in foo

GHC would translate that into the following:

-- The constructor of `Pierc` isn't imported, but GHC substitutes it in
-- As we have full control of how this happens, it is safe
let x = Pierc (-1) 
    in foo

Likewise, in a situation like this:

-- The constructor of `Pierc` is not imported
case x of 
    OnlyFalse -> doOneThing
    OnlyTrue -> doAnotherThing
    Both -> doAThirdThing

GHC would transform it into this:

case x of 
    Pierc (-1) -> doOneThing
    Pierc 1 -> doAnotherThing
    Pierc 0 -> doAThirdThing

This is why such patterns are referred to as bidirectional - they can be used both to construct values and to pattern match. Effectively, these allow us to define our own data constructors, which do not necessarily mirror the representation of the data type.

The earlier pattern matching translation from the bidirectional patterns, however, shows a limitation of our initial definition: that is, it isn't exhaustive. Indeed, if we tried this, GHC would warn us about it. However, we know that there isn't any other Int8 that a Pierc could wrap. In order to inform GHC of this, we need to add a special pragma:

{-# COMPLETE OnlyFalse, OnlyTrue, Both #-}

This tells GHC that this combination of constructors should be treated as exhaustive for Pierc.

To provide our patterns to those who import our module, we need to export them. The regular way to do this also makes use of the pattern keyword:

module 3VL (Pierc, pattern OnlyFalse, pattern OnlyTrue, pattern Both) where 
    -- rest of module

However, this method has two downsides:

• There is no direct association between the patterns and the data type whose constructors they are supposed to replace. Unlesss we are careful with the ordering of the exports, this association is easy to lose.

• Anyone importing the 3VL module would have to also enable PatternSynonyms, as to import our patterns, they'd need to use the pattern keyword in their imports.

Thus, GHC provides an alternative means:

module 3VL (Pierc, OnlyFalse, OnlyTrue, Both) where 
    -- rest of module

This solves both issues: now, these patterns will accompany Pierc in any generated documentation via Haddock, and those importing our module don't have to enable PatternSynonyms, or indeed, even know that OnlyFalse and friends are pattern synonyms.

This combination of safety and efficiency allows us to define our improved versions of the three functions over Piercs:

not :: Peirc -> Peirc
not = coerce @(Int8 -> Int8) negate

and :: Peirc -> Peirc -> Peirc
and = coerce @(Int8 -> Int8 -> Int8) min

or :: Peirc -> Peirc -> Peirc
or = coerce @(Int8 -> Int8 -> Int8) max

However, nothing stops us from using our pattern synonyms if that makes our code clearer:

instance Ord Pierc where
    _ <= Both = True
    Both <= _ = False
    _ <= OnlyTrue = True
    OnlyFalse <= _ = True
    _ <= _ = False

Furthermore, because we hide the constructor of Pierc, those that import our module cannot work directly over the underlying representation, potentially putting values into a Pierc that don't make sense. This lets us benefit from the performance of packed data without losing any of the expressiveness of data constructors.

To see just how large a performance improvement we get, let's repeat our earlier benchmark, but now comparing the original results to the new Pierc and operations, stored in a packed Array instead.

All
  Not, 3VL, basic:   OK
    3.73 ms ±  71 μs, 8.0 MB allocated, 617 B  copied,  39 MB peak memory
  Not, 3VL, pattern: OK
    1.25 ms ±  24 μs, 1.0 MB allocated, 151 B  copied,  39 MB peak memory
  And, 3VL, basic:   OK
    4.44 ms ±  40 μs, 8.0 MB allocated, 509 B  copied,  55 MB peak memory
  And, 3VL, pattern: OK
    1.38 ms ±  14 μs, 1.0 MB allocated,  75 B  copied,  55 MB peak memory
  Or, 3VL, basic:    OK
    4.25 ms ±  35 μs, 8.0 MB allocated, 293 B  copied,  55 MB peak memory
  Or, 3VL, pattern:  OK
    1.38 ms ±  13 μs, 1.0 MB allocated,  64 B  copied,  55 MB peak memory

We can see that packing our data improved our representation size by a factor of 8. This is not surprising, as we have replaced pointers to our data (which are a machine word in size) with a single byte. Furthermore, we can see approximately a threefold speedup in processing time for the same size of data, which stems from us not having to 'chase pointers' in order to work with Pierc values.

This performance benefit would ordinarily require us to give up on the utility and clarity of data constructors and pattern matching, or possibly tolerate some loss of safety. Thanks to pattern synonyms, we can have the best of both worlds: an optimal, packed representation, but an interface that looks, and acts, just like pattern matching and data constructors. Furthermore, because we have now completely separated interface and implementation, we no longer have to worry about representation changes to Pierc breaking existing code, provided our pattern synonyms retain their original signatures.

Safe underlying access via read-only patterns

The above set of operations, together with pattern matching on Pierc, is certainly sufficient to define any other operation in the Logic of Paradox. However, such definitions are not necessarily going to be efficient, and due to the large number of possible operations in the Logic of Paradox, it isn't feasible for us to provide efficient implementations of all of them. This means that users of Pierc may end up being unable to implement the operator they want efficiently, even if such an option existed, due to their (deliberate) inability to access the underlying representation.

To see an example of this, consider the 'if and only if' operator. We can define it as follows:

iff :: Pierc -> Pierc -> Pierc
iff Both _ = Both
iff _ Both = Both
iff OnlyTrue OnlyFalse = OnlyFalse
iff OnlyFalse OnlyTrue = OnlyFalse
iff _ _ = OnlyTrue

-- equivalent definition
-- iff x y = and (or (not x) y) (or (not y) x)

Neither of these definitions are particularly efficient. However, if we write down the truth table for 'if and only if', but substitute our Int8 representations for truth values, we see an interesting pattern:

x	y	x ↔ y
-1	-1	1
-1	1	-1
-1	0	0
1	-1	-1
1	0	0
1	1	1
0	-1	0
0	1	0
0	0	0

x↔y in our choice of representation is actually just xy. However, this more efficient implementation is not possible outside of the module that defines Pierc, as we do not expose Pierc's constructor.

We could allow (at the cost of some clarity later down the line) those using Pierc to gain access to the underlying representation by writing a function like this:

toInt8 :: Pierc -> Int8
toInt8 = coerce

However, we can instead use this as an opportunity to demonstrate a different kind of pattern synonym. We will thus instead write a unidirectional pattern synonym for Pierc that achieves the same result, but with pattern matching syntax:

pattern AsInt8 :: Int8 -> Pierc
pattern AsInt8 i8 <- Pierc i8

We can see three differences to our previous pattern synonyms on display:

• The signature now has a function type with an argument; and

• Instead of the definition's left-hand-side being separated from its right-hand-side by =, we instead have <-.

• There is a variable bound in the definition's left-hand-side, which also occurs on the right-hand-side.

The function type arguments correspond to 'fields' that our synonym will (claim to) have. In this case, we're essentially defining AsInt8 to mimic a data constructor with one field of type Int8. The use of <- instead of = designates AsInt8 as a unidirectional pattern synonym, which makes it read-only. Thus, code like this:

case (x :: Pierc) of 
    AsInt8 i8 -> doSomething

would be translated by GHC into this:

case (x :: Pierc) of 
    Pierc i8 -> doSomething

However, just like with bidirectional pattern synonyms, the Pierc data constructor does not have to be in scope at the use site of the pattern synonym for this to work. If we instead tried something like this:

-- will not compile!
let x = AsInt8 (-1) 
    in foo

GHC would throw an error, stating that AsInt8 is a unidirectional pattern synonym.

We can export AsInt8 alongside our other pattern synonyms exactly as you'd expect:

module 3VL (Pierc (OnlyFalse, OnlyTrue, Both, AsInt8)) where
    -- rest of module

We also note that a match against AsInt8 should be exhaustive. Thus, we can add a second COMPLETE pragma to tell GHC this information:

{-# COMPLETE AsInt8 #-}

Together with our original COMPLETE pragma, GHC will now know that any of the following combinations of matches are exhaustive:

• OnlyFalse, OnlyTrue and Both; or

• AsInt8.

This is one of the greatest advantages of pattern synonyms over regular data constructors, as we can define read-only 'views' of our data types, but still allow others to use familiar pattern matching syntax.

View patterns: a helping hand

Readers familiar with representations of three-valued logics will note that Pierc's packed representation is balanced ternary. We chose this representation because it makes negation, conjunction and disjunction efficient, but it is not the only possible choice. Another popular option is to have OnlyFalse represented as 0, OnlyTrue as 1, and Both as 2. This representation effectively treats Piercs as ternary numbers, and has numerous advantages of its own: for example, the Ord instance for Pierc is the natural ordering for ternary numbers.

It would be good for us to be able to convert ternary digits as Word8s (perhaps having read them in from some external data) into Piercs. For that purpose, we could define a function like this:

fromTrit :: Word8 -> Maybe Pierc
fromTrit = \case
    0 -> Just OnlyFalse
    1 -> Just OnlyTrue
    2 -> Just Both
    _ -> Nothing

However, we saw that earlier we could define a way of 'converting' a Pierc into an Int8 using a unidirectional pattern synonym. Surprisingly, we can do a similar thing here: effectively, we will be defining a 'fake' data constructor for Word8 which looks like it has a Pierc as a 'field'.

Normally, what we want would be impossible: you cannot normally add data constructors to data types 'after the fact'. Furthermore, we do not define (or even control in any way) Word8, as this type is provided by base. However, these are not issues for pattern synonyms, potentially allowing us to add 'new constructors to old types'. This is another powerful tool, potentially allowing us to make existing types more convenient for ourselves, and others, to pattern match on.

Let's try and build such a pattern match. We'll begin with the pattern signature:

pattern FromTrit :: Pierc -> Word8

We can immediately see that the function type part of the pattern synonym signature changes. Instead of the result being Pierc as it has been so far, it is now Word8. This makes sense: whereas before, we were defining 'data constructors' for Pierc, we are now doing the same for Word8 instead. However, when we get to the definition of the pattern synonym, we hit a snag:

pattern FromTrit :: Pierc -> Word8
pattern FromTrit p <- _ -- what on earth goes here?

There seems to be no pattern on Word8 we could use that would give us a Pierc, or even anything resembling one. Indeed, the only pattern on Word8 we could use at all would give us a Word8#, which doesn't get us any closer.

Here, we can make use of a different extension: view patterns. This allows us to effectively add arbitrary functions to patterns, then match on their results. Additionally, we have the ability to implicitly 'carry' arguments through such patterns, similarly to how we can use >>> or . to compose functions without explicitly naming their arguments.

To demonstrate how view patterns work, let's consider a function maybeEven, which, given a Maybe of some integral type, keeps it intact if it is both a Just and even, and produces Nothing otherwise:

maybeEven :: (Integral a) => Maybe a -> Maybe a
maybeEven = \case
    Just x -> if even x
                then Just x
                else Nothing
    Nothing -> Nothing
-- alternative definition
-- maybeEven x = do
--      Just y <- x
--      guard (even y)
--      pure y

We have to use a slightly awkward combination of tools because we have to separate the use of functions to produce results and pattern matching. View patterns allow us to avoid that restriction:

-- needs ViewPatterns enabled
maybeEven :: (Integral a) => Maybe a -> Maybe a
maybeEven x = case x of 
    Just (even -> True) -> x
    Nothing -> Nothing

We can see the view pattern in the Just 'arm' of the pattern match. We use the Just pattern as normal, but instead of binding the field to a variable, we use a view pattern to first apply even implicitly to that field, then check if it matches to True. The -> represents an implicit carrying of the result of a function or first field of a match.

We can potentially use multiple view patterns at once, and bind their results. Consider this variant of maybeEven that lifts it to both halves of a pair:

pairMaybeEven :: (Integral a, Integral b) => (Maybe a, Maybe b) -> Maybe (a, b)
pairMaybeEven= \case 
    (Just @x(even -> True), Just y@(even -> True)) -> Just (x, y)
    _ -> Nothing

While in regular functions, view patterns are not necessarily easier to read or use, in pattern synonyms, they are essential, as a pattern synonym must be a pattern. Combining view patterns and pattern synonyms gives us a lot more power, as we can now essentially replace any function similar to fromTrit above with an interface that looks like a pattern match.

How would we apply view patterns here? The easiest option would be re-using our fromTrit function:

pattern FromTrit :: Pierc -> Word8
pattern FromTrit p <- (fromTrit -> Just p)

We can see the use of implicit arguments here. Effectively, we are translating a match like this:

case (w8 :: Word8) of
    FromTrit p -> doSomethingWith p
    _ -> doSomethingElse

to this:

case fromTrit w8 of 
    Just p -> doSomethingWith p
    Nothing -> doSomethingElse

Just as previously, we can see that any variable on the left-hand-side of the pattern synonym definition must occur somewhere on the right-hand-side.

However, we don't have to re-use fromTrit if we don't want to. FromTrit can be written entirely inline:

pattern FromTrit :: Pierc -> Word8
pattern FromTrit p <-
  ( \case
      0 -> Just F
      1 -> Just T
      2 -> Just U
      _ -> Nothing ->
      Just p
    )

This shows the capabilities of view patterns taken to the extreme, making use of a case-lambda to produce a Maybe, then verify that it is a Just and bind the field. However, we don't suggest writing code like this: it obscures the intent of the pattern synonym, even for people used to view patterns. Using a helper function like fromTrit is both clearer and easier to write. We only show this version to show what view patterns are capable of.

Unlike our previous synonym, FromTrit should not be considered exhaustive, as matching on it only tells us whether the Word8 is one of 0, 1 or 2. Furthermore, unlike previously, FromTrit is a pattern synonym for Word8, which is not a type we define ourselves. Thus, exporting it requires us to use the pattern form of exports:

module 3VL (Pierc (OnlyFalse, OnlyTrue, Both, AsInt8), pattern FromTrit) where
    -- rest of module

This means that someone who wants to import FromTrit would have to enable the PatternSynonyms extension, and use the pattern keyword in their import list as well.

Another example: views over vectors

To show a different, and perhaps more general, example, let's address a limitation of the vector library. Our motivation will be based on the syntax of lists, and its convenience. Lists in Haskell are widely used, not least of all because their syntax is so convenient:

find :: forall a . (a -> Bool) -> [a] -> Maybe a
find f = \case
    [] -> Nothing
    (x : xs) -> if f x 
                  then Just x
                  else find f xs

This convenience also extends functions that construct lists:

mapMaybe :: forall a b . (a -> Maybe b) -> [a] -> [b]
mapMaybe f = \case
    [] -> []
    (x : xs) -> case f x of 
                    Nothing -> mapMaybe f xs
                    Just y -> y : mapMaybe f xs

Despite this convenience, lists are often a bad choice of data structure. Being singly-linked lists, they lack random access, use a lot of memory, and lack locality. Furthermore, Haskell lists mix metaphors, being simultaneously 'a linear collection', 'a pure stream' and 'the non-determinism monad', without a clear designation which particular role they are supposed to be fulfilling in any given case. Furthermore, despite the rather significant difference in functionality (and performance) across these three use cases, it isn't clear at all which functions that consume or produce lists are intended to be used for which case. Thus, in most cases, it is better to use a more focused data type.

In cases where we want a linear collection, one of the Vector types from the vector package is usually a good choice. It gives us random access, potentially allows for packed data, and has a rich (and fairly efficient) API. However, Vectors (of all types) cannot be pattern matched on similarly to lists. The best we can do is make use of uncons, but this is much less convenient. Furthermore, unlike lists, whose cons operation is Θ(1), Vector cons is Θ(n), which can easily balloon performance if not used carefully.

We can make this situation more pleasant, as well as protecting ourselves from potential performance blowups, by defining some pattern synonyms for Vectors. Initially, we will define synonyms only for boxed Vectors, but we will then generalize this to work on any type of Vector defined in the vector library. We can also use this to demonstrate some other capabilities of pattern synonyms (and by extension, view patterns), such as polymorphism.

Our design will consist of two pattern synonyms:

• NilV, which is equivalent to [] for lists. This can be bidirectional, as constructing the empty Vector is cheap.

• ConsV, which is equivalent to : for lists. This should be unidirectional, due to the Θ(n) cost of cons for Vectors.

Although NilV is a bidirectional synonym, we have to use a slightly different syntax to define it:

-- we import Data.Vector qualified as Vector
pattern NilV :: Vector.Vector a
pattern NilV <- (Vector.null -> True)
    where
        NilV = Vector.empty

Instead of looking like our previous bidirectional pattern synonyms, NilV looks like a unidirectional synonym, combined with a strange where bind. This is an alternative syntax for bidirectional pattern synonyms, where we don't have an identical translation in both the 'construction' and 'matching' directions. In this case, GHC would translate this:

let x = NilV 
    in foo

into

let x = Vector.empty
    in foo

but this:

case x of 
    NilV -> doAThing
    _ -> doAnotherThing

would become

if Vector.empty x
    then doAThing
    else doAnotherThing

In fact, the =-based bidirectional synonym syntax we used earlier could be replaced entirely with this new form:

-- similarly for the other two
pattern OnlyFalse :: Peirc
pattern OnlyFalse <- Pierc (-1)
    where
        OnlyFalse = Pierc (-1)

However, this is longer, and ultimately unnecessary, as both the 'match' direction and the 'build' direction are identical. Thus, using = is both shorter and clearer.

Another interesting difference is that NilV is polymorphic. This is necessary to allow pattern synonyms to take on the full generality of data constructor functionality. In fact, we are even allowed to have type class constraints in our pattern synonyms, which we will use to our advantage later.

ConsV is a more typical unidirectional pattern:

pattern ConsV :: a -> Vector a -> Vector a
pattern ConsV x xs <- (Vector.uncons -> Just -> (x, xs))

We once again turn to view patterns to help us. However, because Vector.uncons produces Just (a, Vector a), we have to 'unwrap' two data constructors in our pattern synonym right-hand-side. View patterns permit this by chaining using ->. Effectively, code such as this

case v of 
    ConsV x xs -> doSomethingWith x xs

would translate to

case Vector.uncons v of 
    Just (x, xs) -> doSomethingWith x xs

Lastly, we can ensure that exhaustiveness checking still works as we expect:

{-# COMPLETE NilV, ConsV #-}

This shows that mixing unidirectional and bidirectional pattern synonyms is fine for COMPLETE pragmas. As a result, functions that 'take apart' Vectors are now as convenient to write as ones on lists:

findV :: forall a . (a -> Bool) -> Vector a -> Maybe a
findV f = \case
    NilV -> Nothing
    ConsV x xs -> if f x
                    then Just x
                    else findV f xs

However, we cannot accidentally use ConsV to build Vectors, due to the Θ(n) performance cost:

mapMaybeV :: forall a b . (a -> Maybe b) -> Vector a -> Vector b
mapMaybeV f = \case
    NilV -> NilV
    ConsV x xs -> case f x of 
                    Nothing -> mapMaybeV f xs
                    -- This won't compile!
                    Just y -> ConsV y : mapMaybe f xs

We can make these pattern synonyms even more useful by relying on vector's generic interface across all the types of Vector they support, rather than choosing a single one. The change required is minor:

-- Needs Data.Vector.Generic imported as Vector

pattern NilV :: forall a . Vector.Vector v a => v a
pattern NilV <- (Vector.null -> True)
    where
        NilV = Vector.empty

pattern ConsV :: forall a . Vector.Vector v a => a -> v a -> v a
pattern ConsV x xs <- (Vector.uncons -> Just -> (x, xs))

{-# COMPLETE NilV, ConsV #-}

This will now work for any kind of Vector provided by the vector library. It also shows that we can use type class constraints on type variables in pattern synonym signatures. In such a case, these pattern synonyms will effectively work for any type or combination of fields that satisfy those constraints:

import Data.Vector.Storable as Storable
import Data.Vector as Boxed

case (v :: Boxed.Vector (Storable.Vector Int)) of 
    ConsV (ConsV x xs) ys -> doSomething
    -- and so on

There are more capabilities of pattern synonyms (such as GADT-like constraint 'revealing' and record pattern synonyms), but these are much less common. Furthermore, they are relatively straightforward extensions of the examples and principles from our article, so you can consult the documentation for how they work equipped with your new knowledge.

Conclusion

Having seen how pattern synonyms work, we can see that they can address many of the issues with data constructors, especially with regard to excessive coupling between representation and interface. Furthermore, together with view patterns, pattern synonyms allow us to also provide read-only 'views' over data types, as well as data-constructor-like interfaces even for types we did not write ourselves. While we could address some of these limitations with smart constructors, or quasiquotation, pattern synonyms fill a convenient niche: they are more 'constructor-like' than smart constructors, and fit more smoothly into pattern use, but don't require use of Template Haskell or hooks into the GHC parser like quasiquotation. This makes them a good general choice for solving the limitations of data constructors conveniently.

Furthermore, for those who only use, rather than define, pattern synonyms, they can be almost entirely transparent, requiring no extensions to be enabled, no special syntax, and no knowledge beyond the fact that they work like regular data constructors do. Neither smart constructors, nor quasiquotation, offer this degree of convenience for those using, rather than defining, them. When combined with their 'retrofitting' ability for existing datatypes, as well as the ability to make use of GHC's exhaustiveness checking, pattern synonyms become a great tool for designers of interfaces in Haskell of all sorts.

We showed how many different ways pattern synonyms can be used, starting with basic bidirectional synonyms, and going all the way through to combinations of polymorphic unidirectional and bidirectional synonyms involving type class constraints and view patterns. Given that the documentation for both extensions is somewhat cryptic, we feel these examples better show both how these extensions work, and why they're useful. While we didn't show every possible capability of these tools, we feel that, with these examples and explanations, the documentation will be much easier to follow and use for your particular cases and situations.

So give pattern synonyms a go - you'll be surprised how quickly you'll find uses for them absolutely everywhere. Finally, if you enjoyed this article and it sounds relevant to your business, don’t hesitate to get in touch.

---

1. It would be wrong of us not to mention that technically, this logic does not originate with either paraconsistency or Priest. Kleene described this exact system as the logic K3, where the third value was 'unknown', but with identical operations. Likewise, the Logic of Paradox was first described by Florencio González Asenjo, which Priest popularized and extended. We only refer to this as Priest's logic here because much of the literature around it stems from Priest's work.
2. Our choice of name stems from Bool being the unit of binary logic truth value, which is named after George Boole, who first described what we now know as Boolean logic. Since our first recorded instance of a three-valued logic was described by Charles Sanders Peirce, Pierc seemed a suitable analog.
3. Meaning 'represented by a pointer to their data'.