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

2012-10-09 Thread Henning Thielemann
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

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

2012-10-05 Thread 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

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

2012-10-04 Thread Heinrich Apfelmus
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

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

2012-10-03 Thread 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

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

2012-10-03 Thread Johan Tibell
Hi, On Wed, Oct 3, 2012 at 7:52 PM, Henning Thielemann lemm...@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