{
  "$type": "site.standard.document",
  "bskyPostRef": {
    "cid": "bafyreiefrjycudutxq34gqi5cbks52x6ewt7aurc275nczieuwaqyv6yby",
    "uri": "at://did:plc:pi6woz4d47bkuws673w2il2r/app.bsky.feed.post/3mlqsgofvkww2"
  },
  "path": "/t/knownnat-indexed-vectors/14099#post_1",
  "publishedAt": "2026-05-13T16:15:02.000Z",
  "site": "https://discourse.haskell.org",
  "tags": [
    "Ray Tracing in One Weekend",
    "@n",
    "@m",
    "@p",
    "@q"
  ],
  "textContent": "The way sized vectors are usually implemented in Haskell is with a `data` declaration, typically involving several fields of the same type, for example:\n\n\n    data V3 x = V3 !x !x !x deriving ({- ... -})\n\n\nThis representation has the obvious benefits of automatic deriving for many classes, but working with arbitrary sizes is rather difficult. So I’ve been toying with another approach: using a function type!\n\n\n    {-# LANGUAGE BlockArguments #-}\n    {-# LANGUAGE LambdaCase #-}\n\n    newtype V n x = V {unV :: Natural -> x} deriving (Functor)\n\n\nThis particular formulation doesn’t allow for automatic deriving of `Eq`, `Ord`, `Foldable` or `Traversable`, but with a few helper functions they are easily expressed by hand:\n\n\n    dimensions :: forall n. (KnownNat n) => Proxy n -> [Natural]\n    dimensions Proxy = case natVal (Proxy @n) of\n      0 -> []\n      n -> [0 .. pred n]\n\n    (!) :: V n x -> Natural -> x\n    V f ! x = f x\n\n    instance (KnownNat n, Eq x) => Eq (V n x) where\n      (==) :: V n x -> V n x -> Bool\n      v == w = List.all (\\i -> v ! i == w ! i) (dimensions (Proxy @n))\n\n    instance (KnownNat n, Ord x) => Ord (V n x) where\n      compare :: V n x -> V n x -> Ordering\n      compare v w = foldMap (\\i -> compare (v ! i) (w ! i)) (dimensions (Proxy @n))\n\n    instance (KnownNat n) => Foldable (V n) where\n      foldMap :: (Monoid m) => (a -> m) -> V n a -> m\n      foldMap f (V x) = foldMap (f . x) (dimensions (Proxy @n))\n\n    instance (KnownNat n) => Traversable (V n) where\n      traverse :: (Applicative f) => (a -> f b) -> V n a -> f (V n b)\n      traverse f (V x) =\n        traverse (f . x) (dimensions (Proxy @n)) <&> \\xs ->\n          V \\i -> xs List.!! fromIntegral i\n\n\nThe `Traversable` instance is perhaps unfortunate, since we must keep a reference to the list `xs` to determine the values of the resulting vector, but I haven’t heavily used the `Traversable` instance yet in my experiments, so I can’t muse on its performance.\n\nThe `Applicative` instance is also straightforward, and `(<*>)` in particular gives me peace:\n\n\n    instance (KnownNat n) => Applicative (V n) where\n      pure :: x -> V n x\n      pure x = V (const x)\n\n      (<*>) :: V n (x -> y) -> V n x -> V n y\n      V f <*> V x = V (f <*> x)\n\n\nOf course, it’s tedious to write case expressions each time you want to define a vector, but the pattern is easily extractable:\n\n\n    v2 :: forall x. x -> x -> V 2 x\n    v2 x y = V \\case\n      0 -> x\n      _ -> y\n\n    withV2 :: (x -> x -> y) -> V 2 x -> y\n    withV2 f v = f (v ! 0) (v ! 1)\n\n    v3 :: forall x. x -> x -> x -> V 3 x\n    v3 x y z = V \\case\n      0 -> x\n      1 -> y\n      _ -> z\n\n    withV3 :: (x -> x -> x -> y) -> V 3 x -> y\n    withV3 f v = f (v ! 0) (v ! 1) (v ! 2)\n\n    v4 :: forall x. x -> x -> x -> x -> V 4 x\n    v4 x y z w = V \\case\n      0 -> x\n      1 -> y\n      2 -> z\n      _ -> w\n\n    withV4 :: (x -> x -> x -> x -> y) -> V 4 x -> y\n    withV4 f v = f (v ! 0) (v ! 1) (v ! 2) (v ! 3)\n\n\nThis formulation also extends to matrices:\n\n\n    newtype M m n x = M {unM :: V m (V n x)} deriving (Functor)\n\n    m22 :: forall x. x -> x -> x -> x -> M 2 2 x\n    m22 a b c d = M $ V \\i -> V \\j -> case (i, j) of\n      (0, 0) -> a\n      (0, 1) -> b\n      (1, 0) -> c\n      _ -> d\n\n    {- m33, etc... -}\n\n    row :: V n x -> M 1 n x\n    row x = M $ V (const x)\n\n    column :: V m x -> M m 1 x\n    column x = M $ V \\i -> V (const (x ! i))\n\n\nIn this case the instances map/fold/traverse over both of the `dimensions`, `@m` and `@n`. What’s more, the Kronecker product is super easy to exhibit:\n\n\n    kronecker ::\n      forall m n p q x.\n      (KnownNat p, KnownNat q, Num x) =>\n      M m n x -> M p q x -> M (m * p) (n * q) x\n    kronecker (M a) (M b) = M $ V \\i -> V \\j ->\n      let p = natVal (Proxy @p)\n          q = natVal (Proxy @q)\n          (ia, ib) = quotRem i p\n          (ja, jb) = quotRem j q\n       in a ! ia ! ja * b ! ib ! jb\n\n\nAre there libraries where this kind of vector has been implemented? So far I’ve used this technique in my own attempt at Ray Tracing in One Weekend with much success, though I haven’t compared it to `data` libraries like `linear` in terms of performance.",
  "title": "KnownNat-indexed vectors"
}