Library Reccomendation/Best Practices for length-indexed vectors?

Learn
#1

Length indexed lists aka vectors have been a primary staple for discussion of dependent types in Haskell (and other functional languages) for a while now.

However, I am not sure what is the ‘go-to’ library or implementation people use in practice for something like this?

I would very much like to know which library to use which has a decent balance of efficiency, ergonomics, functionality, type safety.

For context, I have some code like this:

import GHC.TypeLits (Nat)

data Transducer (in :: Nat) (out :: Nat) = Transducer
    { nClocks :: Int
    , inputLabels :: [StateLabel] -- length inputLabels == in
    , stateData :: Map Int (StateData in out)
    }

data StateData = StateData in out
    { transitions :: [Transition]
    , inputConjunct :: [Maybe Bool] -- length inputConjunct == in
    , outputConjunct :: [Bool] -- length outputConjunct == out
    , finalizable :: Bool
    }

I would very much like to be able to replace these lists with length-indexed vectors.

2 Likes
#2

I’ve used vector-sized and liked it?

4 Likes
#3

I second vector-sized, especially when you want GHC type level naturals (which is the easiest for a start) and you are happy about good performance from Vector. If you later need induction over natural numbers, you might want to have a look at vec: Vec: length-indexed (sized) list.

#4

But one can do induction on GHC’s type level natural numbers. Like so:

% ghci
GHCi, version 9.2.7: https://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/kindaro/code/dotfiles/ghci.conf
λ import GHC.TypeLits
λ :set -XUndecidableInstances
λ :set -XAllowAmbiguousTypes
λ class Iterate (n ∷ Nat) where iterate ∷ (α → α) → α → α
> instance Iterate 0 where iterate = flip const
> instance {-# overlappable #-} (Iterate n, m ~ n + 1) ⇒ Iterate m where iterate function = function . iterate @n function
>
λ iterate @3 (+1) 0
3
λ
Leaving GHCi.

% ghci
GHCi, version 9.2.7: https://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/kindaro/code/dotfiles/ghci.conf
λ :set -XUndecidableInstances
λ import GHC.TypeLits
λ type family F (n ∷ Nat) (c ∷ ★ → ★) (x ∷ ★) ∷ ★ where
>   F 0 c x = x
>   F n c x = c (F (n - 1) c x)
>
λ :kind! F 3 Maybe Int
F 3 Maybe Int ∷ ★
= Maybe (Maybe (Maybe Int))
λ
Leaving GHCi.

Maybe you have some other kind of recursion in mind?

#5

Why would I want induction over natural numbers? To prove a theorem?

I have a question about vector-sized. How do you add a list literal in your code? For example, is there a way to hardcode <True, False, True> and have the compiler agree that it should be interpretted as Vec 3 Bool?

#6

I usually use the conversions from tuples.

2 Likes
#7

I’m not sure anymore why I opted or fin and vec for my particular problem, but it might have been these language extensions. (And also overlappable instances.) They may be fine if you think about the code really long, but I couldn’t figure it out, I believe.

I believe already to something like replicate :: a -> Vec n a, which repeats an element a n times where n is only known on the type level, either needs unsafeCoerce or induction in n: You can either build it unsafely by using prelude’s replicate :: Int -> a -> [a], creating an unsized vector, and then unsafely casting to a vector of particular size. Or you can use something like the Iterate type class:

I think there is no straightforward way to use list literals. The IsList type class governs how list literals are interpreted, and it does not allow for a type to depend on the length of the literal. (Maybe one can write a GHC plugin that adds the right type annotations to make it work.)

1 Like