[Haskell-cafe] total Data.Map.! function

[Heinrich Apfelmus]

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.


Best regards,
Heinrich Apfelmus

--
http://apfelmus.nfshost.com