{
  "$type": "site.standard.document",
  "bskyPostRef": {
    "cid": "bafyreifkuuacjr3wlpbj4c33r4qrmt5tcxucwoseub65v3fzi2mnel5nwa",
    "uri": "at://did:plc:pi6woz4d47bkuws673w2il2r/app.bsky.feed.post/3mlw2jahh7p22"
  },
  "path": "/t/knownnat-indexed-vectors/14099?page=2#post_27",
  "publishedAt": "2026-05-15T17:39:02.000Z",
  "site": "https://discourse.haskell.org",
  "tags": [
    "fixed-vector"
  ],
  "textContent": "There’s also approach from fixed-vector. It works with Church-encoded products. For example ordinary haskell data type\n\n\n    data V2 a = V2 a a\n\n\nis isomorphic to:\n\n\n    newtype Church2 a = Church2 (forall r. (a -> a -> r) -> r)\n\n    inspect :: V2 a -> Church2 a\n    inspect (V2 x y) = Church2 $ \\f -> f x y\n\n    construct :: Church2 a -> V2 a\n    construct (Church2 f) = f V2\n\n\nnext trick is notice that it’s possible to define N-dimensional Church vectors inductively. But one has to define standard Peano numerals since type level naturals don’t support induction.\n\n\n    data Nat = Z | S Nat\n\n    type family Fn n a b where\n      Fn  Z    a b = b\n      Fn (S n) a b = a -> Fn n a b\n\n    newtype Fun n a b = Fun (Fn n a b)\n\n    newtype Church n a = Church (forall r. Fun n a r -> r)\n\n\nThen it’s possible to define all operations on Church encoded vectors. And single missing piece is to define type class that establish isomorphism between Church encoding and whatever representation one wants to use. Naturally this approach only works with small vectors.\n\nIt is possible to define vector that are generic in length.",
  "title": "KnownNat-indexed vectors"
}