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