Does a package exist with type-indexed containers? i.e. carrying a type-level proof of their size. Something like

```
Map (s :: Nat) k v
insert :: k -> v -> Map s k v -> Map (s + 1) k v
```

Thanks!

Does a package exist with type-indexed containers? i.e. carrying a type-level proof of their size. Something like

```
Map (s :: Nat) k v
insert :: k -> v -> Map s k v -> Map (s + 1) k v
```

Thanks!

1 Like

Your `insert`

might be wrong, if you overwrite a mapping instead of adding one.

I have difficulty imagining a scenario where I need to know the number of mappings that accurately but not what the keys are. With that in mind, you might find the `justified-containers`

package relevant here — it works by providing proofs that keys are present in maps. The technique was expanded and generalised into package `gdp`

, standing for “**G**hosts of **D**eparted **P**roofs”.

8 Likes

There is vector-sized.

For containers with known keys that always contain all their keys, you can think of them as total functions `Key -> a`

, i.e. they’re `Representable`

with your specific key type. You can usually define a specific datatype for that, or sometimes it’s nice to just wrap a newtype around `Finite`

and `Sized.Vector`

and use the `Representable`

instance for `Vector`

(whose key is `Finite`

s of the appropriate size).

5 Likes