{
  "$type": "site.standard.document",
  "bskyPostRef": {
    "cid": "bafyreiacoygpkekypn6q23spclavgcypiy7z2mjhznrj5gfexx7dqmcsp4",
    "uri": "at://did:plc:pi6woz4d47bkuws673w2il2r/app.bsky.feed.post/3mjrrwictgqu2"
  },
  "path": "/t/lawvere-theories/13944#post_8",
  "publishedAt": "2026-04-18T14:51:26.000Z",
  "site": "https://discourse.haskell.org",
  "tags": [
    "deep-map"
  ],
  "textContent": "I didn’t use type-level naturals, but I did use type-level lists with a `FilterableWithIndex` constraint in my deep-map library. A `DeepMap` is a recursive `Map` indexed by a list of types, with an agglomerating `Semigroup` instead of an overwriting one. In order to\n\n\n    filterWithKeys ::\n      (FilterableWithIndex (Deep (k ': ks)) (DeepMap (k ': ks))) =>\n      (Deep (k ': ks) -> v -> Bool) ->\n      DeepMap (k ': ks) v ->\n      DeepMap (k ': ks) v\n    filterWithKeys = Witherable.ifilter\n\n\nfor all maps with at least one key type (but possibly still empty as maps), I need the induction principle:\n\n\n    -- base case\n    instance FilterableWithIndex (Deep '[k]) (DeepMap '[k]) where\n      imapMaybe f (Wrap m) = Wrap $ Map.mapMaybeWithKey (\\k (Core v) -> Core <$> f (D1 k D0) v) m\n\n    -- recursive case\n    instance\n      (Ord j, FilterableWithIndex (Deep (k ': ks)) (DeepMap (k ': ks))) =>\n      FilterableWithIndex (Deep (j ': k ': ks)) (DeepMap (j ': k ': ks))\n      where\n      imapMaybe f (Wrap m) = Wrap $ Map.mapWithKey (\\k -> Witherable.imapMaybe (f . D1 k)) m\n\n\nIt doesn’t avoid the need to add the constraint to the definition of `filterWithKeys`, but in practice it is trivially satisfied except for `DeepMap '[] v`, which was what we wanted.\n\nMaybe a similar thing with unary representations could work?",
  "title": "Lawvere theories"
}