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 < [email protected]> 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" <[email protected]> wrote: > > > On Apr 18, 2016, at 9:45 AM, Simon Peyton Jones <[email protected]> > 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 > [email protected] > http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs > > > _______________________________________________ > ghc-devs mailing list > [email protected] > http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs > >
_______________________________________________ ghc-devs mailing list [email protected] http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
