Stage Hygiene for Template Haskell

[Ericson2314]

Template Haskell currently doesn't work well with cross compilation. This is a big nuisance for anyone making phone or browser software. To fix this, enforce stronger separation between the stages.

There are some TODOs, but I am purposefully leaving them there now to be resolved during discussion.

Rendered

[mpickering]

There are some good ideas in this proposal and I would like to work with you on getting this proposal into shape. At the moment the key ideas are a bit lost in the weeds so it would be good to distinguish the fundamental from the accidental.

[goldfirere]

I have not thought deeply about the cross-compilation problem for TH, but this seems plausible. I'm broadly in support of something like this, as long as it doesn't make TH harder to use for those not worried about cross-compilation (unless there's a very compelling reason to burden us). The motivation section of the proposal is compelling to me.

[michaelpj]

Do we need to expose the full complexity of stage offsets in user-visible syntax? This comes up in a couple of places:

• In source Haskell you propose stage-offset imports and bindings.
• In Cabal you propose stage-offset dependencies.

However the other existing systems seem like they can get away with only exposing two phases to the user:

• In Racket, you have define-for-syntax and import-for-syntax, but nothing more.
• In other systems that handle cross compilation you have "native build dependencies" and nothing more.

I think both of these correspond to exposing the -1 and 0 stages and no others, and they have the advantage of being relatively easy to describe, whereas I am worried that the full stage offsetting machinery will be hard for people to understand (I certainly found it hard to understand!).

While it might make sense for the underlying system to know about phases in full generality, I'd be interested in how much expressiveness we would lose if we were to restrict the surface syntax (at least initially - we could add a fuller version later if we needed it).

For example, I think it would make it impossible to do anything too fancy within a single package (component?), but this might be an acceptable price to pay.

[Ericson2314]

@mpickering and I have talked quite a lot already, and I would like to thank him for putting up with me stumbling through a rather large backlog of hitherto unexpressed ideas.

@goldfirere

as long as it doesn't make TH harder to use for those not worried about cross-compilation (unless there's a very compelling reason to burden us)

You are on the money. I am definitely imposing a burden, but I hope to justify it.

@michaelpj

In Racket, you have define-for-syntax and import-for-syntax, but nothing more.

Ah but see https://docs.racket-lang.org/guide/phases.html. There is a for-meta with an explicit phase offset just like here! Heh, I haven't looked at the Racket docs in a while....turns out they count the phases in the other direction. oops!

While it might make sense for the underlying system to know about phases in full generality, I'd be interested in how much expressiveness we would lose if we were to restrict the surface syntax (at least initially - we could add a fuller version later if we needed it).

So do note that I restrict the user to stages -1, 0, and 1 in a single module. This correspond's to Racket's for-syntax, for-meta, and for-template. As you say, it is important that the overall system understand things more broadly since a composition of modules via offset imports can generate more stages than those 3. I even agree 2 at a time is most likely...except sometimes it's -1 and 0, and sometimes it's 0 and 1.

[Ericson2314]

CC @nh2 I wrote up @mboes's point about easier static linking, which should interest you.

---

Where I wanted a "typed AppE', i wrote a function instead. There is no principle type for that (yet!), so I just used multiple versions.

---

OK, so with that I think I've included all the new ideas, and hopefully clarified the background with a appendix on cross compilation in general. There are still the TODO's around clarifying the Cabal changes + bikeshedding cli syntax, but, well, I think it's better to make sure the GHC parts / big picture before that.

[nh2]

@Ericson2314 Since I was just pinged here I haven't read everything yet, but here is another idea in case that isn't included yet:

I believe most TH is some very simple "pure" syntax generation, like generating lenses.

"Pure" means it doesn't do any runIO and it is architecture independent.

Thus it can always be run on the host in the interpreter; no need for external interpreters or any object code generation.

Thus I propose: Let's make a "pure" variant of TH that isn't allowed to do any runIO. Then we can always run that on the host

[Ericson2314]

@nh2 Yes I am sympathetic to that, but to be clear I don't think it is a substitute for what is being proposed here. For example in the static linking use-case, that wouldn't help only build SOs when needed (for TH), and ensure they weren't part of the run-time closure (to use the Nix term).

[michaelpj]

@nbp I agree. But we'd need to be careful in specifying what we mean by "architecture-independent" (getting rid of IO seems comparatively easy).

[JacquesCarette]

