<div dir="ltr"><div class="gmail_extra"><div class="gmail_quote">On Mon, Oct 21, 2013 at 6:52 PM, Gábor Lehel <span dir="ltr"><<a href="mailto:illissius@gmail.com" target="_blank">illissius@gmail.com</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><br><div class="gmail_extra"><div class="gmail_quote"><div class="im">On Mon, Oct 21, 2013 at 3:42 PM, Richard Eisenberg <span dir="ltr"><<a href="mailto:eir@cis.upenn.edu" target="_blank">eir@cis.upenn.edu</a>></span> wrote:<br>


<blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div style="word-wrap:break-word"><br><div><div class="gmail_extra"><div>On Oct 21, 2013, at 6:06 AM, Gábor Lehel <<a href="mailto:illissius@gmail.com" target="_blank">illissius@gmail.com</a>> wrote:</div>
<br><div class="gmail_quote">On Mon, Oct 21, 2013 at 6:04 AM, Richard Eisenberg <span dir="ltr"><<a href="mailto:eir@cis.upenn.edu" target="_blank">eir@cis.upenn.edu</a>></span> wrote:<br>

<blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
<div style="word-wrap:break-word">- There is a new function (in Data.Type.Equality) gcastWith :: (a :~: b) -> ((a ~ b) => r) -> r. Type inference for this function works well.</div></blockquote><div><br>
</div><div>In my experience, for partial application it's convenient to have the arguments the other way around.<br></div></div></div><div><div><br></div></div><div>I'd be worried about type inference with partial application and reversed parameters. The values of a and b can only be gleaned from the equality witness, so I would think that delaying that parameter would cause some havoc. Is that not what you've seen?</div>


</div></div></blockquote><div><br></div></div><div>I haven't used it in super-complicated scenarios. But basically, when I have used it, no. If it's used for a top-level definition, it will have a type signature and the types will be known from there, and if it's part of a larger expression just shuffled around for convenience, the equality witness will presumably be in there somewhere.<br>


<br></div><div>For example, you could define the three combinators from above as partial applications:<div class="im"><br><br>inner :: (f a :~: g b) -> (a :~: b)<br></div></div><div>inner = gcastWith Refl<div class="im">
<br>outer :: (f a :~: g b) -> (f :~: g)<br>

</div></div><div>outer = gcastWith Refl<div class="im"><br>apply :: (f :~: g) -> (a :~: b) -> (f a :~: g b)<br></div></div><div>apply = gcastWith (gcastWith Refl)<br><br></div><div>I'm not implying these are better in any way than just e.g. `inner Refl = Refl`, but it's the kind of thing you can write which is much more annoying if the arguments are in the reverse order.</div>
</div></div></div></blockquote></div><br></div><div class="gmail_extra">Just want to add that this is analogous to the `maybe`, `either`, `uncurry` etc. functions for their respective types, so most of the same motivations apply.<br>
<br>-- <br>Your ship was destroyed in a monadic eruption.
</div></div>