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 <[email protected]> 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 < > [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
