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"
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@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs