Should TH TExp be able use the Q monad

[Carter Schonwald]

to better clarify what i'm referrring to i shall link to
http://agda.readthedocs.org/en/latest/language/reflection.html
which describes the agda reflection / type checking monad and associated
quote/unquote facilitie further

On Mon, Apr 18, 2016 at 2:50 PM, Thomas Bereknyei <tomberek at gmail.com>
wrote:

> 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/97354afa/attachment.html>