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 `CoerceD`

s 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.

[...] 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 |