Proposal: Overloaded Quotes for Template Haskell

[Simon Peyton-Jones]

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".