Conal Elliott

An Applicative instance

As a review, here is our Functor instance:

instance Functor (Vec n) where
  fmap _ ZVec     = ZVec
  fmap f (a :< u) = f a :< fmap f u

And part of an Applicative instance:

instance Applicative (Vec n) where
  pure a = ??
  ZVec      ⊛ ZVec      = ZVec
  (f :< fs) ⊛ (x :< xs) = f x :< (fs ⊛ xs)

For pure, recall the troublesome goal signature:

  pure ∷ a → Vec n a

There's at least one very good reason this type is problematic. The type n is completely unrestricted. There is nothing to require n to be a natural number type, rather than Bool, String, String → Bool, etc.

In contrast to this difficulty with pure, consider what if n ≡ String in the type of fmap:

fmap ∷ (a → b) → Vec n a → Vec n b

The definition of Vec guarantees that that there are no values of type Vec String a. So it's vacuously easy to cover that case (with an empty function). Similarly for (⊛).

If we were to somehow define pure with the type given above, then pure () would have type Vec String () (among many other types). However, there are no values of that type. Hence, pure cannot be defined without restricting n.

Since the essential difficulty here is the unrestricted nature of n, let's look at restricting it. We'll want to include exactly the types that can arise in constructing Vec values, namely Z, S Z, S (S Z), S (S (S Z)), etc.

As a first try, define a class with two instances:

class IsNat n

instance IsNat Z
instance IsNat n ⇒ IsNat (S n)

Then change the Applicative instance to require IsNat n:

instance IsNat n ⇒ Applicative (Vec n) where
  ⋯

The definition of (⊛) given above still type-checks. Well, not quite. Really, the recursive call to (⊛) fails to type-check, because the IsNat constraint cannot be proved. One solution is to add that constraint to the vector type:

data Vec ∷ * → * → * where
  ZVec ∷ Vec Z a
  (:<) ∷ IsNat n ⇒ a → Vec n a → Vec (S n) a

Another is to break the definition (⊛) out into a separate recursion that omits the IsNat constraint:

instance IsNat n ⇒ Applicative (Vec n) where
  pure = ???
  (⊛)  = applyV

applyV ∷ Vec n (a → b) → Vec n a → Vec n b
ZVec      `applyV` ZVec      = ZVec
(f :< fs) `applyV` (x :< xs) = f x :< (fs `applyV` xs)

Now, how can we define pure? We still don't have enough structure. To get that structure, add a method to IsNat. That method could simply be the definition of pure that we need.

class IsNat n where pureN ∷ a → Vec n a

instance IsNat Z                where pureN a = ZVec
instance IsNat n ⇒ IsNat (S n) where pureN a = a :< pureN a

To get this second instance to type-check, we'll have to add the constraint IsNat n to the (:<) constructor in Vec. Then define pure = pureN for Vec.

I prefer a variation on this solution. Instead of pureN, use a method that can only make vectors of ():

class IsNat n where units ∷ Vec n ()

instance            IsNat Z     where units = ZVec
instance IsNat n ⇒ IsNat (S n) where units = () :< units

Then define

  pure a = fmap (const a) units

Neat trick, huh? I got it from Applicative Programming with Effects (section 7).

Value-typed natural numbers

There's still another way to define IsNat, and it's the one I actually use.

Define a type of natural number with matching value & type:

data Nat ∷ * → * where
  Zero ∷                    Nat Z
  Succ ∷ IsNat n ⇒ Nat n → Nat (S n)

Interpret a Nat as an Integer

natToZ ∷ Nat n → Integer
natToZ Zero     = 0
natToZ (Succ n) = (succ ∘ natToZ) n

I wrote the second clause strangely to emphasize the following lovely property, which corresponds to a simple commutative diagram:

natToZ ∘ Succ = succ ∘ natToZ

This natToZ function is handy for showing natural numbers:

instance Show (Nat n) where show = show ∘ natToZ

A fun & strange thing about Nat n is that it can have at most one inhabitant for any type n. We can synthesize that inhabitant via an alternative definition of the IsNat class defined (twice) above:

class IsNat n where nat ∷ Nat n

instance            IsNat Z     where nat = Zero
instance IsNat n ⇒ IsNat (S n) where nat = Succ nat

Using this latest version of IsNat, we can easily define units (and hence pure on Vec n for IsNat n):

units ∷ IsNat n ⇒ Vec n ()
units = unitsN nat

unitsN ∷ Nat n → Vec n ()
unitsN Zero     = ZVec
unitsN (Succ n) = () :< unitsN n

I prefer this latest IsNat definition over the previous two, because it relies only on Nat, which is simpler and more broadly useful than Vec. Examples abound, including improving an recent post, as we'll see now.

Revisiting type-bounded numbers

The post Type-bounded numbers defined a type BNat n of natural numbers less than n, which can be used, for instance, as numerical digits in base n.

data BNat ∷ * → * where
  BZero ∷          BNat (S n)
  BSucc ∷ BNat n → BNat (S n)

One useful operation is conversion from integer to BNat n. This operation had the awkward task of coming up with BNat structure. The solution given was to introduce a type class, with instances for Z and S:

class HasBNat n where toBNat ∷ Integer → Maybe (BNat n)

instance HasBNat Z where toBNat _ = Nothing

instance HasBNat n ⇒ HasBNat (S n) where
  toBNat m | m < 1     = Just BZero
           | otherwise = fmap BSucc (toBNat (pred m))

We can instead eliminate the HasBNat class and reuse the IsNat class, as in the last technique above for defining units or pure.

toBNat ∷ ∀ n. IsNat n ⇒ Integer → Maybe (BNat n)
toBNat = loop n where
  n = nat ∷ Nat n
  loop ∷ Nat n' → Integer → Maybe (BNat n')
  loop Zero      _ = Nothing
  loop (Succ _)  0 = Just BZero
  loop (Succ n') m = fmap BSucc (loop n' (pred m))

A Monad instance

First the easy parts: standard definitions in terms of pure and join:

instance IsNat n ⇒ Monad (Vec n) where
  return  = pure
  v >>= f = join (fmap f v)

The join function on Vec n is just like join for functions and for streams. (Rightly so, considering the principle of type class morphisms.) It uses diagonalization, and one way to think of vector join is that it extracts the diagonal of a square matrix.

join ∷ Vec n (Vec n a) → Vec n a
join ZVec      = ZVec
join (v :< vs) = headV v :< join (fmap tailV vs)

The headV and tailV functions are like head and tail but understand lengths:

headV ∷ Vec (S n) a → a
headV (a :< _) = a

tailV ∷ Vec (S n) a → Vec n a
tailV (_ :< as) = as

Unlike their list counterparts, headV and tailV are safe, in that the precondition of non-emptiness is verified statically.