#4230: Template Haskell: less type checking in quotations?
---------------------------------+------------------------------------------
Reporter: simonpj | Owner:
Type: feature request | Status: new
Priority: normal | Milestone: 6.16.1
Component: Compiler | Version: 6.12.3
Keywords: | Testcase:
Blockedby: 4128 | Difficulty:
Os: Unknown/Multiple | Blocking: 4125, 4135, 4170
Architecture: Unknown/Multiple | Failure: None/Unknown
---------------------------------+------------------------------------------
Description changed by simonpj:
Old description:
> This ticket introduces two related Template Haskell design questions.
> It's inspired by several other tickets, for which these issues are the
> underlying cause
> * #4135
> * #4170
> * #4125
>
> -----------------------
> = ISSUE 1 =
>
> Consider this module
> {{{
> module M where
> import ...
> f x = x
> $(th1 4)
> h y = k y y
> $(th2 10)
> }}}
> In our present setup we typecheck down to the first splice, run the
> splice, then typecheck to the second splice, run that, and so on.
>
> But GHC's main structure is:
> * parse
> * rename (resolve lexical scopes)
> * typecheck
>
> The above setup makes this impossible. We can't even rename the
> definition of h until we've run the splice $(th1 4) because that might be
> what brings k into scope. All this is a bit hard to explain to users.
>
> Now suppose that instead we did the following.
>
> * Typecheck and run '''top-level''' splices in the renamer
>
> That is, when the renamer finds a top-level splice:
> * rename it
> * typecheck it
> * run it
> * replace the splice by the result of running it
> * and then rename *that* as if that's what the user had written in the
> first place
> But what about nested quotes? eg
> {{{
> $(th1 [| f x |])
> }}}
> Well we can't typecheck that quote, because we don't have a type for f
> and x, because we are in the renamer. But we don't '''need''' to
> typecheck the quote to be able to typecheck and run the splice!
> Remember, we already have a staging restriction that only imported
> functions can be '''run''' in a top-level splice.
>
> So the proposal would mean that we don't attempt to typecheck those
> nested quotes. Instead they'll be checked after the top-level splice is
> run, the result spliced in, and the whole shebang typechecked in the
> context of the program as a whole.
> This defers the error message, but not too muce, since typechecking the
> output of the splice is what will happen next.
>
> This approach would have a number of rather compelling advantages:
>
> * It would allow us to show the program after renaming and splice
> expansion, but before typechecking. That's quite helpful. It
> makes it easier to say that we
> * rename the program, and then
> * typecheck the program
> Remember, GHC is also a Haskell library, and the current
> story (a bit of renaming, a bit of typechecking, then a bit more
> renaming and a bit more typechecking) complicates the API.
>
> * Geoff Mainland's quasi-quotation mechanism is run in the
> renamer (because it can expand to patterns) so it would make
> all the TH stuff more consistent.
>
> * Even more exciting, we could support pattern splices, thus
> {{{
> f $(g 4) = x+y
> }}}
> because the splice $(g 4) would be typechecked and run, perhaps
> expanding to (x,y), say, by the renamer *before* it goes on to
> do scope-analysis on x+y. This is exactly why quasiquoting
> *can* do pattern splicing at the moment, and TH cannot.
> [[BR]][[BR]]
> This would fix a long-standing infelicity in TH, namely the
> absence of pattern splices.
>
> * In the same way we could support local declaration
> splices (which are currently ruled out)
> {{{
> f x = let $(g [| x |]) in ....
> }}}
> * At the top level we could get rid of the top-to-bottom bias.
> We could allow, say
> {{{
> f x = x+x
> $(th [| g |] [| f |])
> g y = y+1
> }}}
> One disadvantage is that it'd "bake in" the staging restriction that a
> splice can only (typecheck and) run functions imported from another
> module. Currently this is only an implementation restriction, which in
> principle might be lifted. On the other hand, I have no plans to lift
> it, and in practice people don't complain about it.
>
> ------------------
> = ISSUE 2 =
>
> Consider this:
> {{{
> f :: Q Type -> Q [Dec]
> f t = [d| data T = MkT $t;
> g (MkT x) = g+1 |]
> }}}
> This function f returns a declaration splice, declaring T and g.
> You'll see that the constructor MkT takes an argument whose type is
> passed (as a quotation) to f -- a type splice.
>
> The difficulty is that we can't typecheck the declaration of 'g'
> until we know what $t is; and we won't know that until f is called.
> So
> * we can't really typecheck the declaration quote at all
>
> In the case of '''term''' splices in a quotation we can simply give them
> type (forall a. a), which never gets in the way. But there is no
> equivalent for *type* splices. An analogous problem occurs in other
> declaration splices, for example
> {{{
> f t = [d| instance C $t where ... |]
> }}}
> Here GHC's check that an instance decl is always of form
> {{{
> instance C (T a b c)
> }}}
> falls over, again because we don't know what $t will be.
>
> It's hard to see what to do about this.
>
> * We could get rid of type splices (but people like them)
>
> * We could refrain from typechecking quotations *at all*
> I have users asking me for exactly this: #4125, #4135
>
> * We could refrain from typechecking *declaration* quotes.
> But the problem still happens for terms
> {{{
> [| let { f :: $t; f = e } in .. |]
> }}}
> * We could refrain from typechecking any quotation that
> included a type splice. This is probably the most benign:
> it switches off the type checker just when it's problematic,
> and it's very predictable when that is. Awkward to implement
> though.
>
> Do you have any other ideas?
>
> ----------------------
> = DISCUSSION =
>
> The two issues are related of course, because both involve doing
> less typechecking of quotations.
>
> That seems a pity, because it'd lose one of TH's advantages --
> that of typechecking meta programs rather than just typechecking
> the output of the meta programs. And in the case of ISSUE 2,
> error messages might get delayed, perhpas to another module
> altogether.
>
> However, we deliberately designed TH so that it ''is'' possible to
> get a type error when typechecking the result of a type-correct
> top-level splice. Reason: we use type Exp rather than (Exp t) as
> in MetaML. That gave us (a lot) more flexibility. Apart from
> anything else, declaration splices would be problematic in the
> MetaML approach.
>
> Seen in that light, the proposals here just move a bit further in
> the direction of flexibility, at the cost of somewhat-increased
> danger of errors being reported later than is ideal.
New description:
This ticket introduces two related Template Haskell design questions.
It's inspired by several other tickets, for which these issues are the
underlying cause
* #4135
* #4128
* #4170
* #4125
* #4124
-----------------------
= ISSUE 1 =
Consider this module
{{{
module M where
import ...
f x = x
$(th1 4)
h y = k y y
$(th2 10)
}}}
In our present setup we typecheck down to the first splice, run the
splice, then typecheck to the second splice, run that, and so on.
But GHC's main structure is:
* parse
* rename (resolve lexical scopes)
* typecheck
The above setup makes this impossible. We can't even rename the definition
of h until we've run the splice $(th1 4) because that might be what brings
k into scope. All this is a bit hard to explain to users.
Now suppose that instead we did the following.
* Typecheck and run '''top-level''' splices in the renamer
That is, when the renamer finds a top-level splice:
* rename it
* typecheck it
* run it
* replace the splice by the result of running it
* and then rename *that* as if that's what the user had written in the
first place
But what about nested quotes? eg
{{{
$(th1 [| f x |])
}}}
Well we can't typecheck that quote, because we don't have a type for f and
x, because we are in the renamer. But we don't '''need''' to typecheck
the quote to be able to typecheck and run the splice! Remember, we
already have a staging restriction that only imported functions can be
'''run''' in a top-level splice.
So the proposal would mean that we don't attempt to typecheck those nested
quotes. Instead they'll be checked after the top-level splice is run, the
result spliced in, and the whole shebang typechecked in the context of the
program as a whole.
This defers the error message, but not too muce, since typechecking the
output of the splice is what will happen next.
This approach would have a number of rather compelling advantages:
* It would allow us to show the program after renaming and splice
expansion, but before typechecking. That's quite helpful. It
makes it easier to say that we
* rename the program, and then
* typecheck the program
Remember, GHC is also a Haskell library, and the current
story (a bit of renaming, a bit of typechecking, then a bit more
renaming and a bit more typechecking) complicates the API.
* Geoff Mainland's quasi-quotation mechanism is run in the
renamer (because it can expand to patterns) so it would make
all the TH stuff more consistent.
* Even more exciting, we could support pattern splices, thus
{{{
f $(g 4) = x+y
}}}
because the splice $(g 4) would be typechecked and run, perhaps
expanding to (x,y), say, by the renamer *before* it goes on to
do scope-analysis on x+y. This is exactly why quasiquoting
*can* do pattern splicing at the moment, and TH cannot.
[[BR]][[BR]]
This would fix a long-standing infelicity in TH, namely the
absence of pattern splices.
* In the same way we could support local declaration
splices (which are currently ruled out)
{{{
f x = let $(g [| x |]) in ....
}}}
* At the top level we could get rid of the top-to-bottom bias.
We could allow, say
{{{
f x = x+x
$(th [| g |] [| f |])
g y = y+1
}}}
One disadvantage is that it'd "bake in" the staging restriction that a
splice can only (typecheck and) run functions imported from another
module. Currently this is only an implementation restriction, which in
principle might be lifted. On the other hand, I have no plans to lift it,
and in practice people don't complain about it.
------------------
= ISSUE 2 =
Consider this:
{{{
f :: Q Type -> Q [Dec]
f t = [d| data T = MkT $t;
g (MkT x) = g+1 |]
}}}
This function f returns a declaration splice, declaring T and g.
You'll see that the constructor MkT takes an argument whose type is passed
(as a quotation) to f -- a type splice.
The difficulty is that we can't typecheck the declaration of 'g'
until we know what $t is; and we won't know that until f is called.
So
* we can't really typecheck the declaration quote at all
In the case of '''term''' splices in a quotation we can simply give them
type (forall a. a), which never gets in the way. But there is no
equivalent for *type* splices. An analogous problem occurs in other
declaration splices, for example
{{{
f t = [d| instance C $t where ... |]
}}}
Here GHC's check that an instance decl is always of form
{{{
instance C (T a b c)
}}}
falls over, again because we don't know what $t will be.
It's hard to see what to do about this.
* We could get rid of type splices (but people like them)
* We could refrain from typechecking quotations *at all*
I have users asking me for exactly this: #4125, #4135
* We could refrain from typechecking *declaration* quotes.
But the problem still happens for terms
{{{
[| let { f :: $t; f = e } in .. |]
}}}
* We could refrain from typechecking any quotation that
included a type splice. This is probably the most benign:
it switches off the type checker just when it's problematic,
and it's very predictable when that is. Awkward to implement
though.
Do you have any other ideas?
----------------------
= DISCUSSION =
The two issues are related of course, because both involve doing
less typechecking of quotations.
That seems a pity, because it'd lose one of TH's advantages --
that of typechecking meta programs rather than just typechecking
the output of the meta programs. And in the case of ISSUE 2,
error messages might get delayed, perhpas to another module
altogether.
However, we deliberately designed TH so that it ''is'' possible to
get a type error when typechecking the result of a type-correct
top-level splice. Reason: we use type Exp rather than (Exp t) as
in MetaML. That gave us (a lot) more flexibility. Apart from
anything else, declaration splices would be problematic in the
MetaML approach.
Seen in that light, the proposals here just move a bit further in
the direction of flexibility, at the cost of somewhat-increased
danger of errors being reported later than is ideal.
--
--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/4230#comment:8>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler
_______________________________________________
Glasgow-haskell-bugs mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
