Reification of out-of-scope variables?

[Michael Sloan]

I have considered how to add this capability some in the past, it's
something I'd also like to have.  Collecting the type info in the module
finalizer is an interesting idea!  This may well be the cheapest way to get
the info necessary for this usecase.

As far as I understand it, currently we're in the middle of typechecking
when quasiquotes get run, so we don't yet have concrete.  The types of
reified variables may well depend upon the type of the expression generated
by the quasi-quote.  There seems to be a straightforward-ish way to resolve
this - run typechecking twice.  The first typechecking pass uses
quasi-quotes substituted with stub versions of their output.  For this
example, it'd be (undefined :: IO double).  To support this, we'd add a
(Maybe ExpQ) field to QuasiQuoter, hopefully doing this in a way that
preserves backwards compatibility (via pattern syns, or adding a new
constructor to QuasiQuoter).

For consistency, we would want to ensure that the stub unifies with the
expression that actually gets used.  To enforce this, we'd typecheck
something equivalent to

case True of
    True -> ... -- generated code
    False -> (undefined :: IO Double)  -- stub

My particular use case is similar, in that it's related to FFI.  What I
want to do is have quasiquoters for typescript in GHCJS code.  Since GHCJS
already runs TH in node, we can actually load up the typescript compiler
and do the typechecking directly at the quasi-quote location.  For the
first-pass stubs, we pretend like all the captured variables are the "Any"
type, and ask typescript what it thinks the overall type is.  For the
second pass, we have the types of the anti-quotes, and so can typecheck the
whole expression.

It'd also be really cool if we could generated code + typecheck anti-quotes
during the first pass.  This would make it possible to use anti-quotes
which are more complicated than just a variable.

-Michael

On Fri, Apr 8, 2016 at 6:48 AM, Boespflug, Mathieu <m at tweag.io> wrote:

> Hi all,
>
> the community is increasingly using quasiquotation as a means to
> interoperate with foreign languages. E.g. language-c-inline, inline-c
> and inline-r allow calling foreign functions using foreign language
> syntax, rather than "foreign import" declarations. There are efforts
> underway for Java, Javascript and other languages too. The pattern
> common to most of these libraries is:
>
> * collect the content of all quasiquotes that appear in a module,
> generate a compilable foreign source file based on that, and then link
> the object code resulting from compiling that.
>
> When the foreign language is itself statically typed, we need to make
> sure we generate code with proper type annotations, including for any
> antiquotation variables. In older versions of GHC, we could derive the
> type annotations from the inferred Haskell types, but this is not
> possible since 7.8 because the types of any variable in the current
> "declaration group" are not made available. So libraries like inline-c
> ask for some extra verbosity from the user:
>
> mycossin1 :: Double -> IO Double
> mycossin1 somex = [cexp| double { cos($(double somex)) * sin($(double
> somex)) } |]
>
> The type annotations inside the quasiquote are redundant with the
> explicitly provided type signature. C types are typically short
> enough, but other languages (e.g. C++, Java), have really long fully
> qualified type names, so the extra annotations are a cost.
>
> The are good reasons why types aren't available from within a
> declaration group (it was possible to observe the order in which type
> inference works), hence why the extra annotations are necessary. But
> by the time type checking of the whole module is finished, types are
> fixed once and for all. So the question is:
>
> * Could we make it possible to query the types of local variables at
> the end of type checking?
>
> The reason I ask is: with 'addModFinalizer' and friends that TH
> provides, we're tantalizingly close to being able to generate foreign
> code wrappers that have the right types that match those of the
> antiquotation variables present in a module.
>
> Template Haskell already provides 'addModFinalizer'. You feed it a Q
> action, which will run once the whole module is type checked. If at
> that point we could ask, "what's the type of somex (above)?", then we
> could let the user write
>
> mycossin2 :: Double -> IO Double
> mycossin2 somex = [cexp| cos($somex) * sin($somex) |]
>
> and yet still generate a C file capturing the content of above
> quasiquote with the right types:
>
> double module_foo_qq1(double v1)
> {
>     return (cos(v1) * sin(v1));
> }
>
> since we know that somex :: Double and that the Haskell type "Double"
> corresponds to C's "double" primitive type.
>
> Bound variables have a unique name associated to them, which we can
> get hold of in Template Haskell using the 'var syntax, but
>
> f x = $(let name = 'x in addModFinalizer (reify name >>= \info ->
> runIO (print info)) >> [| x |])
>
> results in a compiler error,
>
>     The exact Name `x' is not in scope
>       Probable cause: you used a unique Template Haskell name (NameU),
>       perhaps via newName, but did not bind it
>       If that's it, then -ddump-splices might be useful
>
> because by the time the TH finalizer runs, we're no longer in the scope of
> x.
>
> But since the names of the local variables are unique, could it
> possibly make sense to allow calling reify on them, even outside of
> their scope, so as to get at their type?
>
> Best,
>
> Mathieu
> _______________________________________________
> ghc-devs mailing list
> ghc-devs at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20160408/02e2e1d1/attachment.html>