Reiner Pope

July 18, 2009

Building first-class patterns. The “Difference type-list”.

Filed under: pattern-combinators — Reiner Pope @ 9:54 am
Tags:

This post is in Literate Haskell. The entire contents can be copied into a file called Difference.lhs and will be compilable by GHC.

In my previous post I used type families to simplify the types in Morten Rhiger’s “Type safe pattern combinators”. Unfortunately, in order to convince GHC that various types were in fact equal (such as (a :++: b) :++: c and a :++: (b :++: c)) we needed to (recursively) build type equality witnesses. In doing this, we prevented GHC optimising away all the overhead, since GHC will never inline a recursive function.

In this post I start to solve the efficiency problem by using unsafeCoerce. By carefully choosing the exports from the module, we can ensure that the API presented is never-the-less safe.

Type lists, again

These are the same as defined in the previous post, so I give no explanation of them.

> {-# LANGUAGE TypeFamilies, EmptyDataDecls, TypeOperators, ScopedTypeVariables, Rank2Types, GADTs, GeneralizedNewtypeDeriving #-}
> module Difference(
>     Nil,
>     (:*:),
>     (:++:),
>     Difference(..),
>     D,
>  ) where
>
> import Unsafe.Coerce
>
> data Nil
> data h :*: t
> infixr :*:
> type family (:++:) a b
> type instance Nil     :++: xs = xs
> type instance (h:*:t) :++: xs = h :*: (t :++: xs)
> data Proxy a
> proxy :: Proxy a
> proxy = undefined

Difference type-lists

It will be (also, has been) a common theme in building the pattern combinators to define a type inductively for lists. For instance, in the previous post, we defined Tuple xs and CurryFunc xs as types on lists, essentially as folds on the list structure: e.g. with Tuple, replace every (:*:) with a (,), and every Nil with a ().

We can efficiently (read: non-recursively) build objects of these types when we only build the types using Nil and (:*:); however, we have more difficulties when we want to efficiently construct such types using (:++:). For instance, suppose we wanted to construct a function

f :: Tuple xs -> Tuple ys -> Tuple (xs :++: ys)

With the definition of Tuple used in the previous post, we would find it difficult (impossible?) to define such a function non-recursively.

In the previous post, this problem was solved by the “difference list” technique, which we used for the DConv type. It will be convenient to use difference list technique again. Here we package the technique in a single convenient type, D, which adds efficient (non-recursive) concatenation to datatypes defined on type-lists.

We put the operations we will need in a type-class, Difference, which is defined below. The idea is that, if d is an instance of Difference, and t is some datatype defined inductively on lists, then d t is the “difference list converted” version of this type — that is, it contains the same data, but with an efficient append.

> class Difference d where
>     -- | constructs the empty `d t`.
>     zeroD :: d t Nil
>     -- | appends two `d t`s.
>     plusD :: d t xs -> d t ys -> d t (xs :++: ys)
>     -- | given a "cons" operation, constructs the singleton `d t`.
>     mkOneD :: (forall ys. t ys -> t (a :*: ys)) -> d t (a :*: Nil)
>     -- | given a "nil" value, "runs" the `d t`.
>     evalD :: t Nil -> d t xs -> t xs

It is interesting that zeroD and plusD can be defined without any knowledge of the underlying type: internally, they will be implemented just as id and (.). All the knowledge is contained within mkOneD and evalD.

As a demonstration of its use, we can define difference tuples. Note that the t mentioned in the typeclass above must have kind (* -> *). This means that t cannot be a type family. However, it can be a data family, so this is how we define tuples. First, we define tuples inductively:

> data family Tuple' xs
> data instance Tuple' Nil = TupleEmpty
> data instance Tuple' (h:*:t) = TupleCons h !(Tuple' t)

The zeroD and plusD functions need no work. However, we need a little work for the singleton and evaluation functions, mkOneD and evalD:

> singletonTuple :: Difference d => a -> d Tuple' (a :*: Nil)
> singletonTuple a = mkOneD (\t -> TupleCons a t)
> evalTuple :: Difference d => d Tuple' xs -> Tuple' xs
> evalTuple = evalD TupleEmpty

