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 “Ghosts of Departed Proofs”.
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 Finites of the appropriate size).
5 Likes