<div dir="ltr">On Tue, Jan 13, 2015 at 12:39 PM, Nicholls, Mark <span dir="ltr"><<a href="mailto:nicholls.mark@vimn.com" target="_blank">nicholls.mark@vimn.com</a>></span> wrote:<br><div class="gmail_extra"><div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">





<div link="blue" vlink="purple" lang="EN-GB">
<div><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d"></span>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d">But….<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d"><u></u> <u></u></span></p>
<p><u></u><span style="font-size:11.0pt;font-family:Wingdings;color:#1f497d"><span>Ø<span style="font:7.0pt "Times New Roman""> 
</span></span></span><u></u><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d">-- | Generalized form of type-safe cast using propositional equality<u></u><u></u></span></p>
<p><u></u><span style="font-size:11.0pt;font-family:Wingdings;color:#1f497d"><span>Ø<span style="font:7.0pt "Times New Roman""> 
</span></span></span><u></u><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d">gcastWith :: (a :~: b) -> ((a ~ b) => r) -> r<u></u><u></u></span></p>
<p><u></u><span style="font-size:11.0pt;font-family:Wingdings;color:#1f497d"><span>Ø<span style="font:7.0pt "Times New Roman""> 
</span></span></span><u></u><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d">gcastWith Refl x = x<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d"><u></u> <u></u></span></p>
<div>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d">I don’t even understand the signature<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d"><u></u> <u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d">What does “~” mean…(it’s something that comes out in error messages when my types are all messed up)….and then there’s a “=>” going on…in the middle of a signature….I
 know “=>” in the context of “Num a => a -> a -> a”</span></p></div></div></div></blockquote><div><br></div><div>a ~ b is a constraint that a and b are exactly the same type. For example, Int ~ Int is satisfiable, but Int ~ Bool is not. So what gcastWith does is take a witness that a and b are the same type (witnessed by the a :~: b value), and then lets you form a value using that evidence.<br><br><br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div link="blue" vlink="purple" lang="EN-GB"><div><div><p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d"><u></u><u></u></span></p>

<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d">What would a value of type “((a ~ b) => r)” look like?<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d"><u></u></span></p></div></div></div></blockquote><div><br></div><div>I can't come up with a workable example right now, but I could imagine that you might have:<br><br></div><div>   reverseReverse :: a :~: (Reverse (Reverse a))<br><br></div><div>Then if you have something that needs to work on a Reverse (Reverse a) value, but you only have a 'a' around, you can show GHC that it doesn't matter - because they are the same type:<br><br></div><div>  gcastWith reverseReverse :: (a ~ Reverse (Reverse a) => r) -> r<br><br></div><div>Presumably whatever 'r' is will refer to 'a' and do something with it (maybe mapping over a list or something).<br><br></div><div>Sorry that this is all fairly vague, but hopefully that gives you some leads.<br><br></div><div>-- ocharles<br></div></div><br></div></div>