Haskell :: How do I create a Vector of arbitrary length?

Question

Wanted to implement type safe matrix multiplication in Haskell. Defined the following:

{-# LANGUAGE TypeFamilies, DataKinds, GADTs  #-}
module Vector where

data Nat = Succ Nat | Zero

data Vector (n :: Nat) a where
    Nil :: Vector 'Zero a
    (:::) :: a -> Vector n a -> Vector (Succ n) a
type Matrix n m a = Vector m (Vector n a)

instance Foldable (Vector n) where
    foldr f b (a ::: as) = f a (foldr f b as)
    foldr _ b Nil = b

instance Functor (Vector n) where
    fmap f (x ::: xs) = f x ::: fmap f xs
    fmap _ Nil = Nil

zipV :: (a -> b -> c) -> Vector n a -> Vector n b -> Vector n c
zipV f (a ::: as) (b ::: bs) = f a b ::: zipV f as bs
zipV f Nil Nil = Nil

Eventually had the need to implement

transpose :: Matrix n m a -> Matrix m n a

but the best I could do in Haskell was:

transpose :: Matrix n (Succ m) a -> Matrix (Succ m) n a
transpose (h ::: rest@(_ ::: _)) = zipV (:::) h (transpose rest)
transpose (h ::: Nil) = fmap (::: Nil) h

which is limited to m > 0 because I couldn't implement

nils :: {n :: Nat} -> Vector n (Vector Zero a)

Switched to Idris just to practice and did much better job:

matrix : Nat -> Nat -> Type -> Type
matrix n m a = Vector n (Vector m a)

nils : {n: Nat} -> Vector n (Vector Z a)
nils {n = Z}   = Nil
nils {n = S k} = Nil ::: nils

transpose : matrix n m a -> matrix m n a
transpose (h ::: rest) = zipV (:::) h (transpose rest)
transpose Nil = nils

I have the urge to implement nils, but type level programming in Haskell is very awkward. I also had to patternmatch on rest@(_ ::: _) in Haskell, but I hadn't in Idris. How can I implement "nils"?

Featherston

I don't think this is feasible. In Haskell, types are erased, so the only way to recover n from a Vector n t is to patter match some value of such vector type. That's a problem when you only have a value of type Vector 0 (Vector n t). One way to fix this is to store a singleton inside the matrix type, something like Matrix n m a = (Sing n, Vector m (Vector n a)). Otherwise, require the singleton as an argument in transpose. – Petulance

Answer 1

This is essentially what singletons are there for. That's a value-level witness for a typeclass that gives you access to this (conceptually reduntant) information that every number can in fact be described in the standard form. A minimal implementation:

data NatSing n where
  ZeroSing :: NatSing Zero
  SuccSing :: KnownNat n => NatSing (Succ n)

class KnownNat n where
  natSing :: NatSing n
instance KnownNat Zero where natSing = ZeroSing
instance KnownNat n => KnownNat (Succ n) where natSing = SuccSing

And now it's possible to write

{-# LANGUAGE ScopedTypeVariables, UnicodeSyntax, TypeApplications #-}
nils :: ∀ n a . KnownNat n => Vector n (Vector Zero a)
nils = case natSing @n of
  ZeroSing ->     Nil
  SuccSing -> Nil ::: nils

Echolalia