Re: [Haskell-cafe] Use distributivity proof in a simple example

Hi Ollie, On 02/12/14 10:56, Oliver Charles wrote:

Adam Gundry writes:

...

-- Now it's easy to define wrap wrap :: DF xs -> DF (Map [] xs) wrap Empty = Empty wrap (Single a) = Single [ a ] wrap (Cons x y) = case mapDist (toSingleton x) y of Refl -> Cons (wrap x) (wrap y)

Am I right in thinking that you can also use

case unsafeCoerce Refl `asTypeOf` mapDist (toSingleton x) of ..

to get the same proof, but without any runtime cost? It seems like this might be a nice middle ground. Of course there is a risk that the proof is just wrong, in which case things could awry. Maybe another option is to switch that line with -XCPP macros depending on whether or not you're in "production" mode.

Well, yes, but it rather depends what you mean by "the same proof". Certainly you can write unsafeCoerce, save some CPU cycles and nothing bad will happen in this case, because mapDist is total. There's nothing to enforce that, however. This is where having a totality checker (like in Agda or Idris) really helps: the compiler can safely erase known-total proof terms. In Haskell, I can write down the "proof" bad :: a :~: b bad = bad which will lead to a safe infinite loop if evaluated, but if I'm just blindly trusting it using unsafeCoerce, it will give me... well, unsafeCoerce. I can certainly understand the temptation to write proof terms in development and replace them with unsafeCoerce in production, though. You just need a good test suite. ;-) Happy Advent, Adam -- Adam Gundry, Haskell Consultant Well-Typed LLP, http://www.well-typed.com/