[Haskell-cafe] total Data.Map.! function
apfelmus at quantentunnel.de
Thu Oct 4 18:14:52 CEST 2012
Henning Thielemann wrote:
> I wondered whether there is a brilliant typing technique that makes
> Data.Map.! a total function. That is, is it possible to give (!) a type,
> such that m!k expects a proof that the key k is actually present in the
> dictionary m? How can I provide the proof that k is in m?
> Same question for 'lab' (import Data.Graph.Inductive(lab)). That is,
> can there be a totalLab, with (totalLab gr = fromJust . lab gr) that
> expects a proof that the node Id is actually contained in a graph?
I think it's possible. However, if you are able to track keys in a
meaningful way, you are also able to reify the contents of the map in
the type! At this point, it's no longer clear whether you really want that.
Here's the reason. Consider the expression
map' = insert key value map
The idea is that the type of map' should now indicate that the key
is in the map. Since map does not necessarily contain the key , you
have to add to the type information. But at this point, why not add the
*value* to the type as well? Instead of adding just the key to the
type information, you can add a tuple (key,value) to the type by
virtue of some mild form of parametricity. But at this point, you've put
the whole map into the type.
More information about the Haskell-Cafe