How to make fixed-length vectors instance of Applicative?

Question

I recently learned about promotion and decided to try writing vectors.

{-# LANGUAGE DataKinds, GADTs, KindSignatures #-}
module Vector where
  data Nat = Next Nat | Zero
  data Vector :: Nat -> * -> * where
    Construct :: t -> Vector n t -> Vector ('Next n) t
    Empty :: Vector 'Zero t
  instance Functor (Vector n) where
    fmap f a =
      case a of
        Construct x b -> Construct (f x) (fmap f b)
        Empty -> Empty

So far, everything is working. But I ran into a problem when trying to make Vector instance of Applicative.

instance Applicative (Vector n) where
  a <*> b =
    case a of
      Construct f c ->
        case b of
          Construct x d -> Construct (f x) (c <*> d)
      Empty -> Empty
  pure x = _

I had no idea how to do pure. I tried this:

case n of
  Next _ -> Construct x (pure x)
  Zero -> Empty

but got Variable not in scope: n :: Nat error for the first line and Couldn't match type n with 'Zero for the third line of this expression.

So, I used the following hack.

class Applicative' n where
  ap' :: Vector n (t -> u) -> Vector n t -> Vector n u
  pure' :: t -> Vector n t
instance Applicative' n => Applicative' ('Next n) where
  ap' (Construct f a) (Construct x b) = Construct (f x) (ap' a b)
  pure' x = Construct x (pure' x)
instance Applicative' 'Zero where
  ap' Empty Empty = Empty
  pure' _ = Empty
instance Applicative' n => Applicative (Vector n) where
  (<*>) = ap'
  pure = pure'

It gets the job done, but it's not pretty. It introduces a useless class Applicative'. And every time I want to use Applicative for Vector in any function, I have to supply the additional useless constraint Applicative' n which actually holds for any n.

What would be a better, cleaner way of doing this?

Answer 1

This is a (commented) alternative which exploits the singletons package.

Very roughly, Haskell does not let us pattern match on type-level values such as n in the code above. With singletons, we can, at the cost of requiring and providing a few instances of SingI here and there.

{-# LANGUAGE GADTs , KindSignatures, DataKinds, TemplateHaskell, 
             TypeFamilies, ScopedTypeVariables #-}
{-# OPTIONS -Wall #-}

import Data.Singletons.TH

-- Autogenerate singletons for this type
$(singletons [d|
   data Nat = Next Nat | Zero
   |])

-- as before
data Vector :: Nat -> * -> * where
   Construct :: t -> Vector n t -> Vector ('Next n) t
   Empty :: Vector 'Zero t

-- as before
instance Functor (Vector n) where
   fmap _ Empty = Empty
   fmap f (Construct x b) = Construct (f x) (fmap f b)        

-- We now require n to carry its own SingI instance.
-- This allows us to pattern match on n.
instance SingI n => Applicative (Vector n) where
   Empty <*> Empty = Empty
   -- Here, we need to access the singleton on n, so that later on we
   -- can provide the SingI (n-1) instance we need for the recursive call.
   -- The withSingI allows us to use m :: SNat (n-1) to provide the instance.
   (Construct f c) <*> (Construct x d) = case sing :: SNat n of
      SNext m -> withSingI m $ Construct (f x) (c <*> d)

   -- Here, we can finally pattern match on n.
   -- As above, we need to provide the instance with withSingI
   -- to the recursive call.
   pure x = case sing :: SNat n of
      SZero -> Empty
      SNext m -> withSingI m $ Construct x (pure x)

Using this will require to provide a SingI n instance at every use, which is a bit inconvenient, but not too much (IMO). The sad part is that <*> does not really need SingI n, since, in principle, it could recompute that from the two vectors at hand. However, pure has no input vector, so it can only pattern match with a provided singleton.

As another alternative, similar to the original code, one could write

instance Applicative (Vector Zero) where
   ...
instance Applicative (Vector n) => Applicative (Vector (Next n)) where
   ...

This is not completely equivalent, and will require to add contexts Applicative (Vector n) => in all the functions later on where n is unknown, but could be enough for many purposes.

Answer 2

You could make same directly:

instance Applicative (Vector Zero) where
  a <*> b = Empty
  pure x = Empty

instance Applicative (Vector n) => Applicative (Vector (Next n)) where
  a <*> b = 
    case a of
      Construct f c ->
        case b of
          Construct x d -> Construct (f x) (c <*> d)
  pure x = Construct x (pure x)

As I can reason about it: for different types of the class, the code should be type-aware. If you had several instances, different types would get different implementation, and it would be easily resolved. But, if you try to make it with single non-recursive instance, there is basically no information about the type in runtime, and code which is always the same still needs to decide which type to handle. When you have input parameters, you can exploit GADTs to provide you the type information. But for pure there are no input parameters. So you have to have some context for the Applicative instance.

Answer 3

Consider this an addendum to @chi's answer to provide additional explanation of the singleton approach...

I would suggest reading the Hasochism paper if you haven't already done so. In particular, in section 3.1 of that paper, they deal with exactly this problem, and use it as the motivating example for when implicit singleton parameters (the SingI of @chi's answer, and the NATTY type class in the Hasochism paper) are necessary, rather than merely convenient.

As it applies to your code, the main issue is that pure needs a run-time representation of the length of the vector that it's supposed to be generating, and the type-level variable n doesn't fit the bill. The solution is to introduce a new GADT, a "singleton" that provides runtime values that correspond directly to the promoted types Next and Zero:

data Natty (n :: Nat) where
  ZeroTy :: Natty Zero
  NextTy :: Natty n -> Natty (Next n)

I tried to use roughly the same naming convention as the paper: Natty is the same, and ZeroTy and NextTy correspond to the paper's Zy and Sy.

By itself, this explicit singleton is useful. For example, see the definition of vchop in the paper. Also, we can easily write a variant of pure that takes the explicit singleton to do its job:

vcopies :: Natty n -> a -> Vector n a
vcopies ZeroTy _ = Empty
vcopies (NextTy n) x = Construct x (vcopies n x)

We can't yet use this to define pure, though, because pure's signature is determined by the Applicative type class, and we have no way to squeeze the explicit singleton Natty n in there.

The solution is to introduce implicit singletons, which allow us to retrieve an explicit singleton whenever needed through the natty function in the context of the following type class:

class NATTY n where
  natty :: Natty n
instance NATTY Zero where
  natty = ZeroTy
instance NATTY n => NATTY (Next n) where
  natty = NextTy natty

Now, provided we're in a NATTY n context, we can call vcopies natty to supply vcopies with its explicit natty parameter, which allows us to write:

instance NATTY n => Applicative (Vector n) where
  (<*>) = vapp
  pure = vcopies natty

using the definitions of vcopies and natty above, and the definition of vapp below:

vapp :: Vector n (a -> b) -> Vector n a -> Vector n b
vapp Empty Empty = Empty
vapp (Construct f c) (Construct x d) = Construct (f x) (vapp c d)

Note one oddity. We needed to introduce this vapp helper function for an obscure reason. The following instance without NATTY matches your case-based definition and type-checks fine:

instance Applicative (Vector n) where
  Empty <*> Empty = Empty
  Construct f c <*> Construct x d = Construct (f x) (c <*> d)
  pure = error "Argh!  No NATTY!"

If we add the NATTY constraint to define pure:

instance NATTY n => Applicative (Vector n) where
  Empty <*> Empty = Empty
  Construct f c <*> Construct x d = Construct (f x) (c <*> d)
  pure = vcopies natty

the definition of (<*>) doesn't type check any more. The problem is that the NATTY n constraint on the left-hand side of the second (<*>) case doesn't automatically imply a NATTY n1 constraint on the right-hand side (where Next n ~ n1), so GHC doesn't want to allow us to call (<*>) on the right-hand side. In this case, because the constraint isn't actually needed after it's used for the first time, a helper function without a NATTY constraint, namely vapp, works around the problem.

@chi uses case matching on natty and the helper function withSingI as an alternative workaround. The equivalent code here would use a helper function that turns an explicit singleton into an implicit NATTY context:

withNATTY :: Natty n -> (NATTY n => a) -> a
withNATTY ZeroTy a = a
withNATTY (NextTy n) a = withNATTY n a

allowing us to write:

instance NATTY n => Applicative (Vector n) where
  Empty <*> Empty = Empty
  Construct f c <*> Construct x d = case (natty :: Natty n) of
    NextTy n -> withNATTY n $ Construct (f x) (c <*> d)
  pure x = case (natty :: Natty n) of
    ZeroTy -> Empty
    NextTy n -> Construct x (withNATTY n $ pure x)

This would need both ScopedTypeVariables and RankNTypes.

Anyway, sticking with the helper functions, the complete program looks like this:

{-# LANGUAGE DataKinds, GADTs, KindSignatures #-}

module Vector where

data Nat = Next Nat | Zero
data Vector :: Nat -> * -> * where
  Construct :: t -> Vector n t -> Vector ('Next n) t
  Empty :: Vector 'Zero t

data Natty (n :: Nat) where
  ZeroTy :: Natty Zero
  NextTy :: Natty n -> Natty (Next n)

class NATTY n where
  natty :: Natty n
instance NATTY Zero where
  natty = ZeroTy
instance NATTY n => NATTY (Next n) where
  natty = NextTy natty

instance Functor (Vector n) where
  fmap f a =
    case a of
      Construct x b -> Construct (f x) (fmap f b)
      Empty -> Empty

instance NATTY n => Applicative (Vector n) where
  (<*>) = vapp
  pure = vcopies natty

vapp :: Vector n (a -> b) -> Vector n a -> Vector n b
vapp Empty Empty = Empty
vapp (Construct f c) (Construct x d) = Construct (f x) (vapp c d)

vcopies :: Natty n -> a -> Vector n a
vcopies ZeroTy _ = Empty
vcopies (NextTy n) x = Construct x (vcopies n x)

The correspondence with the singletons library is that:

$(singletons [d|
  data Nat = Next Nat | Zero
  |])

automatically generates the singletons (with constructors SZero and SNat instead of ZeroTy and NatTy; and with type SNat instead of Natty) and the implicit singleton class (called SingI instead of NATTY and using the function sing instead of natty), giving the complete program:

{-# LANGUAGE DataKinds, GADTs, KindSignatures, TemplateHaskell, TypeFamilies #-}

module Vector where

import Data.Singletons
import Data.Singletons.TH

$(singletons [d|
  data Nat = Next Nat | Zero
  |])

data Vector :: Nat -> * -> * where
  Construct :: t -> Vector n t -> Vector ('Next n) t
  Empty :: Vector 'Zero t

instance Functor (Vector n) where
  fmap f a =
    case a of
      Construct x b -> Construct (f x) (fmap f b)
      Empty -> Empty

instance SingI n => Applicative (Vector n) where
  (<*>) = vapp
  pure = vcopies sing

vapp :: Vector n (a -> b) -> Vector n a -> Vector n b
vapp Empty Empty = Empty
vapp (Construct f c) (Construct x d) = Construct (f x) (vapp c d)

vcopies :: SNat n -> a -> Vector n a
vcopies SZero _ = Empty
vcopies (SNext n) x = Construct x (vcopies n x)

For more on what the singletons library does and how it's built, I'd suggest reading Introduction to Singletons.

Answer 4

Several other answers have introduced a Natty or SNat type to implement pure. Indeed, having such a type greatly reduces the need for one-off type classes. A potential downside of the traditional Natty/SNat GADT, however, is that your program will actually build the representation and then use it, even if the Nat is known at compile time. This generally wouldn't happen with the auxiliary-class approach. You can get around this by using a different representation.

I'm going to use these names:

data Nat = Z | S Nat

Suppose we define the usual

data Natty n where
  Zy :: Natty 'Z
  Sy :: Natty n -> Natty ('S n)

We can write its eliminator (induction principle) thus:

natty :: p 'Z -> (forall k. p k -> p ('S k)) -> Natty n -> p n
natty z _ Zy = z
natty z s (Sy n) = s (natty z s n)

For our purpose, we don't really need the Natty; we only need its induction principle! So let's define another version. I imagine there's a proper name for this encoding, but I have no idea what it might be.

newtype NatC n = NatC
  { unNatC :: forall p.
              p 'Z  -- base case
           -> (forall k. p k -> p ('S k))  -- inductive step
           -> p n }

This is isomorphic to Natty:

nattyToNatC :: Natty n -> NatC n
nattyToNatC n = NatC (\z s -> natty z s n)

natCToNatty :: NatC n -> Natty n
natCToNatty (NatC f) = f Zy Sy

Now we can write a class for Nats we know how to eliminate:

class KnownC n where
  knownC :: NatC n
instance KnownC 'Z where
  knownC = NatC $ \z _ -> z
instance KnownC n => KnownC ('S n) where
  knownC = NatC $ \z s -> s $ unNatC knownC z s

Now here's a vector type (I've renamed things to match my own taste):

infixr 4 :<
data Vec :: Nat -> * -> * where
  (:<) :: t -> Vec n t -> Vec ('S n) t
  Nil :: Vec 'Z t

Because Vec's length parameter isn't its last one, we'll have to flip it to use with NatC:

newtype Flip f a n = {unFlip :: f n a}

induct2 :: f 'Z a
         -> (forall k. f k a -> f ('S k) a)
         -> NatC n -> f n a
induct2 z s n = unFlip $ unNatC n (Flip z) (\(Flip r) -> Flip (s r))

replC :: NatC n -> a -> Vec n a
replC n a = induct2 Nil (a :<) n

instance KnownC n => Applicative (Vec n) where
   pure = replC knownC
   (<*>) = ...

Now if the vector length is known at compile time, the pure vector will be built directly, with no intermediate structure needed.