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?

_______________________________________________
Haskell-Cafe mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/haskell-cafe

Reply via email to