Proposal: Overloaded Quotes for Template Haskell

[Michael D. Adams]

Simon, the two-week deadline has passed but I'm hesitant to transfer
this to the bug tracker unless you're on board (GHC HQ would likely be
the ones to implement it afterall).  Does what I'm suggesting make
sense, or do we need more discussion on/explanation of this?

On Thu, Jan 5, 2012 at 1:07 PM, Michael D. Adams <mdmkolbe at gmail.com> wrote:
> 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".
>>
>>