I think that @nh2 's idea of having a "pure" part of TH is an excellent, and relatively small, first step in the direction of this proposal. It could be done independently, and might gather a lot more support. And is in line with other current proposals about TH. This current proposal is so huge, breaking it down into small steps is likely the best way of actually making forward progress.

[Ericson2314]

I'm worried about the opposite. I think most people won't know what they are missing and declare that good enough, sapping support for this proposal.

Besides the other benefits like build incrementality and static linking, saying pure TH is good enough is saying there is some subset of Haskell where the build and host coincide. But I'm interested long term in cross compiling to really exotic targets: circuits, embedded systems with no dynamic memory allocation, etc etc.

I really rather rip off the bandaid and start with no assumption the build and host have anything in common. It's the correct programming model.

[lexi-lambda]

This proposal seems somewhat dormant. But since it was linked in a recent Twitter discussion, I figured I’d still chime in.

I mostly want to say this: please consult the Racket prior art for this. There are a handful of fairly tricky details here, but Racket gets all of them right and has successfully used a phased compilation model for almost two decades now. The canonical publication about this is Composable and compilable macros: you want it when?, which explains the core issues concisely and outlines a clear solution.

I can say from personal experience that Racket’s model gets all of this overwhelmingly right. It handles everything I’ve ever thrown at it (which is a lot), it’s easy to use, and it is conceptually simple. What’s more, it has since been successfully extended with additional features that one could, in theory, imagine Haskell programmers finding useful as well, such as nested modules, discussed in Submodules in Racket: You Want it When, Again?.

Racket’s phasing system is sophisticated enough to support local macro definitions (i.e. elimination of the GHC stage restriction), predictable compilation with arbitrary, user-defined, compile-time state, and full macro hygiene. Fully adopting all the features of Racket’s module system is out of scope for TH in the short term, but there is no reason to not adopt a common subset, as many of those features would be useful in Haskell as well. In particular, I would recommend making positive numbers “more compile-time” phases and negative ones “closer to runtime” phases, simply because the choice is wholly arbitrary and opposite conventions would be needlessly confusing. (Also, in practice, references to positive phases seem to occur much more often in Racket than negative ones.)

[Ericson2314]

Being like Racket is absolutely the goal here. The order of the integers was an unconscious holdover from Nixpkgs where I last did this sort of thing; I'm happy with flipping the order.

This is mainly been dormant as we [mainly @hsyl20!] chip away at https://github.com/hsyl20/ghc-cross-compilation. The prereqs for this are less controversial, and after those are done I think this proposal will be easier to discuss because the marginal cost will be substantially less.

[wz1000]

My suggestion would be to start small, with the simplest, most conservative change that yields tangible benefits.

For me, this would be something like -XStagedImports, which would require "compile time" imports to be explicitly marked.

For example

