[Haskell-cafe] total Data.Map.! function
johan.tibell at gmail.com
Wed Oct 3 20:17:22 CEST 2012
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?
More information about the Haskell-Cafe