# Decidable Propositional Equality in Haskell

A recent discussion on the cvs-ghc mailing list touched on propositional decidable equality in Haskell. This post will explain propositional equality and consider different encodings of this idea in Haskell.

## Preface

This blog post is a literate Haskell file, compatible with GHC 7.6.1. As usual, we need some initial declarations to get off the ground.

``````> {-# LANGUAGE DataKinds, PolyKinds, GADTs, TypeFamilies,
>              LambdaCase #-}
> {-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
>
> data Nat = Zero | Succ Nat
``````

Throughout the post, I will be talking about equality on `Nat`s, but the ideas here extend to any types that would admit a good instance of `Eq`.

We will need length-indexed vectors to make interesting use of the ideas here:

``````> data Vec :: * -> Nat -> * where
>   VNil  :: Vec a Zero
>   VCons :: a -> Vec a n -> Vec a (Succ n)
>
> safeHead :: Vec a (Succ n) -> a
> safeHead (VCons h _) = h
>
> safeTail :: Vec a (Succ n) -> Vec a n
> safeTail (VCons _ t) = t
``````

Note that there is no need for another clause for `safeHead` or `safeTail` because the types forbid, for example, `safeHead VNil`.

## Propositional Equality

We are all (hopefully?) familiar with Boolean equality:

``````> boolEq :: Nat -> Nat -> Bool
> boolEq Zero     Zero     = True
> boolEq (Succ a) (Succ b) = boolEq a b
> boolEq _        _        = False
``````

We can even lift this idea to the type level:

``````> type family BoolEq (a :: Nat) (b :: Nat) :: Bool
> type instance BoolEq Zero Zero = True
> type instance BoolEq (Succ a) (Succ b) = BoolEq a b
> type instance BoolEq Zero (Succ x) = False
> type instance BoolEq (Succ x) Zero = False
``````

Let’s try to write a function to retrieve the second element from a vector:

``````cadr :: Vec a n -> a

We get an error:

``Couldn't match type `n' with 'Succ ('Succ n0)``

Naturally, GHC can’t confidently apply `safeHead` and `safeTail` because we don’t know that `v` has at least 2 elements.

Let’s try again:

``````cadr :: (BoolEq n (Succ (Succ n')) ~ True) => Vec a n -> a

Still doesn’t work:

``````Could not deduce (n ~ 'Succ ('Succ n0))
from the context (BoolEq n ('Succ ('Succ n')) ~ 'True)``````

The problem is that GHC doesn’t know that our Boolean equality function really shows the equality of two types.

This is a contrived example, though. Instead, let’s consider a program passing around explicit evidence of whether or not a list has at least two elements. If the list doesn’t, the function should return a supplied default.

To pass around evidence of a type-level Boolean quantity, we need the singleton type for Booleans:

``````> data SBool :: Bool -> * where
>   STrue  :: SBool True
>   SFalse :: SBool False
``````

(If you’ve never seen singleton types before, my singletons paper on the subject contains helpful information.)

``````cadr :: SBool (BoolEq n (Succ (Succ n'))) -> a -> Vec a n -> a
cadr evidence deflt v = case evidence of
SFalse -> deflt``````

Still, no go:

``````Could not deduce (n ~ 'Succ ('Succ n0))
from the context (BoolEq n ('Succ ('Succ n')) ~ 'True)
bound by a pattern with constructor
STrue :: SBool 'True,``````

In the end, this last example is the same as the previous. Pattern-matching on the `SBool` just brings the equality `(BoolEq n (Succ (Succ n'))) ~ True` into the context.

We need to convert Boolean equality to propositional equality, which is denoted by `~`. Propositional equality is an equality among types that GHC can make use of in type checking code. To work with propositional equality, we need to make it first class, instead of just a constraint.

``````> data PropEq :: k -> k -> * where
>   Refl :: PropEq x x
``````

Let’s now try to write a conversion function from Boolean equality to propositional equality:

``````boolToProp :: (BoolEq a b ~ True) => PropEq a b
boolToProp = Refl``````

Same old problem:

``````Could not deduce (a ~ b)
from the context (BoolEq a b ~ 'True)``````

What we need to do is to build up the propositional equality from pieces that GHC can easily verify are indeed equal. We need an inductive proof that our definition of Boolean equality is correct for any natural number. To write such a proof, we will need to do case analysis on a and b. To do that, in turn, we will need a singleton over natural numbers.

``````> data SNat :: Nat -> * where
>   SZero :: SNat Zero
>   SSucc :: SNat n -> SNat (Succ n)
``````

Now, let’s write the inductive proof:

``````boolToProp :: (BoolEq a b ~ True) => SNat a -> SNat b -> PropEq a b
boolToProp SZero SZero = Refl
boolToProp (SSucc x') (SSucc y') = boolToProp x' y'``````

Oops:

``````Could not deduce (n ~ 'Succ n)
...
Could not deduce (n1 ~ 'Succ n1)``````

The problem is that we are returning the result of `boolToProp x' y'` directly from `boolToProp`, even though `x'` and `y'` have different types than `SSucc x` and `SSucc y`. The solution is to use a pattern match on the result from the recursive call. Let’s call the type index associated with `x'` to be `a'` and that with `y'` to be `b'`. Then, the recursive call gives us `(Refl :: PropEq a' b')`. If we pattern match on this, we get the propositional equality `a' ~ b'` into the context. This can be used to show `Succ a' ~ Succ b'` (which is really just `a ~ b`), so we can now use `Refl` once again, though at a different type:

``````> boolToProp :: (BoolEq a b ~ True) => SNat a -> SNat b -> PropEq a b
> boolToProp SZero SZero = Refl
> boolToProp (SSucc a') (SSucc b') =
>   case boolToProp a' b' of
>     Refl -> Refl
``````

Great. Except now we get this warning:

``````Pattern match(es) are non-exhaustive
In an equation for `boolToProp':
Patterns not matched:
SZero (SSucc _)
(SSucc _) SZero``````

The problem is that there is no possible way out in these cases, so we’ll just have to put undefined:

``````boolToProp SZero (SSucc _) = undefined
boolToProp (SSucc _) SZero = undefined``````

Wait. Now there’s a new problem:

``````Couldn't match type 'False with 'True
Inaccessible code in ...
Couldn't match type 'False with 'True
Inaccessible code in ...``````

GHC rightly determines that these cases are impossible. Why are they impossible? Because we know that `BoolEq a b ~ True`. In these cases, that wouldn’t be the case, so GHC can’t match `False` with `True`.

But now we are in a quandary. Without the extra matches, we get a warning (due to `-fwarn-incomplete-patterns`, which you should never leave home without). With the matches, we get an error. That’s silly. And others agree that it’s silly, filing bug report #3927. According to the commentary on the bug report, Simon PJ says, “The more complaints the more likely I am to put off other things to do this one!” So, at the risk of pestering dear Simon, if you are annoyed by this, please complain! The best way to complain is simply to add yourself to the Cc list of the bug report. If enough people do this, the bug will get fixed sooner. Or, even better, try to fix it yourself!

So, where does this leave us? I can’t stand a warning in my code, so we’ll suppress it with this:

``````> boolToProp _ _ = error "bug 3927"
``````

Let’s try to write `cadr` one last time, this time armed with `boolToProp`:

``````> cadr :: SBool (BoolEq n (Succ (Succ n'))) -> SNat n
>      -> SNat n' -> a -> Vec a n -> a
> cadr evidence n n' deflt v = case evidence of
>   STrue -> case boolToProp n (SSucc (SSucc n')) of
>     Refl -> safeHead (safeTail v)
>   SFalse -> deflt
``````

It works! Hurrah!

The sad part here is that, to make it work, we needed to pass around two `SNat`s and perform an O(n) operation (at runtime – the `boolToProp` “proof” runs!) to prove to GHC that the operation is valid. Can we do better?

## Decidable Propositional Equality

Yes, we can.

The problem lies in the fact that we branch on a witness of Boolean equality. There is an alternative: decidable propositional equality. The idea is that instead of just type-level Booleans, decidable equality stores either evidence that two types are equal or evidence that they are not. We know how to write evidence that two types `a` and `b` are equal: `PropEq a b`. What’s the opposite of `PropEq a b`? It’s the statement that `PropEq a b` implies falsehood. In Haskell, we can represent falsehood with an empty type.

``````> data Falsehood
> type Not a = a -> Falsehood
``````

Now, we can define decidable equality in Haskell:

``````> type DecidableEquality (a :: k) (b :: k) = Either (PropEq a b) (Not (PropEq a b))
``````

We can even write a function to decide equality over `Nat`s. Because this function produces runtime evidence, it uses singletons to work with types.

``````> decEq :: SNat a -> SNat b -> DecidableEquality a b
> decEq SZero SZero = Left Refl
> decEq (SSucc x') (SSucc y') = case decEq x' y' of
>   Left Refl -> Left Refl
>   Right contra -> Right (\case Refl -> contra Refl)
``````

There’s a little magic going on here, so let’s pause and reflect. The first equation is straightforward. In the second, we recur on `a'` and `b'`. If those in fact are equal, we still unpack the `Left Refl` result and create a new `Left Refl` at a different type. We’ve seen this before, so it’s OK.

But what’s going on with `Right`? Once again, let’s call the type index associated with `x'` to be `a'`, and likewise with `y'` and `b'`. The return type of `decEq x' y'` is `DecidableEquality a' b'`. Because we’ve matched with `Right`, we know that `contra` must have type `Not (PropEq a' b')`, synonymous with `PropEq a' b' -> Falsehood`. We must produce something of type `PropEq a b -> Falsehood`. So, we write a lambda-case pattern match on the `PropEq a b` to get the equality `a ~ b`. Because `a` is `Succ a'` and `b` is `Succ b'`, GHC can use `a ~ b` to derive `a' ~ b'`, and thus we can call `contra` with `Refl :: PropEq a' b'`. Whew.

Now, we deal with the failure cases. If we know that, say, `a` is `Zero` and `b` is `Succ b'`, then GHC rightly figures out that `PropEq a b` (which expands to `PropEq Zero (Succ b')`) is an empty type.

``````decEq SZero (SSucc _) = Right (\case {})
decEq (SSucc _) SZero = Right (\case {})``````

No go:

``parse error on input `}'``

GHC does not support empty pattern matches. (UPDATE [Jan 4, 2013]: Simon PJ has implemented empty pattern matches in HEAD. Yay!) A feature request to support these was submitted as bug report #2431. Drat. Explicitly pattern matching on `Refl` gives us an inaccessible code error (correctly), so we are forced to do this dreadful workaround:

``````> decEq SZero (SSucc _) = Right (\_ -> error "bug 2431")
> decEq (SSucc _) SZero = Right (\_ -> error "bug 2431")
``````

(Incidentally, this bug seems much easier to fix than #3927, so if you have a little time, go for it!)

So, now that we’ve defined `decEq`, how can we use it? Let’s write a wrapper around `safeHead` with evidence. We’ll first need a way to eliminate `Falsehood`. From logic, we learn that falsehood implies anything, neatly expressed in this type:

``````> exFalsoQuodlibet :: Falsehood -> a
``````

Unfortunately, even with a manifestly empty type, we can’t use an empty pattern match. So, we do this:

``````> exFalsoQuodlibet = \case _ -> error "bug 2431"
``````

Here is the type for our new head operation:

``````> safeHead' :: DecidableEquality n Zero -> SNat n -> a -> Vec a n -> a
``````

In this example, as opposed to above, we reason about whether `n` is `Zero`. Because we set the example up this way, the evidence when `n` is not `Zero` will be necessary for a complete definition of the `safeHead'` operation.

``````> safeHead' (Left Refl) _ deflt _ = deflt
> safeHead' (Right contra) n _ v = case n of
>   SZero -> exFalsoQuodlibet (contra Refl)
>   SSucc _ -> safeHead v
``````

Note that this definition is complete: we can use the primitives that we have built up to eliminate the impossible case match. Of course, those primitives had to avoid empty pattern matches. However, it is easy to imagine a future where bugs #2431 and #3927 are gone and we can define this without any partial features of Haskell.

I should also note that we can’t use `exFalsoQuodlibet (contra Refl)` in the `SSucc _` case. GHC rightly complains `Couldn't match type 'Succ n1 with 'Zero` in the use of `Refl`.

Fun stuff, no?

# Variable-arity zipWith

At ICFP in September, an interesting problem was posed: Is it possible to define a variable-arity `zipWith` in Haskell using GHC 7.6.1? Can we leverage the new expressivity in promoted types and kinds to do away with `zipWith3`, `zipWith4` and friends? The answer turns out to be yes.

Let’s start by enabling a bunch of non-controversial language options and declaring the module:

``````{-# LANGUAGE TypeFamilies, ExplicitForAll, DataKinds, GADTs,
MultiParamTypeClasses, FlexibleInstances, FlexibleContexts #-}

module ZipWith where

import Prelude hiding (zipWith)``````

Though promotion is not strictly necessary to pull this off, it turns out to be convenient for GHC to kind-check our code. We define the natural numbers to use at the kind level:

``data Nat = Zero | Succ Nat``

Now, we need to start thinking about what the type of a variable-arity `zipWith` must be. Clearly, it will need to take the function to apply and a bunch of lists, but the number of lists is not known when we write the type. We correspondingly don’t know how many arguments the function itself should take. We’ve narrowed our type down to `f -> <dragons>`, for some function type `f`. The dragons will have to be some type-level function that evaluates to the correct sequence of arrows and argument types, based on the type substituted for `f`.

Examples may help here:

• If `f` is `a -> b`, then the dragons should be `[a] -> [b]`.
• If `f` is `a -> b -> c`, then the dragons should be `[a] -> [b] -> [c]`.
• and so on.

OK. That’s not too hard. We essentially want to map the type-level `[]` operator over the components of the type of `f`. However, a problem lurks: what if the final result type is itself an arrow? In the first example above, there is nothing stopping `b` from being `d -> e`. This turns out to be a fundemental ambiguity in variable-arity `zipWith`. Let’s explore this for a moment.

We’ll need a three-argument function to make the discussion interesting. Here is such a function:

``````splotch :: Int -> Char -> Double -> String
splotch a b c = (show a) ++ (show b) ++ (show c)``````

Now, there are two conceivable ways to apply `splotch` with `zipWith`:

``````*ZipWith> :t zipWith2 splotch
zipWith2 splotch :: [Int] -> [Char] -> [Double -> String]
*ZipWith> :t zipWith3 splotch
zipWith3 splotch :: [Int] -> [Char] -> [Double] -> [String]``````

(Here, `zipWith2` is really just the `zipWith` in the Prelude.)

In general, there is no way for an automated system to know which one of these possibilities we want, so it is sensible to have to provide a number to the dragons, which we’ll now name `Listify`. This number is the number of arguments to the function `f`. Here is the definition for `Listify`:

``````-- Map the type constructor [] over the types of arguments and return value of
-- a function
type family Listify (n :: Nat) (arrows :: *) :: *
type instance Listify (Succ n) (a -> b) = [a] -> Listify n b
type instance Listify Zero a = [a]``````

Now it would seem we can write the type of `zipWith`. Except, when we think about it, we realize that the operation of `zipWith` will have to be different depending on the choice for `n` in `Listify`. Because this `n` is a type, it is not available at runtime. We will need some runtime value that the implementation of `zipWith` can branch on.

Furthermore, we will need to convince GHC that we’re not doing something very silly, like trying `Listify (Succ (Succ (Succ Zero))) (Int -> Int)`. So, we create a GADT that achieves both of these goals. A value from this GADT will both be a runtime witness controlling how `zipWith` should behave and will assert at compile time that the argument to `Listify` is appropriate:

``````-- Evidence that a function has at least a certain number of arguments
data NumArgs :: Nat -> * -> * where
NAZero :: NumArgs Zero a
NASucc :: NumArgs n b -> NumArgs (Succ n) (a -> b)

oneArg = NASucc NAZero
twoArgs = NASucc oneArg
threeArgs = NASucc twoArgs``````

Finally, we can give the type for `zipWith`:

``zipWith :: NumArgs numArgs f -> f -> Listify numArgs f``

Note that, though this `zipWith` is variable-arity, we still have to tell it the desired arity. More on this point later.

Once we have the type, we still need an implementation, which will need to be recursive both in the length of the lists and the number of arguments. When we think about recursion in the number of arguments to `f`, currying comes to the rescue… almost. Consider the following:

``zipWith threeArgs splotch [1,2] ['a','b'] [3.5,4.5]``

We would like a recursive call to come out to be something like

``zipWith twoArgs  ['a','b'] [3.5,4.5]``

The problem is that there is no replacement for `<splotch ??>` that works. We want to apply `(splotch 1)` to the first members of the lists and to apply `(splotch 2)` to the second members. What we really need is to take a list of functions to apply. Let’s call the function that works with list of functions `listApply`. Then, the recursive call would look like

``listApply twoArgs [splotch 1, splotch 2] ['a','b'] [3.5,4.5]``

With such a `listApply` function, we can now implement `zipWith`:

``zipWith numArgs f = listApply numArgs (repeat f)``

The type and implementation of `listApply` is perhaps a little hard to come up with, but otherwise unsurprising.

``````-- Variable arity application of a list of functions to lists of arguments
-- with explicit evidence that the number of arguments is valid
listApply :: NumArgs n a -> [a] -> Listify n a
listApply NAZero fs = fs
listApply (NASucc na) fs = listApply na . apply fs
where apply :: [a -> b] -> [a] -> [b]
apply (f:fs) (x:xs) = (f x : apply fs xs)
apply _      _      = []``````

And now we’re done. Here are some examples of it all working:

``````example1 = listApply (NASucc NAZero) (repeat not) [False,True]
example2 = listApply (NASucc (NASucc NAZero)) (repeat (+)) [1,3] [4,5]

example3 = zipWith twoArgs (&&) [False, True, False] [True, True, False]
example4 = zipWith twoArgs (+) [1,2,3] [4,5,6]

example5 = zipWith threeArgs splotch [1,2,3] ['a','b','c'] [3.14, 2.1728, 1.01001]``````

But wait: can we do better? The `zipWith` built here still needs to be told what its arity should be. Notwithstanding the ambiguity mentioned above, can we somehow infer this arity?

I have not come up with a way to do this in GHC 7.6.1. But, I happen to (independently) be working on an extension to GHC to allow ordering among type family instance equations, just like equations for term-level functions are ordered. GHC will try the first equation and then proceed to other only if the first doesn’t match. The details are beyond the scope of this post (but will hopefully appear later), but you can check out the GHC wiki page on the subject. The following example should hopefully make sense:

``````-- Count the number of arguments of a function
type family CountArgs (f :: *) :: Nat
type instance where
CountArgs (a -> b) = Succ (CountArgs b)
CountArgs result = Zero``````

This function counts the number of arrows in a function type. Note that this cannot be defined without ordered equations, because there is no way in GHC 7.6.1 to say that `result` (the type variable in the last equation) is not an arrow.

Now, all we need to do is to be able to make the runtime witness of the argument count implicit through the use of a type class:

``````-- Use type classes to automatically infer NumArgs
class CNumArgs (numArgs :: Nat) (arrows :: *) where
getNA :: NumArgs numArgs arrows
instance CNumArgs Zero a where
getNA = NAZero
instance CNumArgs n b => CNumArgs (Succ n) (a -> b) where
getNA = NASucc getNA``````

Here is the new, implicitly specified variable-arity `zipWith`:

``````{-# LANGUAGE ScopedTypeVariables #-}
-- Variable arity zipWith, inferring the number of arguments and using
-- implicit evidence of the argument count.
-- Calling this requires having a concrete return type of the function to
-- be applied; if it's abstract, we can't know how many arguments the function
-- has. So, zipWith (+) ... won't work unless (+) is specialized.
zipWith' :: forall f. CNumArgs (CountArgs f) f => f -> Listify (CountArgs f) f
zipWith' f = listApply (getNA :: NumArgs (CountArgs f) f) (repeat f)``````

This version does compile and work with my enhanced version of GHC. Expect to see ordered type family instances coming to a GHC near you soon!