How to specify the type of a vector of fixed size?

Question

I am trying to use Data.Vector.Fixed as the input to a function and am struggling to specify the vector's dimension in the type signature.

For example, I am trying to do something like the following:

acronym :: Vector (Peano 8) String -> String
acronym = foldl1 (++)

and thus specifying the vector's dimension (8) using peano numbers as defined in Data.Vector.Fixed.Cont.

However, attempting to compile this gives kind-mismatch errors:

...:12: error:
    * Expected a type, but
      `Vector (Peano 8) String' has kind
      `Constraint'
    * In the type signature:
        acronym :: Vector (Peano 8) String -> String
   |
61 | acronym :: Vector (Peano 8) String -> String
   |            ^^^^^^^^^^^^^^^^^^^^^^^

...:20: error:
    * Expected kind `* -> *', but `Peano 8' has kind `PeanoNum'
    * In the first argument of `Vector', namely `(Peano 8)'
      In the type signature: acronym :: Vector (Peano 8) String -> String
   |
61 | acronym :: Vector (Peano 8) String -> String

How can I specify a fixed vector's size in a type signature?

Answer 1

You're probably looking for something like:

{-# LANGUAGE DataKinds, FlexibleContexts, GADTs #-}
import qualified Data.Vector.Fixed as V
acronym :: (V.Vector v String, V.Dim v ~ 8) => v String -> String
acronym = V.foldl1 (++)

The type class constraint Vector v String indicates that v is a vector with elements of type String, while the constraint Dim v ~ 8 ensures it has the right size.

It can be used with specific vector types, like boxed or continuation vectors, like so:

import qualified Data.Vector.Fixed.Boxed as BV
import qualified Data.Vector.Fixed.Cont as CV
eight = ["one","two","three","four","five","six","seven","eight"]
main = do
  print $ acronym (V.fromList eight :: BV.Vec 8 String)
  print $ acronym (V.fromList eight :: CV.ContVec 8 String)