Should TH TExp be able use the Q monad

[Carter Schonwald]

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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20160418/e143f158/attachment.html>