total Data.Map.! function
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?
Hi,
On Wed, Oct 3, 2012 at 7:52 PM, 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? 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?
Perhaps by using a HList in the type of the Map? -- Johan
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
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@joachim-breitner.de | nomeata@debian.org | GPG: 0x4743206C xmpp: nomeata@joachim-breitner.de | http://www.joachim-breitner.de/
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. :-(
participants (4)
-
Heinrich Apfelmus -
Henning Thielemann -
Joachim Breitner -
Johan Tibell