<div dir="ltr">I have some code that I could provide, but I don't seem to see George's email address in the CC (only Tom's). Perhaps GMail ate it for some reason - but either way, I don't know where to send my code :)<div><br></div><div>-- Ollie</div></div><div class="gmail_extra"><br><div class="gmail_quote">On Thu, Feb 19, 2015 at 5:37 PM, Simon Peyton Jones <span dir="ltr"><<a href="mailto:simonpj@microsoft.com" target="_blank">simonpj@microsoft.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<div lang="EN-GB" link="#0563C1" vlink="#954F72">
<div>
<p class="MsoNormal"><span style="font-size:12.0pt">Friends<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:12.0pt">George Karachalas, Tom Schrijvers, Dimitrios Vytiniotis, and I are working on finally cracking the problem of accurately reporting pattern-match overlap and redundancy warnings, in the presence of GADTs.
You know the problem; consider<u></u><u></u></span></p>
<p>vzip :: Vect n a -> Vect n b -> Vect n (a,b)<u></u><u></u></p>
<p>vzip VN VN = VN<u></u><u></u></p>
<p>vzip (VC x xs) (VC y ys) = VC (x,y) (vzip xs ys)<u></u><u></u></p>
<p><u></u> <u></u></p>
<p>data Vect :: Nat -> * -> * where<u></u><u></u></p>
<p> VN :: Vect Zero a<u></u><u></u></p>
<p> VC :: a -> Vect n a -> Vect (Succ n) a<u></u><u></u></p>
<p class="MsoNormal"><span style="font-size:12.0pt">Are there any missing equations in vzip? No! But GHC complains anyway. We have lots of Trac tickets about this; e.g.
<a href="https://ghc.haskell.org/trac/ghc/ticket/3927" target="_blank">https://ghc.haskell.org/trac/ghc/ticket/3927</a>.<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:12.0pt">We now have a draft paper (wait a week) and a prototype implementation, that fixes the problem. But we need your help. We’d like to try our prototype on real code, not just toy examples.<u></u><u></u></span></p>
<p><b><span style="font-size:12.0pt;color:red">So, could you send George a pointer to any packages you have, or know of, that<u></u><u></u></span></b></p>
<p>
<u></u><span style="font-size:12.0pt;font-family:Symbol"><span>·<span style="font:7.0pt "Times New Roman"">
</span></span></span><u></u><b><span style="font-size:12.0pt;color:red">use GADTS (or other fancy type features) and
</span></b><span style="font-size:12.0pt"><u></u><u></u></span></p>
<p>
<u></u><span style="font-size:12.0pt;font-family:Symbol"><span>·<span style="font:7.0pt "Times New Roman"">
</span></span></span><u></u><b><span style="font-size:12.0pt;color:red">would benefit from accurate pattern-match overlap/redundancy warnings?</span></b><span style="font-size:12.0pt;color:red">
</span><span style="font-size:12.0pt"><u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:12.0pt">Specifically:<u></u><u></u></span></p>
<p><u></u><span style="font-size:12.0pt;font-family:Symbol"><span>·<span style="font:7.0pt "Times New Roman"">
</span></span></span><u></u><span style="font-size:12.0pt">Where you have had to add a catch-all<u></u><u></u></span></p>
<p>f _ _ = error “impossible”<u></u><u></u></p>
<p><span style="font-size:12.0pt">to silence GHC from saying “missing patterns”<u></u><u></u></span></p>
<p><u></u><span style="font-size:12.0pt;font-family:Symbol"><span>·<span style="font:7.0pt "Times New Roman"">
</span></span></span><u></u><span style="font-size:12.0pt">Or where you have added
</span><span><span style="font-size:10.0pt">{-# OPTIONS_GHC –fno-warn-missing-patterns #-}</span></span><span style="font-size:12.0pt"> to silence the warnings.<u></u><u></u></span></p>
<p><u></u><span style="font-size:12.0pt;font-family:Symbol"><span>·<span style="font:7.0pt "Times New Roman"">
</span></span></span><u></u><span style="font-size:12.0pt">Or something else like that.<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:12.0pt">George’s email is in cc. <u></u>
<u></u></span></p>
<p class="MsoNormal"><span style="font-size:12.0pt">Time is short – the ICFP deadline is on 27 Feb. So sooner is better than later for us. But later is better than never.<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:12.0pt">Thank you!<span class="HOEnZb"><font color="#888888"><u></u><u></u></font></span></span></p><span class="HOEnZb"><font color="#888888">
<p class="MsoNormal"><span style="font-size:12.0pt">Simon<u></u><u></u></span></p>
</font></span></div>
</div>
<br>_______________________________________________<br>
Haskell-Cafe mailing list<br>
<a href="mailto:Haskell-Cafe@haskell.org">Haskell-Cafe@haskell.org</a><br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe</a><br>
<br></blockquote></div><br></div>