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

[Joachim Breitner]

Hi Henning,

Am Mittwoch, den 03.10.2012, 19:52 +0200 schrieb Henning Thielemann:
> 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?

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.

So we need to tag values (maps and keys) with variables. We could use
Edward Kmett’s tagged library, but for now lets just roll our own (full
code in the right order attached):

        newtype Tagged a x = Tag { unTag :: x }
        retag :: Tagged t1 x -> Tagged t2 x
        retag (Tag x) = (Tag x)

The idea is that if you have a "Tagged a (Map k v)" and a "Tagged a k",
where the a’s are the same variable, then you have a guarantee that the
key is in the map. In the code we are writing now we can easily break
that, e.g. using retag, but hopefully not via the functions that we are
going to export in the end.

The lookup function just ensures that the tags agree, if all goes well
the "fromJust" will never fail:

        lookup :: Ord k => Tagged t k -> Tagged t (Map k v) -> v
        lookup (Tag k) (Tag m) = fromJust $ M.lookup k m


We want a function that takes an existing map and tags it. As with most
of the functions that follow, we use continuation passing style with a
rank-2-function to ensure that no assumptions can be made about the tag
variable at all.

        fromMap :: Map k v -> (forall t. Tagged t (Map k v) -> c) -> c
        fromMap m f = (f (Tag m))

The user of this code has no tagged keys of this type yet, so he cannot
use lookup yet. Let’s allow him to add an entry:

        insert :: Ord k =>
            k -> v -> Tagged t1 (Map k v) ->
            (forall t2. Tagged t2 (Map k v) -> Tagged t2 k -> (Tagged t1 k -> Tagged t2 k) -> c) -> 
            c
        insert k v (Tag m) f = f (Tag (M.insert k v m)) (Tag k) retag 

Besides the usual arguments (key, value, map), it takes a continuation.
This receives the updated map with a /new/ tag – after all, our
knowledge about it has changed. We also return the tagged key; this is
the proof  (or the certificate) that the key is in the map that can be
passed to lookup. And finally we pass a function that takes a proof „k
is in the original map“ and turns it into a proof „k is in the update
map“.

We can also allow the programmer to check if a key is present, and
obtain a proof if that is the case:

        check :: Ord k => k -> Tagged t1 (Map k v) ->
            (forall t2. Tagged t2 (Map k v) -> Maybe (Tagged t2 k) -> (Tagged t1 k -> Tagged t2 k) -> c) -> 
            c
        check k (Tag m) f = f (Tag m) (if M.member k m then Just (Tag k) else Nothing) retag

This would be useful when a non-empty map is converted with fromMap. The
type of this function could be varied, e.g. by not creating a new tag at
all if the type is not present.

Finally we need to select the functions that are safe to use for the
export list:
        
        module SafeMap (Tagged, unTag, fromMap, insert, lookup, check)
        
More functions need to be added, e.g. an adjust (which luckily would not
require a continuation-style type).
        

Here is some code that uses the library to implement fromList (it is
nice to see that this is possible given the primitives above):
        
        {-# LANGUAGE Rank2Types #-}
        
        import Data.Map (Map, empty)
        import SafeMap
        
        fromList :: Ord k => [(k,v)] -> (forall t. Tagged t (Map k v) -> [Tagged t k] -> c) -> c
        fromList [] f = fromMap empty $ \m -> f m []
        fromList ((k,v):l) f = fromList l $ \m tks ->
            insert k v m $ \m' tk rt ->
                f m' (tk : map rt tks)

And here is it in use:

        *Main> fromList [(1,1),(2,2)] (curry show)
        "(Tag {unTag = fromList [(1,1),(2,2)]},[Tag {unTag = 1},Tag {unTag = 2}])"

The "map rt" will make this quadratic, as GHC does not detect if you map
an (operationally speaking) identity over a list. Hopefully that will be
fixed eventually: http://hackage.haskell.org/trac/ghc/ticket/2110


Is this anything like what you wanted?

Greetings,
Joachim


-- 
Joachim "nomeata" Breitner
  mail at joachim-breitner.de  |  nomeata at debian.org  |  GPG: 0x4743206C
  xmpp: nomeata at joachim-breitner.de | http://www.joachim-breitner.de/

-------------- next part --------------
A non-text attachment was scrubbed...
Name: SafeMap.hs
Type: text/x-haskell
Size: 1003 bytes
Desc: not available
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20121005/b136f311/attachment.hs>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 198 bytes
Desc: This is a digitally signed message part
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20121005/b136f311/attachment.pgp>