This post is in Literate Haskell. The entire contents can be copied into a file called Pattern.lhs
and will be compilable by GHC.
I recently read Morten Rhiger’s Functional Pearl, Type-safe pattern combinators. He develops a library of combinators for pattern matching, allowing user code such as
match (5, (3, 4)) $
pair (cst 5) (pair var var) ->> \ x y → x + y
where the equivalent code using Haskell’s own pattern matching is
case (5, (3, 4)) of
(5, (x, y)) -> x + y
The pattern combinator library has various features we want from a pattern matching library: type-checking of patterns, and a lightweight/efficient implementation. The system is also clearly flexible enough to support all of Haskell’s built-in pattern-matching capabilities, and then some.
However, I found the library confusing to work with, because the type signatures give me no clue about what is going on. For instance, consider the type of var
, the “variable pattern” combinator, given by GHCi:
ghci> :type var
var ::
((t -> t1 -> t2) -> (t3 -> t) -> (t3, t1) -> t2,
t4 -> ((t4, t5) -> t6) -> t7 -> t5 -> t6)
There are tuples and functions everywhere, and it is hard to see what is going on — never mind that GHCi helpfully names all the type variables t
.
In this post, I attempt to tame the types of the pattern combinators, while leaving the internal code as much the same as possible. In the final result, var
has type
var :: Pattern (a :*: Nil) a
The first type parameter lists the types of the variables bound by the pattern, and the second gives the type of the overall pattern to be matched.
Preliminaries
Lists of types
We keep track of the variables bound by a pattern by listing their types. To do that, we use the following type-level list:
> {-# LANGUAGE EmptyDataDecls, TypeFamilies,
> TypeOperators, RankNTypes, GADTs,
> ScopedTypeVariables, NoMonomorphismRestriction #-}
> module Pattern where
>
> import Prelude hiding(succ,fail,any, (||))
>
> data Nil
> data h :*: t
> infixr :*
The main operation we do on this is concatenating two lists, (:++:)
:
> type family (:++:) a b
> type instance Nil :++: xs = xs
> type instance (h:*:t) :++: xs = h :*: (t :++: xs)
We have two different ways of expressing functions of multiple arguments: curried and uncurried. We can express both with type functions:
> type family Tuple xs
> type instance Tuple Nil = ()
> type instance Tuple (h:*:t) = (h, Tuple t)
>
> type UncurryFunc xs r = Tuple xs -> r
>
> type family CurryFunc xs r
> type instance CurryFunc Nil r = r
> type instance CurryFunc (h:*:t) r = h -> CurryFunc t r
Both representations of multi-argument functions are used by Morten’s code: internally, uncurried functions are used, but the curried form is presented to the user as it is more idiomatic. Some of the code is hence devoted to conversions between these forms. We define the type of converters from curried to uncurried form:
> type Conv vs r = CurryFunc vs r -> UncurryFunc vs r
It might seem at first that it would just be simpler to use the curried form internally and avoid the fuss of conversion; however, this is unfortunately not possible: it turns out that the uncurried form is necessary in order to support proper handling of pattern-match failure.
Resolving the ambiguity
Since we are using type families, which are not guaranteed to be injective, a number of type signatures will be ambiguous. We will resolve these by adding a proxy parameter which fixes the ambiguity. For this, we use the (empty) Proxy
type:
> data Proxy a
> proxy :: Proxy a
> proxy = undefined
Values of type Proxy
contain no data, and should not be used by any functions; their only purpose is to fix the types.
As an example of how the disambiguation works, consider the type Conv vars r
. The variable vars
is only ever mentioned inside type functions, so it would be possible to have two types vars1
and vars2
such that Conv vars1 r ~ Conv vars2 r
but not vars1 ~ vars2
. Hence, if we fix the type of Conv vars r
, then we don’t know what vars
is, i.e. vars
is ambiguous in Conv vars r
. To fix this ambiguity, we add a parameter which fixes vs
, to get the new type
Proxy vars -> Conv vars r
Since Proxy
is injective, we can find vars
unambiguously by looking at the first parameter.
The List
class
It will turn out that Morten’s code implicitly uses various properties of list concatenation: in fact, precisely the property that lists form a monoid under ((:++:)
,Nil
). In his code, there is no need to prove that this is true, since his types don’t mention lists explicitly. However, we are using type families, so GHC will need to know these properties in order to type-check our code. Since type families are open, these properties cannot be guaranteed to be true of all instances of (:++:)
: there is nothing to stop someone else defining instances for which the monoid laws fail. Ideally, we would solve this by using Type Invariants for Haskell, but this has not been implemented in GHC. Instead, we encode these axioms as GADTs in a type-class:
> class List a where
> closure :: forall b. List b =>
> Proxy a -> Proxy b ->
> ListD (a :++: b)
> assoc :: forall b c.
> Proxy a -> Proxy b -> Proxy c ->
> ((a :++: (b :++: c)) :==: ((a :++: b) :++: c))
> rightIdent :: Proxy a ->
> (a :++: Nil) :==: a
(In comparison to the monoid laws, this is missing the leftIdent
law. This is because GHC can derive that itself from the type family instance Nil :++: xs
.) This class relies on the types (:==:)
and ListD
, which we have not yet defined, with the following intended meanings: an value of type a :==: b
means that a
and b
are equal types; an value of type ListD a
means that a
is an instance of List
. Both of these types can straightforwardly be defined using GADTs:
> data a :==: b where
> Equal :: a :==: a
>
> data ListD a where
> ListD :: List a => ListD a
We can also define instances for the lists we are interested in (i.e. the ones constructed with Nil
and :*:
). We need to tell GHC where to use induction, but it can prove the rest.
> instance List Nil where
> closure _ _ = ListD
> assoc _ _ _ = Equal
> rightIdent _ = Equal
>
> instance List t => List (h :*: t) where
> closure _ b = case closure (proxy :: Proxy t) b of
> ListD -> ListD
> assoc _ b c = case assoc (proxy :: Proxy t) b c of
> Equal -> Equal
> rightIdent _ = case rightIdent (proxy :: Proxy t) of
> Equal -> Equal
Types for Morten’s primitives
If we look at Morten’s code, we see that the pattern combinators are all 2-tuples. When larger pattern combinators are built from smaller ones, the first components are always built using only the first components of the smaller combinators, and similarly for the second. In other words, the first and second components of the pattern combinators can be constructed independently. So, instead of jumping straight to a type for patterns, we first give types to the first and second components and their combinators.
The first component: curried-to-uncurried-converter-builders
Morten manipulates the first components with the function
> succ n f = \(x,xs) -> n (f x) xs
and the Prelude functions id
and (.)
. The type of succ
inferred by GHCi is:
ghci> :type succ
succ :: (t2 -> t1 -> t3) -> (t -> t2) -> (t, t1) -> t3
which is not very helpful. Although the types of id
and (.)
are simpler, they also don’t give much information about the use in building pattern combinators. Our first aim will be to give meaningful types to these combinators.
Using a rough understanding of Morten’s code and a bit of guesswork, we can define the following type synonym
> type DConv1 vars = forall vars' r.
> Conv vars' r -> Conv (vars :++: vars') r
as the type of the first components of Morten’s pattern combinators. Then, we can give succ
and id
the following types:
> id1 :: DConv1 Nil
> id1 = id
> succ1 :: DConv1 (a :*: Nil)
> succ1 = succ
The type for (.)
is a bit harder, so I will pause now to discuss the interpretation of the DConv1
type. The type Conv vars r
is the type of converters from curried to uncurried form with arguments vars
and result r
. The type DConv1
builds larger converters from smaller converters, so it is a curried-to-uncurried-converter-builder. It is closely analogous to Difference Lists: a DConv1
accepts a tail (vars'
) as a parameter, and sticks its own list of variables onto the front. (This gives us a non-recursive implementation of append, which is what allows the pattern combinators to be completely optimised away by GHC.) So DConv1
is best thought of as the type of curried-to-uncurried converters but with an efficient append.
Under this intepretation, id1
is converter for no parameters, and succ1
is the converter for a single parameter.
Back to (.)
. This functions as the append operation (just like it does for DList
s), so it should have type
(.) :: DConv1 as -> DConv1 bs -> DConv1 (as :++: bs)
However, GHC won’t accept that type, for two reasons: DConv1 vars
is ambiguous with respect to vars
and vars'
; and we need to use the associativity of (:++:)
, but we don’t yet have a list constraint.
We fix the ambiguity of DConv1
by making it a newtype (which fixes vars
) and adding a proxy parameter (which fixes vars'
):
> newtype DConv vars = DConv { runDConv :: forall vars' r.
> Proxy vars' -> Conv vars' r -> Conv (vars :++: vars') r }
Then the combinators can be typed as
> idC :: DConv Nil
> idC = DConv (\_ -> id)
> succC :: DConv (a :*: Nil)
> succC = DConv (\_ -> succ)
> appendC :: forall as bs. List as => DConv as -> DConv bs -> DConv (as :++: bs)
> appendC (DConv fa) (DConv fb) =
> DConv (\(_ :: Proxy vars') ->
> case assoc (proxy :: Proxy as) (proxy :: Proxy bs) (proxy :: Proxy vars') of
> Equal -> fa (proxy :: Proxy (bs :++: vars')) . fb (proxy :: Proxy vars'))
Now, appendC
is considerably longer than the other two functions, but most of the length is just in the proxy types and GADT matches, to satisfy the typechecker. The actual data manipulation is still done by (.)
, which is hidden on the last line of its definition.
These are the only functions Morten uses to manipulate the first components, so we are done with the first component.
The second component: the actual matcher
The process here is similar to the process for the first component, only more complicated. First we find a type which the simple combinators unify with, then we fix the ambiguity problems, and then we discuss the interpretation of the type.
Other than ambiguity and type family problems, the second component of the patterns unifies with this type
> type Component2 vars pat =
> forall vars' r.
> pat -- pattern to match
> -> (UncurryFunc (vars :++: vars') r) -- success continuation
> -> (() -> r) -- failure continuation
> -> Tuple vars' -- already-pushed bindings
> -> r -- continuation result
We can cleanly separate the parts of the type mentioning pat
from the parts mentioning vars
to get
> type Component2' vars pat = pat -> Push1 vars
> type Push1 vars =
> forall vars' r.
> (UncurryFunc (vars :++: vars') r) -- success continuation
> -> (() -> r) -- failure continuation
> -> Tuple vars' -- already-pushed bindings
> -> r -- continuation result
The failure continuation has an odd-looking type, () -> r
. This is similar to the simpler type r
, and one might wonder why the failure continuation isn’t just defined like that. It turns out that the reason is the same as the reason that the success continuation must be uncurried internally: there are times when the success and failure continuations are swapped, so they must have unifiable types, so they must both be a type with a single function arrow. However, they still won’t unify, since that would require unifying ()
with Tuple (vars :++: vars')
, and those types might not be equal. Hence we change the failure continuation’s type to (forall s. s -> r)
. This makes Push1
a rank–3 type.
Making this change, and fixing the ambiguity of vars
and vars'
like we did before, we get the type
> newtype Push vars = Push { runPush ::
> forall vars' r.
> Proxy vars'
> -> (UncurryFunc (vars :++: vars') r)
> -> (forall s. s -> r)
> -> Tuple vars'
> -> r
> }
A value of type Push vars
is something which does the appropriate plumbing: it either pushes the variables in vars
onto the success continuation, or it calls the failure continuation. Below are the 5 functions Morten uses to manipulate (the equivalent of) Push
values. I give their equivalents in the Push
type (these are the functions with the P
suffix). All of them other than catchP
are defined using Morten’s function; in catchP
I needed to modify the failure continuation so that it accepts any parameter rather than just ()
, as discussed above.
> -- | succeeds without pushing any variables
> nil = \ks kf ac -> ks ac
> nilP :: Push Nil
> nilP = Push (\_ -> nil)
> -- | succeeds and pushes one variable
> one v = \ks kf ac -> ks (v,ac)
> oneP :: a -> Push (a :*: Nil)
> oneP v = Push (\_ -> one v)
> -- | Pushes the variables of the first, then the variables of the second (assuming the first succeeds).
> m # n = \ks kf ac -> n (m ks kf) kf ac
> appendP :: forall as bs. List as => Push as -> Push bs -> Push (as :++: bs)
> appendP (Push m) (Push n) =
> Push (\(_ :: Proxy vars') ->
> case assoc (proxy :: Proxy as) (proxy :: Proxy bs) (proxy :: Proxy vars') of
> Equal -> m (proxy :: Proxy (bs :++: vars')) # n (proxy :: Proxy vars'))
> -- | Calls the failure continuation immediately
> fail = \ks kf ac -> kf ()
> failP :: Push as
> failP = Push (\_ -> \ks kf -> fail ks kf)
> -- | Recovers from @m@'s failure by running @n@.
> m `catch` n = \ks kf ac -> m ks (\() -> n ks kf ac) ac
> catchP :: Push as -> Push as -> Push as
> catchP (Push m) (Push n) = Push (\p ks kf ac -> (m p) ks (\_ -> (n p) ks kf ac) ac)
I have omitted the types of Morten’s functions, as they are rather messy and not particularly informative. In contrast, the types of the Push
versions are quite informative: they give a list of variables pushed. In the case of failP
, it can claim that any number of variables can be pushed: like _|_, it doesn’t have to justify that claim, as it simply fails when run.
Types for patterns
Now we can (finally) give types to patterns. A pattern has a first component and a second component, and it also requires that vars
is a list (and it contains the evidence of that).
> data Pattern vars pat = List vars =>
> Pattern (DConv vars) (pat -> Push vars)
We can define all of Morten’s patterns almost as he defined them, since we have typed all of Morten’s primitive manipulation functions. I give the first few of them here:
> var :: Pattern (a :*: Nil) a
> var = Pattern succC oneP
> cst :: (Eq pat) => pat -> Pattern Nil pat
> cst v' = Pattern idC (\v -> if v == v' then nilP else failP)
> pair :: forall as a bs b. Pattern as a -> Pattern bs b -> Pattern (as :++: bs) (a,b)
> pair (Pattern pC pP) (Pattern qC qP) =
> case closure (proxy :: Proxy as) (proxy :: Proxy bs) of
> ListD -> Pattern (appendC pC qC) (\(a,b) -> pP a `appendP` qP b)
> none :: Pattern Nil pat
> none = Pattern idC (\v -> failP)
> (\/) :: Pattern t pat -> Pattern t pat -> Pattern t pat
> (Pattern pC pP) \/ (Pattern qC qP) =
> Pattern pC (\v -> pP v `catchP` qP v)
> any :: Pattern Nil pat
> any = Pattern idC (\v -> nilP)
> (/\) :: forall as bs a. Pattern as a -> Pattern bs a -> Pattern (as :++: bs) a
> (Pattern pC pP) /\ (Pattern qC qP) =
> case closure (proxy :: Proxy as) (proxy :: Proxy bs) of
> ListD -> Pattern (appendC pC qC) (\v -> pP v `appendP` qP v)
In pair
and (/\)
we unfortunately still need to use GADTs to prove the closure rule, but we can define all the other combinators without any cleverness. All the functions have informative types.
Types for clauses
We now have a nicely-typed way to construct patterns, but we still have no way to run them. There are three more primitive functions we need to define: match
, (->>)
and (||)
. Their use is best demonstrated by an example:
match ((3,4),5) $
pair (pair var var) cst 4 ->> \x y -> x + y
|| pair (pair (cst 3) (cst 4)) var ->> \x -> x
We first give the types that these functions should have. The (->>)
function should accept a pattern and an RHS and yield something which match
can be called on (call it a “clause”). The (||)
function should take two clauses and give a clause which tries the first clause, and then the second if the first failed. The match function should accept a value to match, and a clause which matches values of that type, and it should yield the value yielded by the clause. A clause’s type should say two things: what values it can match, and what the result value is.
So, the types are:
> (->>) :: forall vars a r.
> Pattern vars a -> CurryFunc vars r -> Clause a r
> (||) :: Clause a r -> Clause a r -> Clause a r
> match :: a -> Clause a r -> r
An implementation satisfying these types and semantics is below:
> newtype Clause pat res = Clause {
> runClause :: pat -> (forall s. s -> res) -> res
> }
> (Pattern c p) ->> k = Clause
> (case rightIdent (proxy :: Proxy vars) of
> Equal -> \v kf -> runPush (p v) (proxy :: Proxy Nil) (runDConv c (proxy :: Proxy Nil) zero k) kf ()) where
> zero f = \() -> f
> p1 || p2 = Clause (\pat kf -> runClause p1 pat (\_ -> runClause p2 pat kf))
> match a p = runClause p a (\_ -> error "match failed")
The precedences of the operators are
> infix 2 ->>
> infixr 1 ||
This is all the code we need to use our patterns in a nicely-typed way. As an example, we can write
> foo =
> pair (cst 2 \/ cst 3) any ->> "The tuple has either 2 or 3 as the first component"
> || pair any var ->> (\v -> "The second component has value " ++ show v)
> || var ->> (\v -> "The tuple is " ++ show v)
GHC will infer the type of this (under NoMonomorphismRestriction
) as
> foo :: (Num t, Show b) => Clause (t, b) [Char]
Wrapping up
Giving better types to the pattern combinators has benefits. These new types are “more static” than the original ones, which gives us the advantages of stronger typing.
The first advantage is that the code is more modular: we can define a pattern combinator independently of the others; if it has the desired type, we have quite good assurance that we have written it correctly. This was not the case for the original types, because it was hard to tell what the desired type actually was.
We can also provide an easier API for the user; the types of the pattern combinators actually give a lot of information about what they do. We are able to export the Pattern
type abstract, which we couldn’t do for Morten’s code, because there was no datatype.
One disadvantage is that we have lost Haskell98 compatibility: Type Families play a key role in assigning nicer types to the combinators. For my purposes, trading Haskell98 compatibility for nicer types is a good compromise.
One feature of Morten’s code is that all his functions are implemented non-recursively, so GHC is able to inline all the pattern combinators, and completely optimise away all the overhead. Unfortunately, the closure
function in the (h:*:t)
instance of List
is recursive; this recursion prevents GHC from inlining everything. So, we have lost some of the efficiency of Morten’s code. This is particularly unfortunate, because the actual working code is identical: the recursive code exists only to convince GHC that the types are correct. I have been working on an alternative implementation which uses unsafeCoerce
in appropriate places; I will post about this sometime in the future.