Proposal: Overloaded Quotes for Template Haskell

[Michael D. Adams]

As suggested, I've written up the typing judgement that have to change
relative to the TH paper.  (Only two judgments have to change.)  I've
attached those in a PDF to avoid having to write typing judgments in
ASCII art.  If the PDF causes any one trouble, let me know and I can
transcribe it to ASCII art.

I'm not opposed to writing an implementation myself, but I'm not
terribly familiar with the internals of GHC so it would be difficult.
(I really don't understand the treatment of "pending splices" or
HsSpliceOut.)

I agree that top-level splices must run in the type-checker monad, but
I don't see why nested splices would need to.  For example, consider
"$( runStateT [| 1 + $(quux) |] 0)" where "quux :: StateT Int Q Exp"
and an appropriate "Quasi" instance is declared for "StateT".  I'm
thinking of quotes like [| 1 + $(quux) |] as equivalent to "do e1 <-
quux; return (InfixE (Just (LitE (IntegerL 1))) (VarE "GHC.Num.+")
(Just e1)".  What I'm proposing is simply that the quote form along
with it's immediately nested splices have the same types as in the
do-block form.

I do want to be sure you fully understand what I'm proposing.  Let me
know if the type judgments don't make it clear, and I'll try to figure
out how to better explain it.

On Thu, Jan 5, 2012 at 10:08 AM, Simon Peyton-Jones
<simonpj at microsoft.com> wrote:
> I'm sorry Michael, I just don't get it. Maybe I'm just being slow.
>
> One difficulty is that top-level splices (and hence, recursively) nested splices, must be run in the typechecker monad; and TH knows nothing of that monad.  That's why the Quasi class exists in the first place; it says exactly what the "host monad" (the typehcecker in this case) must support.  By moving to ST you are fixing the monad, and I just don't see how to make that work.
>
> Perhaps the thing to do is to write some typing judgements, as in the TH paper, or to implement a prototype, or to write up a design in more detail.  Template Haskell always does my head in.
>
> Sorry not to be more helpful
>
> Simon
>
> |  -----Original Message-----
> |  From: Michael D. Adams [mailto:mdmkolbe at gmail.com]
> |  Sent: 31 December 2011 19:59
> |  To: Simon Peyton-Jones
> |  Cc: libraries at haskell.org
> |  Subject: Re: Proposal: Overloaded Quotes for Template Haskell
> |
> |  On Sat, Dec 31, 2011 at 7:55 AM, Simon Peyton-Jones
> |  <simonpj at microsoft.com> wrote:
> |  > |  > And indeed there is such a function: it's called runQ.
> |  > |  >
> |  > |  > So I think what you want is already available.
> |  > |
> |  > |  If there are no splices in the quote then, yes, that is sufficient.
> |  > |  However, as there is no function of type "forall m. Quasi m => m Exp
> |  > |  -> Q Exp", the contents of all splices must be of type "Q Exp".  Thus
> |  > |  in the expression "[| ... $( foo ) ... |]" there is no way for foo to
> |  > |  modify the state of the memoization table.
> |  >
> |  > I'm sorry, I don't understand what you say here.
> |  >
> |  > You started your post by saying that you want quote to be of type
> |  >        forall m. Quasi m => m Exp
> |  > But they already are! (With a newtype wrapper.)
> |
> |  The constructor of that newtype wrapper is *not* exported by the
> |  Template Haskell libraries.  The destructor *is* exported in the form
> |  of "runQ" (which is equivalent to "unQ" (and I don't know why the two
> |  names)), but the constructor "Q" is not.
> |
> |  However, while it may look like exporting "Q" is sufficient to get
> |  what I want, that doesn't quite work.
> |
> |  To see why it doesn't work, suppose we have:
> |   - "c :: StateT S Q Exp -> StateT S Q Exp" and
> |   - "e :: StateT S Q Exp" and
> |   - "instance Quasi (StateT s Q)".
> |
> |  Now, consider "c (runQ [| ... $(Q (e)) ... |])".  There will be a type
> |  error in the application of "Q" to "e" since "forall m. Quasi m => m
> |  Exp" is not an instantiation of "State S Q Exp".
> |
> |  However, if the types of quotes and splices are generalized as I
> |  proposed, then "c [| ... $(e) ... |]" will type check just fine and
> |  achieve the effect that I'm after.
> |
> |  Another way to think of this distinction is to the quotes as
> |  functions.  The function "\e = [| ... $e ... |]" has type "Q Exp -> Q
> |  Exp".  On the other hand the function "\e -> runQ [| ... $(Q e) ...
> |  |]" has type "(forall m. Quasi m => m Exp) -> (forall m. Quasi m => m
> |  Exp)".  Note that the two "m" do not unify.  Under my proposal "\e ->
> |  [| ... $e ... |]" would have type "forall m. Quasi m => m Exp -> m
> |  Exp".
>
>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: quote.pdf
Type: application/pdf
Size: 141476 bytes
Desc: not available
URL: <http://www.haskell.org/pipermail/libraries/attachments/20120105/42f5ca14/attachment-0001.pdf>