{
  "$type": "site.standard.document",
  "bskyPostRef": {
    "cid": "bafyreih2esgsc2tbx6bmrfwjgzz2by2tmvsgdo6q4prqtvdjs5k4fu55gq",
    "uri": "at://did:plc:pi6woz4d47bkuws673w2il2r/app.bsky.feed.post/3mlr7vf42ujg2"
  },
  "path": "/t/knownnat-indexed-vectors/14099#post_13",
  "publishedAt": "2026-05-13T20:25:00.000Z",
  "site": "https://discourse.haskell.org",
  "tags": [
    "finite-typelits",
    "data-fin",
    "fin-int",
    "fin"
  ],
  "textContent": "mixphix:\n\n> Are there libraries where this kind of vector has been implemented?\n\nThere exist several packages that define a family of finite types indexed by type-level naturals, e.g. finite-typelits, data-fin, fin-int or fin. For each natural number `n`, there is a type `Finite n` that has exactly `n` elements. Then you can define\n\n\n    newtype V n x = V (Finite n -> x)\n\n\nand derive a lot of instances via `Reader (Finite n)`. You certainly want memoization for performance.\n\nBy the way, it is fun to define matrices this way. Conal Elliott gave a talk about this at least once.",
  "title": "KnownNat-indexed vectors"
}