Reification of out-of-scope variables?

[Boespflug, Mathieu]

Hi all,

For our use case, namely automatic bindings generation via
quasiquotation à la language-c-inline, typed quasiquotation alone
wouldn't solve much. Because in order to be sensible it would likely
have to be restricted (one way or another) to only allowing
reification of variables in the previous declaration groups (since we
AFAICT all agree that the current permissiveness of reification in
typed splices is a bug). That won't fit the use case, since it's
precisely the types of the locally bound variables we're interested in
(see examples on the updated wiki page:
https://ghc.haskell.org/trac/ghc/wiki/TemplateHaskell/Reify).

So that brings us back to the question of allowing addModFinalizer to
capture the local type environment of the call site somehow. There's a
proposal for this that Facundo came up with and wrote up at the end of
the aforementioned wiki page, but does anyone else have a better way
of doing this in mind?

Best,
--
Mathieu Boespflug
Founder at http://tweag.io.


On 16 April 2016 at 16:02, Richard Eisenberg <eir at cis.upenn.edu> wrote:
>
> On Apr 15, 2016, at 11:51 AM, Simon Peyton Jones <simonpj at microsoft.com> wrote:
>>
>> Hang on!  The design for typed splices, describe here,
>> https://ghc.haskell.org/trac/ghc/wiki/TemplateHaskell/BlogPostChanges
>> says "Unlike TH, the only way to construct a value of type TExp is with a quote. You cannot drop into do-notation, nor use explicit construction of the values in the Exp algebraic data type. That restriction limits expressiveness, but it enables the strong typing guarantees."
>>
>> So why does the above work?  $$(e) requires a TExp, and do-notation doesn’t produce a TExp.
>
> Indeed this is true -- this is what that page says. But it's not what's implemented: when I say $$( _ ) :: Bool, GHC tells me that the hole has type Q (TExp Bool).
>
> There still is no way to create a TExp other than to use a type TH quote.
>
> Addressing your other message: a typed quasiquoter would be somewhat limited, but not utterly silly. For example, this works:
>
>> bool :: String -> Q (TExp Bool)
>> bool "true"  = [|| True ||]
>> bool "false" = [|| False ||]
>> bool _ = fail "not a bool"
>>
>> -- and then, in another module because of the stage restriction:
>> yes :: Bool
>> yes = $$(bool "true")
>
> Now `bool` could be a typed quasiquoter.
>
> I don't know whether any of this is worth implementing, but it's not, a priori, a terrible idea.
>
> Richard
>
>>
>> |  * Should we consider it a bug (and file a ticket) that reification in
>> |  typed splices is able to observe the order of type checking, just like
>> |  reify used to do in untyped splices?
>>
>> Yes I think so!!!
>>
>> Simon
>>
>