<div dir="ltr">to better clarify what i'm referrring to i shall link to <div><a href="http://agda.readthedocs.org/en/latest/language/reflection.html">http://agda.readthedocs.org/en/latest/language/reflection.html</a><br></div><div>which describes the agda reflection / type checking monad and associated quote/unquote facilitie further</div></div><div class="gmail_extra"><br><div class="gmail_quote">On Mon, Apr 18, 2016 at 2:50 PM, Thomas Bereknyei <span dir="ltr"><<a href="mailto:tomberek@gmail.com" target="_blank">tomberek@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">I'm not clear what the tradeoffs would be in the case that prompted this thread, but I have been in situations where I wanted a richer ecosystem around Typed TH. Access to Q effects are definitely part of that.<br></div><div class="HOEnZb"><div class="h5"><div class="gmail_extra"><br><div class="gmail_quote">On Mon, Apr 18, 2016 at 2:49 PM, Carter Schonwald <span dir="ltr"><<a href="mailto:carter.schonwald@gmail.com" target="_blank">carter.schonwald@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><p dir="ltr">This thread is reminding me of the metaprograming ux that agda has as of the new 2.5 release, where there's a type checking monad for proposed terms and the ability to choose to do error handling when a proposed term fails to type check. Note that their meta ast is unindexed, so the program fragments are constructed in a sort of untyped debrujin data model of agda terms </p>
<div class="gmail_quote">On Apr 18, 2016 10:04 AM, "Richard Eisenberg" <<a href="mailto:eir@cis.upenn.edu" target="_blank">eir@cis.upenn.edu</a>> wrote:<br type="attribution"><blockquote style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div><br>
On Apr 18, 2016, at 9:45 AM, Simon Peyton Jones <<a href="mailto:simonpj@microsoft.com" target="_blank">simonpj@microsoft.com</a>> wrote:<br>
<br>
> Well, it opens up the entire issue of dependence on typechecking order and reification. Other things being equal, simple is good...<br>
<br>
</div>Of course that's true, but other things aren't equal -- losing Q decreases the usefulness of typed TH. I agree that there is some nastiness regarding reification. We could refuse to reify something from the same group. I'm not sure how hard that would be to enforce. Or if reification were a real bear, we could provide the IO monad.<br>
<br>
Just to see how this is used, I poked around in a download of all of Hackage from September 2015. Here's what I found.<br>
<br>
- 6 packages use typed TH: clash-prelude-0.9.2, llvm-general-quote-0.2.0.0, lookup-tables-0.1.1.1, network-uri-static-0.1.0.0, refined-0.1.1.0, and validated-literals-0.2.0.<br>
<br>
- None seem to use the ability to do work in the Q (or IO) monad.<br>
<br>
- Two (lookup-tables and refined) do use the fact that the TExp constructor is exported from Language.Haskell.TH.Syntax to make an untyped TH expression and unsafely force it into a typed TH expression. If we're going to close back doors, this seems like a much wider one than access to Q.<br>
<br>
So I guess this suggests that taking typed TH out of the Q monad wouldn't be too disruptive. But saying "no reification of anything, anywhere" seems like a big sledgehammer to stop people from reifying local things whose typed haven't settled yet.<br>
<div><br>
Richard<br>
_______________________________________________<br>
ghc-devs mailing list<br>
<a href="mailto:ghc-devs@haskell.org" target="_blank">ghc-devs@haskell.org</a><br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs</a><br>
</div></blockquote></div>
<br>_______________________________________________<br>
ghc-devs mailing list<br>
<a href="mailto:ghc-devs@haskell.org" target="_blank">ghc-devs@haskell.org</a><br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs</a><br>
<br></blockquote></div><br></div>
</div></div></blockquote></div><br></div>