Reiner Pope

June 29, 2009

Nicer types for Type-safe pattern combinators

Filed under: pattern-combinators — Reiner Pope @ 12:29 pm
Tags:

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 Lists1: 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 DLists), 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.


  1. Hence the choice of name for DConv.
About these ads

2 Comments »

  1. [...] my previous post I used type families to simplify the types in Morten Rhiger’s “Type safe pattern [...]

    Pingback by Building first-class patterns. The “Difference type-list”. « Reiner Pope — July 18, 2009 @ 9:54 am | Reply

  2. [...] with non-recursive append. Using that framework, we can solve the efficiency problem of my first attempt at nicer types for pattern combinators. At the same time, I find the implementation here easier to [...]

    Pingback by Building first-class patterns, continued. « Reiner Pope — July 19, 2009 @ 1:50 am | Reply


RSS feed for comments on this post. TrackBack URI

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s

The Rubric Theme. Create a free website or blog at WordPress.com.

Follow

Get every new post delivered to your Inbox.

%d bloggers like this: