Should TH TExp be able use the Q monad

[Thomas Bereknyei]

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.

On Mon, Apr 18, 2016 at 2:49 PM, Carter Schonwald <
carter.schonwald at gmail.com> wrote:

> 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
> On Apr 18, 2016 10:04 AM, "Richard Eisenberg" <eir at cis.upenn.edu> wrote:
>
>
> On Apr 18, 2016, at 9:45 AM, Simon Peyton Jones <simonpj at microsoft.com>
> wrote:
>
> > Well, it opens up the entire issue of dependence on typechecking order
> and reification.  Other things being equal, simple is good...
>
> 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.
>
> 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.
>
> - 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.
>
> - None seem to use the ability to do work in the Q (or IO) monad.
>
> - 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.
>
> 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.
>
> Richard
> _______________________________________________
> ghc-devs mailing list
> ghc-devs at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>
>
> _______________________________________________
> ghc-devs mailing list
> ghc-devs at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20160418/1589d39d/attachment.html>