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

[Henning Thielemann]

Hi Joachim,


On Wed, 5 Oct 2012, Joachim Breitner wrote:

> On Wed, 3 Oct 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 is possible to do this using the same trick that ST is using, 
> i.e. rank 2 types. The problem is that this code is likely to be 
> unwieldy to use, as the variable needs to change with every change to 
> the map – but I guess if you create your map once and then use it in 
> various places without modification, this can actually work.

  Thank you for your detailed answer! I thought about such a tagging method 
but was missing your idea of updating tags of existing keys in order to 
reflect the knowledge about newly added keys.
  Your solution will certainly work for the set of methods you have 
implemented. All of your methods extend the set of keys or preserve it. 
But what about deletion? The certificate that key k is contained in a Map 
must be invalidated by the deletion of k. How could I add this to your 
approach?
  Maybe I should track the operations applied to the keys of a map and 
provide algebraic simplifications, like so:

    insert ::
       Ord k =>
       Tagged s k -> v -> Tagged m (Map k v) ->
       Tagged (Insert s m) (Map k v)

    lookup ::
       Ord k =>
       Tagged s k -> Tagged (Insert s m) (Map k v) -> v

    -- * example simplifications

    commuteInsert ::
       Tagged (Insert s0 (Insert s1 m)) (Map k v) ->
       Tagged (Insert s1 (Insert s0 m)) (Map k v)

    simplifyInsertInsert ::
       Tagged (Insert s (Insert s m)) (Map k v) ->
       Tagged (Insert s m) (Map k v)

    simplifyInsertDelete ::
       Tagged (Insert s (Delete s m)) (Map k v) ->
       Tagged (Insert s m) (Map k v)

    simplifyDeleteInsert ::
       Tagged (Delete s (Insert s m)) (Map k v) ->
       Tagged (Delete s m) (Map k v)


    example =
       lookup k0 $ commuteInsert $
       insert k1 "for" $ insert k0 "bar" m


  I also thought about something like the "exceptions trick". That is, a 
context like

    (ContainsKeyA k, ContainsKeyB k) => Map k x

  might tell that certain keys are in the Map. However, this would not only 
mean that I need a type class for every insertion, it would also not work 
reliably for deletion. If keyA = keyB, then deletion of keyA must also 
remove the ContainsKeyB constraint. :-(