<div dir="ltr"><div class="gmail_extra"><div class="gmail_quote">On Mon, Dec 12, 2016 at 1:31 PM, David Feuer <span dir="ltr"><<a href="mailto:david.feuer@gmail.com" target="_blank">david.feuer@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="auto"><span class=""><div><div class="gmail_extra"><div class="gmail_quote">On Dec 12, 2016 1:15 PM, "Edward Kmett" <<a href="mailto:ekmett@gmail.com" target="_blank">ekmett@gmail.com</a>> wrote:<br type="attribution"><blockquote class="m_6514440456076263841quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr">A few thoughts in no particular order:<br><br>Unlike this proposal, the existing 'reify' itself as core can actually be made well typed.<br></div></blockquote></div></div></div><div dir="auto"><br></div></span><div dir="auto">Can you explain this?</div></div></blockquote><div><br></div><div>I mean just that. If you look at the core generated by the existing 'reify' combinator, nothing it does is 'evil'. We're allowing it to construct a dictionary. That isn't unsound where core is concerned.</div><div><br></div><div>Where the surface language is concerned the uniqueness of that dictionary is preserved by the quantifier introducing a new type generatively in the local context, so the usual problems with dictionary construction are defused.</div><div><br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="auto"><span class=""><div dir="auto"><div class="gmail_extra"><div class="gmail_quote"><blockquote class="m_6514440456076263841quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr">Tagged in the example could be replaced with explicit type application if backwards compatibility isn't a concern. OTOH, it is.<br></div></blockquote></div></div></div><div dir="auto"><br></div></span><div dir="auto">Would that help Core typing?</div></div></blockquote><div><br></div><div>It doesn't make a difference there. The only thing is it avoids needing to make up something like Tagged. </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="auto"><span class=""><div dir="auto"><br></div><div dir="auto"><div class="gmail_extra"><div class="gmail_quote"><blockquote class="m_6514440456076263841quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div> On the other other hand, if you're going to be magic, you might as well go all the way to something like:</div><div><br><span style="font-size:12.8px">reify# :: (p => r) -> a -> r<br></span></div></div></blockquote></div></div></div><div dir="auto"><br></div></span><div dir="auto">How would we implement reify in terms of this variant?</div></div></blockquote><div><br></div><div>That I don't have the answer to. It seems like it should work though. </div><div><br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="auto"><span class=""><div dir="auto"><div class="gmail_extra"><div class="gmail_quote"><blockquote class="m_6514440456076263841quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div>and admit both fundep and TF forms. I mean, if you're going to lie you might as well lie big.</div></div></blockquote></div></div></div><div dir="auto"><br></div></span><div dir="auto">Definitely.</div></div></blockquote><div> </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="auto"><span class=""><div dir="auto"><div class="gmail_extra"><div class="gmail_quote"><blockquote class="m_6514440456076263841quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div>There are a very large number of instances out there scattered across dozens of packages that would be broken by switching from Proxy to Tagged or explicit type application internally. (I realize that this is a lesser concern that can be resolved by a major version bump and some community friction, but it does mean pragmatically that migrating to something like this would need a plan.)</div></div></blockquote></div></div></div><div dir="auto"><br></div></span><div dir="auto">I just want to make sure that we do what we need to get Really Good Code, if we're going to the trouble of adding compiler support.</div></div>
</blockquote></div></div><div class="gmail_extra"><br></div><div class="gmail_extra">That makes sense to me.</div><div class="gmail_extra"><br></div><div class="gmail_extra">-Edward</div></div>