Should TH TExp be able use the Q monad
| > Hang on! The design for typed splices, describe here, | > https://ghc.haskell.org/trac/ghc/wiki/TemplateHaskell/BlogPostChanges | > says "Unlike TH, the only way to construct a value of type TExp is | with a quote. You cannot drop into do-notation, nor use explicit | construction of the values in the Exp algebraic data type. That | restriction limits expressiveness, but it enables the strong typing | guarantees." | > | > So why does the above work? $$(e) requires a TExp, and do-notation | doesn’t produce a TExp. | | Indeed this is true -- this is what that page says. But it's not what's | implemented: when I say $$( _ ) :: Bool, GHC tells me that the hole has | type Q (TExp Bool). | There still is no way to create a TExp other than to use a type TH quote Humph. I suppose that provided you can't forge a TExp, there's no way to splice in a type-incorrect program; and having Q available lets you (say) do input/output or consult the context to decide which of two quotes to return. We could do this selectively. For example we'd certainly need (TExp t) to be able to fail
bool :: String -> TExp Bool bool "true" = [|| True ||] bool "false" = [|| False ||] bool _ = failTexp "not a bool"
My instinct is to make it less expressive, though, and only allow (TExp t) as the argument of $$. Does anyone care either way? I suppose we'd better open a ticket for this. Simon | | quote. | | Addressing your other message: a typed quasiquoter would be somewhat | limited, but not utterly silly. For example, this works: | | > bool :: String -> Q (TExp Bool) | > bool "true" = [|| True ||] | > bool "false" = [|| False ||] | > bool _ = fail "not a bool" | > | > -- and then, in another module because of the stage restriction: | > yes :: Bool | > yes = $$(bool "true") | | Now `bool` could be a typed quasiquoter. | | I don't know whether any of this is worth implementing, but it's not, a | priori, a terrible idea. | | Richard | | > | > | * Should we consider it a bug (and file a ticket) that reification | > | in typed splices is able to observe the order of type checking, | > | just like reify used to do in untyped splices? | > | > Yes I think so!!! | > | > Simon | >
On Apr 18, 2016, at 9:14 AM, Simon Peyton Jones
My instinct is to make it less expressive, though, and only allow (TExp t) as the argument of $$.
Does anyone care either way? I suppose we'd better open a ticket for this.
I don't see any harm that is introduced by having access to the Q monad. As you say, as long as we can create only well-typed TExps, it doesn't seem to matter what information we have access to on the way. In other words: what's the gain by reducing expressiveness here? Richard
Well, it opens up the entire issue of dependence on typechecking order and reification. Other things being equal, simple is good...
Simon
| -----Original Message-----
| From: Richard Eisenberg [mailto:eir@cis.upenn.edu]
| Sent: 18 April 2016 14:36
| To: Simon Peyton Jones
On Apr 18, 2016, at 9:45 AM, Simon Peyton Jones
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
participants (2)
-
Richard Eisenberg -
Simon Peyton Jones