{-# LANGUAGE StagedImports #-} 
{-# LANGUAGE TemplateHaskell #-} 
module MyModule where

import {-# META #-} Data.Aeson.TH
import {-# UNRESTRICTED #-} Data.Singletons.TH
import Control.Lens.TH

data Foo = ...
deriveJSON defaultOptions ''Foo -- This is legal
genSingletons [''Foo] -- This is too

foo = genSingletons -- This also

makeLenses ''Foo -- This is not

someOptions = defaultOptions -- Neither is this

Packages making use of StagedImports can be backwards compatible if they switch the extension on conditionally in the cabal file, and use -Wno-unrecognised-pragmas for older GHCs.

This would be a major improvement for the purposes of ghcide. We usually don't need to compile code and can just get away with typechecking, but in the presence of any module using -XTemplateHaskell we have to conservatively go and compile everything below it in the module graph, even if nothing downstream from the package is actually being used in a splice, and TH is only used for things like deriveJSON etc.

With -XStagedImports, the impact of this can largely be limited to what is strictly necessary.

[Ericson2314]

@wz1000 I'm sympathetic to the use-case and urgency, but I don't think that will be substantially easier than the whole thing, as I think most of the work GHC will be wrangling the internally separate modules for each stage.

[wz1000]

as I think most of the work GHC will be wrangling the internally separate modules for each stage.

Don't we just need to split the GlobalRdrEnv into two for my proposed change?

[Ericson2314]

My plan was just to split the whole module in two, so mainly changes in driver but compiling each module stays more same. (Eventually we can split apart Rn and Tc again because the computed splices will be provided by the driver, but that comes later.)

[mpickering]

I think I agree with @wz1000 here that starting like he proposes is best and then we can adapt a more complicated schema later. The majority of the benefit for normal users is gained from his proposal.

[Ericson2314]

The spit modules are needed for cross, but not just to solve the incrementally issues. For this one I would keep that approach, but for @mpickering's I also agree we might be able to get away with something simpler. That's why I like the division between the two proposals.

That said, I'm not sure a split module isn't in fact the easier. The current interleaving of TH and other things is a mess, and "just splitting GlobalRdrEnv" reminds me of -dynamic-too --- a simple concept but one that that just contributed to the clutter given the sorry state of today's abstractions.

Still, this can all be dealt with later. Main thing to do is start incrementally approving designs. We can see how all the driver projects fit together after.

[konsumlamm]

Suggested change

	*.See the appendix for what those mean.*
	*See the appendix for what those mean.*

[konsumlamm]

Suggested change

	This was bad for uses wishing to cross compiler, of course, but also bad for everyone else.
	This was bad for users wishing to cross compile, of course, but also bad for everyone else.

[konsumlamm]

Suggested change

	Also, while same-OS cross can sometimes be fairly lightweight
	Also, while same-OS cross compiling can sometimes be fairly lightweight

[konsumlamm]

Suggested change

	Still, this requires building every package twice, since we redo the entire compilation on both platforms, and worse doesn't work if a top-level splice is target specific.
	Still, this requires building every package twice, since we redo the entire compilation on both platforms, and worse, it doesn't work if a top-level splice is target specific.

[konsumlamm]

Suggested change

	Even if ``SomeIosFfiType`` doesn't have any iOS-only types in its definition, the generated code probably refers to ios-only identifiers::
	Even if ``SomeIosFfiType`` doesn't have any iOS-only types in its definition, the generated code probably refers to iOS-only identifiers::

[konsumlamm]

Suggested change

	But try focusing on the needing, the "why", so the subject and object are switched if you imagine being a anthropomorphized dependency node and looking at your now-flipped edges and new adjacent nodes like I do!
	But try focusing on the needing, the "why", so the subject and object are switched if you imagine being an anthropomorphized dependency node and looking at your now-flipped edges and new adjacent nodes like I do!

[konsumlamm]

Suggested change

	If you focus on the building, the work, and who does it, then the build platform is given undo importance:
	If you focus on the building, the work, and who does it, then the build platform is given undue importance:

[konsumlamm]

Suggested change

	We "need" something to be built that "run" on our platform, we don't care where it is built.
	We "need" something to be built that "runs" on our platform, we don't care where it is built.

[konsumlamm]

Suggested change

	stages greater than 0---quotes and nested quotes---corresponding to "target, "post-target", "post-post-target", do and must influence the interface.
	stages greater than 0 --- quotes and nested quotes --- corresponding to "target, "post-target", "post-post-target", do and must influence the interface.

[konsumlamm]

Suggested change

	If I have a ``-1`` import on ``Foo``, and splice some code from ``Foo``, I could end up with a quote form ``Foo`` in exposed in stage 0 of myself.
	If I have a ``-1`` import on ``Foo``, and splice some code from ``Foo``, I could end up with a quote from ``Foo`` exposed in stage 0 of myself.

[shlevy]

This is strictly speaking out of scope for TH, but dependent types does break this model a bit. On the one hand, values in type semantically need to match the target, on the other hand the typechecker needs to evaluate them on the host (or, more precisely, in the internal interpreter, if we have some kind of bytecode for the typechecker rather than using the results of native codegen). I raise it here only because a proper solution might involve changes relevant to just the TH case.

Thanks to @goldfirere and @lexi-lambda for helping clarify the constraints here.

[shlevy]

This is strictly speaking out of scope for TH, but dependent types does break this model a bit.

Actually I haven't looked in detail but perhaps this is basically the same problem with typed template haskell?

[Ericson2314]

@shlevy

if we have some kind of bytecode for the typechecker rather than using the results of native codegen

We do. Anything that is "transparent" to DH must have an unfolding. and then the type checker can munch on that. If you use data kinds and export a type synnonym the moral equivalent of that is happening.

As long as there no effects at the type level, we should be fine.

Actually I haven't looked in detail but perhaps this is basically the same problem with typed template haskell?

Yeah I don't expect typed Template Haskell to work too well. It doesn't have an IMO good enough phase separation. I think https://davidchristiansen.dk/pubs/tyde2020-predictable-macros-abstract.pdf is better, giving regular template Haskell enough power that we can not miss typed template haskell.

[Ericson2314]

Excitedly closing in favor of #682! The cabal parts would become an https://github.com/haskell/ecosystem-proposals