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

[Adam Gundry]

Hi Ollie,


On 02/12/14 10:56, Oliver Charles wrote:
> Adam Gundry <adam at well-typed.com> 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/