There we have it: tuples with efficient append.

Now we actually need to define an instance of Difference.

Instances

The basic idea of the implementation is just

type D t xs = forall ys. t ys -> t (xs :++: ys)

However, to implement plusD, we will need to convince GHC of the equality of the types (a :++: b) :++ c and a :++: (b :++: c). I give two instances of Difference, which differ in how they prove this equality: one uses GADTs and a List type-class (as in the previous post); the other uses unsafeCoerce. As opposed to the unsafeCoerce approach, the GADT approach is guaranteed to be safe, but is recursive. The unsafeCoerce is non-recursive but circumvents the type system; however, the existence of the GADT implementation should convince us that the use of unsafeCoerce here is actually a safe one.

The GADT instance

This is very similar to the previous post, so I don’t give much explanation.

> data GadtD t xs = List xs => GadtD (forall ys. t ys -> t (xs :++: ys))
>
> instance Difference GadtD where
>     zeroD = GadtD id
>     plusD (GadtD fx :: GadtD t xs) (GadtD fy :: GadtD t ys) = 
>         case closure (proxy :: Proxy xs) (proxy :: Proxy ys) of
>           ListD -> GadtD (\(zs :: t zs) -> 
>             case assoc (proxy :: Proxy xs) (proxy :: Proxy ys) (proxy :: Proxy zs) of
>               Equal -> fx (fy zs))
>     mkOneD f = GadtD f
>     evalD nil (GadtD f :: GadtD t xs) =
>         case rightIdent (proxy :: Proxy xs) of
>           Equal -> f nil
>
> 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
>
> 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
>
> data a :==: b where
>     Equal :: a :==: a
> data ListD a where
>     ListD :: List a => ListD a

The unsafeCoerce instance

This instance is a lightweight one. It is the same as the GADT one except that, whenever we needed an equality proof before, we use unsafeCoerce.

> newtype CoerceD t xs = CoerceD (forall ys. t ys -> t (xs :++: ys))
>
> instance Difference CoerceD where
>     zeroD = CoerceD id
>     plusD (CoerceD fx :: CoerceD t xs) (CoerceD fy :: CoerceD t ys) = 
>         CoerceD (\(zs :: t zs) ->
>             case assoc2 (proxy :: Proxy xs) (proxy :: Proxy ys) (proxy :: Proxy zs) of
>               Equal -> fx (fy zs))
>     mkOneD f = CoerceD f
>     evalD nil (CoerceD f :: CoerceD t xs) = 
>         case rightIdent2 (proxy :: Proxy xs) of
>           Equal -> f nil
>
> assoc2 :: Proxy a -> Proxy b -> Proxy c -> (a :++: (b :++: c)) :==: ((a :++: b) :++: c)
> assoc2 _ _ _ = unsafeCoerce Equal
>
> rightIdent2 :: Proxy a -> (a :++: Nil) :==: a
> rightIdent2 _ = unsafeCoerce Equal

The only equalities we prove with unsafeCoerce are a :++: (b :++: c) ~ (a :++: b) :++: c and a :++: Nil ~ a. These equalities are certainly true for all instances of the List class given in the GADT implementation. The GADT implementation also shows that, for any value of type d t xs constructible using the API of the Difference class, xs will be an instance of List. So the equalities used are true (safe) for any CoerceDs constructed using only the Difference interface. So our use of unsafeCoerce is safe if we export only the Difference class, and the name of the type CoerceD. If you look at the imports, this is what I have done.

Wrapping up

Finally, I also export the type D, which is just a newtype of CoerceD, with a derived instance of Difference:

> newtype D t xs = D (CoerceD t xs) deriving(Difference)

This exposes an instance of Difference to the outside world, but hides which one it is. This gives us a single place to change the implementation from CoerceD to GadtD if we so desire.

It turns out that this module encapsulates all the uses of GADTs that we will need.

I’ll stop here for now, but we will see in later posts how this type is used, and we will see the efficiency it allows.

About these ads

1 Comment »

  1. […] my previous post I developed difference type-lists with non-recursive append. Using that framework, we can solve the […]

    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: