Lawvere theories

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

filterWithKeys ::
  (FilterableWithIndex (Deep (k ': ks)) (DeepMap (k ': ks))) =>
  (Deep (k ': ks) -> v -> Bool) ->
  DeepMap (k ': ks) v ->
  DeepMap (k ': ks) v
filterWithKeys = Witherable.ifilter

for all maps with at least one key type (but possibly still empty as maps), I need the induction principle:

-- base case
instance FilterableWithIndex (Deep '[k]) (DeepMap '[k]) where
  imapMaybe f (Wrap m) = Wrap $ Map.mapMaybeWithKey (\k (Core v) -> Core <$> f (D1 k D0) v) m

-- recursive case
instance
  (Ord j, FilterableWithIndex (Deep (k ': ks)) (DeepMap (k ': ks))) =>
  FilterableWithIndex (Deep (j ': k ': ks)) (DeepMap (j ': k ': ks))
  where
  imapMaybe f (Wrap m) = Wrap $ Map.mapWithKey (\k -> Witherable.imapMaybe (f . D1 k)) m

It 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.

Maybe a similar thing with unary representations could work?