Henning Thielemann | 3 Oct 19:52 2012
Picon

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?
Johan Tibell | 3 Oct 20:17 2012
Picon

Re: total Data.Map.! function

Hi,

On Wed, Oct 3, 2012 at 7:52 PM, Henning Thielemann
<lemming <at> henning-thielemann.de> 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?

Perhaps by using a HList in the type of the Map?

-- Johan
Heinrich Apfelmus | 4 Oct 18:14 2012
Picon

Re: total Data.Map.! function

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

--
(Continue reading)

Joachim Breitner | 5 Oct 10:53 2012
Picon

Re: total Data.Map.! function

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:
(Continue reading)

Henning Thielemann | 9 Oct 22:40 2012
Picon

Re: total Data.Map.! function


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 
(Continue reading)


Gmane