Vector.purs

class Nat (a :: Nat) 
  where toInt :: NProxy a → Int

instance natZero :: Nat Zero 
  where toInt _ = 0
instance natSucc :: Nat n ⇒ Nat (Succ n) 
  where toInt _ = 1 + toInt (NProxy :: NProxy n)

newtype Vec (n :: Nat) a = Vec (Array a) 

empty :: ∀ a. Vec Zero a
empty = Vec []

type One = Succ Zero

cons :: ∀ a b c. Add a One b ⇒ c → Vec a c → Vec b c
cons x (Vec xs) = Vec (Array.cons x xs)

infixr 6 cons as +>

add :: ∀ n. Vec n Int → Vec n Int → Vec n Int
add (Vec xs) (Vec ys) = Vec $ Array.zipWith (+) xs ys

dotProduct :: ∀ n. Vec n Int → Vec n Int → Int
dotProduct (Vec xs) (Vec ys) = sum $ Array.zipWith (*) xs ys

test7 = add (1+>3+>(-5)+>empty) (4+>(-2)+>(-1)+>empty)
-- test8 = add empty (4+>(-2)+>(-1)+>empty)

fill :: ∀ a n. Nat n ⇒ (Int → a) → Vec n a
fill f = Vec $ map f $ if x == 0 then [] else 0..(x - 1)
  where x = toInt (NProxy :: NProxy n)
  
zeroVector :: ∀ n. Nat n ⇒ Vec n Int
zeroVector = fill (\_ → 0)

oneVector :: ∀ n. Nat n ⇒ Vec n Int
oneVector = fill (\_ → 1)

newtype Matrix (m :: Nat) (n :: Nat) a = Matrix (Vec m (Vec n a))

instance showVec :: Show a ⇒ Show (Vec n a) where
  show (Vec xs) = "Vec " <> show xs