Pain Free Unfix with Pattern Synonyms

October 17, 2020 Programs

Pattern synonyms are a great feature.

It is common to define closed data types. Later if one wants to annotate their syntax tree or pass along any other additional information this can cause significant problems. A clean solution is to redefine the data type using open recursion and then taking the fixed point.1 This approach allows great flexibility and access to uniform recursion schemes but used to come at a cost. If the library writer had exposed the constructors, all existing user code would break with these changes. Since GHC 7.10, patterns allow us to completely swap out the underlying data type whilst maintaining the original interface.

Here’s how. Consider Hutton’s Razor.

data Hutton = Int Int | Add Hutton Hutton

Typically there will be many different operations defined as traversals of the syntax tree. One might typically be an evaluator.

eval :: Hutton -> Int
eval (Int n) = n
eval (Add n m) = eval n + eval m

Later, we might want to define the unfixed version of Hutton.

data HuttonF a = IntF Int | AddF a a deriving Functor

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

type Hutton = Fix HuttonF

Unfortunately, we can no longer use any of our existing functions. Fortunately, using pattern synonyms we can regain this functionality.

pattern (Int n) = Fix (IntF n)
pattern (Add x y) = Fix (AddF x y)

This is as far as GHC 7.8 will take us. To move further we need to take advantage of explicitly-bidirectional pattern synonyms which are set to be introduced in GHC 7.10. These allow us to explicitly specify the constructor as well as the pattern. Useless in this case but what if we also wanted to annotate out AST?

To do so it is usual to define a product type, Annotate,

data Annotate f = Annotate Label (f (Annotate f))

which we can then take the fixed point to get an annotated AST.

data Annotated = Annotate Hutton

Now we want to be able to keep using our existing functions for both annotated and unannotated values. The catch is that we can only have one pattern which corresponds to each constructor. To get around this we can use view patterns and a type class in order to use the same pattern for both our annotated and unannotated AST.

View provides an injection and projection function. Then defining suitable instances for Annotated and Hutton, we can reuse all of our previous definitions.

class View a where
  proj :: a -> HuttonF a
  inj :: HuttonF a -> a

pattern I n <- (proj -> IF n) where
  I n = inj (IF n)

pattern Add a b <- (proj -> AddF a b) where
  Add a b = inj (AddF a b)


instance View Hutton where
  proj = unFix
  inj = Fix

instance View Annotated where
  proj (Annotated _ e) = e
  inj v = Annotated (mkLabel v) v

mkLabel :: HuttonF Annotated -> Label

So far so good. Let’s test out our sample program.

eval :: View a => a -> Int
eval (I n) = n
eval (Add a b) = eval a + eval b

p1 = Add (I 5) (I 6)

main = do
  let p2 = p1 :: Hutton
  let p3 = p1 :: Annotated
  print (eval p2)
  print (eval p3)

> ./patterns
11
11

To take stock for a moment – using technology available in GHC 7.8 we were able to swap out our standard data type and replace it with an unfixed variant. Then with machinery available to us in GHC 7.10, we were able to vary this underlying type as long as we could provide suitable mapping functions.

Looking back at our definition of inj for Annotated, depending on what we want the label to be, it could make little sense to fill in the annotation whilst we are building the AST. It seems sensible to separate our View typeclass into two separate classes, one for projection and one for injection as they might not both make sense for all data types. Indeed if we introduce one more example, it is clear that they don’t.

data Holey f = Hole | Expr (f (Holey f))

type HuttonHole = Holey HuttonF

This union type represents syntax trees which might have holes in. Clearly there is no total definition of proj so we redefine our type classes as follows.

class Project a where
  proj :: a -> HuttonF a

class Inject a where
  inj :: HuttonF a -> a

instance Inject HuttonHole where
  inj = Expr

Now we should be able to use this data type very naturally to construct trees which might contain holes and later fill in the holes with whatever we please.

hole :: HuttonHole
hole = Hole

p4 :: HuttonHole
p4 = Add (I 5) hole

fillHole :: (Hole -> Hutton) -> HuttonHole -> Hutton
fillHole f Hole = f Hole
fillHole _ (Expr v) = v

Unfortunately we have pushed pattern synonyms a little bit too far. Instead of sweet sweet compilation, we are greeted with the following error message for each of the patterns.

Could not deduce (Inject a) arising from a use of ‘inj’
    from the context (Project a)
      bound by the type signature for Main.I :: Project a => Int -> a
      at patterns.hs:1:1
    Possible fix:
      add (Inject a) to the context of
        the type signature for Main.I :: Project a => Int -> a
    In the expression: inj' (IF n)
    In an equation for ‘I’: I n = inj (IF n)

GHC baulks at the fact that we have different class constraints for the pattern and constructor. I don’t think there is any reason that they need to have the same constraints but it might be desirable so that constructors, even synonyms, continue to match up with patterns.

There are many powerful abstractions in Haskell which allow a library maintainer to provide a consistent interface across interactions. Unfortunately, if they ever chose to expose their internal syntax tree to the end-user, it was previously very difficult to maintain backwards compatibility. Pattern synonyms provide the perfect tool to do just this but they don’t appear to stretch quite far enough to tackle all interesting use cases.

  1. I’ve been meaning to put this post up for a while but this stack overflow answer prompted me to finish up the post. As a result, the examples I use here are heavily inspired by it.↩

Tags: