<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">eir@cis.upenn.edu</a>> wrote:<br type="attribution"><blockquote class="quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div class="quoted-text"><br>
On Apr 18, 2016, at 9:45 AM, Simon Peyton Jones <<a href="mailto:simonpj@microsoft.com">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 class="elided-text"><br>
Richard<br>
_______________________________________________<br>
ghc-devs mailing list<br>
<a href="mailto:ghc-devs@haskell.org">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>