On Fri, Dec 30, 2011 at 5:05 PM, Simon Peyton-Jones wrote:

| Currently quote forms have type "Q Exp" and nested splices expect | their contents to have type "Q Exp".  I propose that quote forms have | type "forall m. Quasi m => m Exp" and nested splices expect a body of | type "m Exp" where the "m" of the nested splice is the same as the "m" | of the quote form that it is inside of.

Happily they already have that type.  Have a look in Language.Haskell.TH.Syntax:   newtype Q a = Q { unQ :: forall m. Quasi m => m a }

You want a function from "Q Exp" to "forall m. Quasi m => m Exp".  It would have type

  Q Exp -> forall m. Quasi m => m Exp

or, isomorphically

  forall m. Quasi m => Q Exp -> m Exp

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.

| > 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.) Simon

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@gmail.com] | Sent: 31 December 2011 19:59 | To: Simon Peyton-Jones | Cc: libraries@haskell.org | Subject: Re: Proposal: Overloaded Quotes for Template Haskell | | On Sat, Dec 31, 2011 at 7:55 AM, Simon Peyton-Jones | 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".

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 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 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@gmail.com] |  Sent: 31 December 2011 19:59 |  To: Simon Peyton-Jones |  Cc: libraries@haskell.org |  Subject: Re: Proposal: Overloaded Quotes for Template Haskell | |  On Sat, Dec 31, 2011 at 7:55 AM, Simon Peyton-Jones |   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".