Parity Clarity

Sometimes good performance seems to be in direct conflict with programmer-understandable types. This post is about ways to get fast parity checking on natural number types, while also maintaining as many invariants as possible automatically. The example here is definitely contrived—if you wanted fast numeric parity calculations you could just check the lowest bit. However, it’s a pretty good stand-in for more complicated encodings, and how we can play with them to make them both performant and easy to understand. Along the way we’ll briefly touch on some cool Haskell language extensions: type families, GADTs, and data kinds.

Let’s start with a tiny subset of the Prelude, and we’ll also define a Bool type as well as the not operation on it which we can use later.

import Prelude((++), Show(..))

data Bool = True | False
  deriving Show

not :: Bool -> Bool
not False = True
not True = False

Hopefully this is straightforward. Here’s our stand-in for an existing type with a focus on understandability by human programmers. We’re encoding natural numbers as Peano numerals, where Z means 0, and S means successor. Let’s also throw in a helpful succ function for finding successors.

data Nat
  = Z
  | S Nat
  deriving Show

succ :: Nat -> Nat
succ = S

Our version of succ here only needs to provide the S constructor, which means it’s simple to write and easy to understand.

For whatever reason, the other constraint on our type is that we want fast parity checking, i.e. a way to tell whether a number is even or odd. Let’s write a version of that now.

even :: Nat -> Bool
even Z = True
even (S Z) = False
even (S (S n)) = even n

odd :: Nat -> Bool
odd n = not (even n)

Here we’re deconstructing our Nat and recursively finding out whether it’s even by reducing the number by two, and checking the parity of that. Intuitively, this works, because we always end at one of the base cases and are making the number smaller at each step. However, it’s rather slow. We’re taking around \(n/2\) steps to check the parity of a number \(n\), which means the runtime of this function grows linearly with the size of its input. Let’s see if we can do better.

Here’s another idea: we can encode odd and even numbers separately. This way, there’s an easy way to check a number’s parity from its encoding in a single step. Maybe our new data type looks like this:

data ParityNat
  = ZZ
  | SO Parity Nat
  | SE ParityNat
  deriving Show

ZZ is the equivalent of Z in Nat, but now we have both an SO (“odd successor”) and an SE (“even successor”). This makes the succ function a bit more complicated now:

succPar :: ParityNat -> ParityNat
succPar ZZ = SO ZZ
succPar n@(SO _) = SE n
succPar n@(SE _) = SO n

We want the SEs and SOs to alternate, which we can do as shown. However, note that now there’s a higher burden on people writing functions dealing with ParityNat as opposed to just plain Nats. Along with additional cases to handle, there are more places for implementations to contain errors. We’re also relying on people to use succ now, rather than just the plain data constructors. At least our new parity checking functions are speedy:

evenPar :: ParityNat -> Bool
evenPar ZZ = True
evenPar (SO _) = False
evenPar (SE _) = True

oddPar :: ParityNat -> Bool
oddPar n = not (evenPar n)

There’s another encoding option, which puts more burden on the author of the encoding, but hopefully automatically enforces more constraints for later users of the library. We can push parity checking into the types. First, let’s make a new type for the parity itself.

data Parity = Even | Odd
  deriving Show

If this seems weirdly familiar, that’s because it’s isomorphic to Bool which we defined earlier. We can also define a “not” operation on Paritys, but first let’s take one step back. If we want to enforce parity in types, having Even and Odd terms isn’t that helpful. We need to promote Parity to a kind, and promote Even and Odd to types. While we’re at it, let’s also add the type families extension so we can define the equivalent to our not function, but at the type level instead of the term level. All in all, we’ll want the following extensions enabled:

{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}

Now we can define the type-level equivalent of not, but for Parity instead of Bool. Let’s call it “Opp”. Here’s its definition:

type family Opp (n :: Parity) :: Parity
type instance Opp 'Even = 'Odd
type instance Opp 'Odd = 'Even

This may look bizarre, but it’s more or less just a different syntax for defining a function. Opp takes a Parity called n and returns a Parity. The opposite of even is odd, and the opposite of odd is even. The ticks in front of 'Even and 'Odd remind us that these have been promoted from terms to types.

We can now define our constructors analogous to Z and S. This stuff here is the reason we needed GADTs.

data Natural :: Parity -> * where
  Zero :: Natural 'Even
  Succ :: Natural p -> Natural (Opp p)

instance Show (Natural p) where
  show Zero = "Zero"
  show (Succ n) = "(Succ " ++ show n ++ ")"

Breaking this down a bit further, a Natural is a type which takes something of kind Parity and gives us back a normal type (something of kind *). Zero is even, and the Succ of any Natural has the opposite parity as that Natural.

The successor function is again trivial to write.

succNat :: Natural p -> Natural (Opp p)
succNat = Succ

Weirdly, it now almost doesn’t make sense to have even and odd functions. Because this information is encoded in the types, it’s already sort of carried along with every Natural. However, just for the sake of completeness we can write something like this:

evenNat :: Natural 'Even -> Bool
evenNat _ = True

oddNat :: Natural 'Odd -> Bool
oddNat _ = True

This was a brief tour of a few possible encodings for a small bit of data with additional outside constraints on it. The first encoding was very simple, but runtime for operations we care about a lot (even and odd) was too slow. We switched to the more performant ParityNat, but this came at the cost of ease of use when writing functions using that type. Finally, we sort of pushed the problem up to the type level so that anything of type Natural 'Even has even parity, and likewise any Natural 'Odd has odd parity. This did away with the need for parity checking as functions, but comes at the cost of a more complicated type system encoding of our desired result.

Like so many places in engineering, this provides an interesting example of multiple tradeoffs that have to be balanced. Normally I lean towards “clarity at most costs”, sacrificing performance to make programmers’ jobs more manageable. However, occasionally understandability has to be traded away for enhancements of the details of how our programs actually run, and this tradeoff is more common as systems become more heavily relied upon by others.