Could GHC track whether a particular value is known at compilation time?

21

Code is a funny type. It has definitions of bind (EDIT: this is actually a slightly different function), and I’m pretty sure it could have a definition of <*> (surely if we have code for a function and code for the argument, we can make code for the application of the two), but it doesn’t have an unrestricted pure, you need a Lift constraint for that.

Which also means you can’t make a derived Functor instance, because you can’t lift a function to then use <*>.

So it’s annoyingly close to being able to actually use sequence, and I suspect the functions like sequenceCode that you would write will look rather like the generic ones, just with some extra explicit (or solved) Lift constraints.

I wonder if there is a way to do things generically, then…

2 Likes
22

One could imagine a language with a templating system such that any runtime value in the templating system can be slurped up and converted to a literal in the generated code. That would be great, except when the slurped up value is something that’s very specific to the runtime system, such as a reference or a file handle. Perhaps what we have in TH is as good as we can get without running into those kinds of problems.

23

…or an I/O action:

24

Wouldn’t it hold that for any proper Lift a => Lift (f a) instance there must also exist sequence :: Quote m => f (Code m a) -> Code m (f a)? For deriving the difference is just in the data-level a.

25

That’s what I meant with Lift1. Pretty sure that these instances can be derived by template Haskell, a la th-lift.

26

There’s probably a sub category of Hask of all types that satisfy Lift and in which all type constructors satisfy Lift1. Then you can define Functor, Applicative and perhaps Monad. But what’s the point?

27

I think I’ve tried enough Template Haskell to point what my issues with it are. Here’s an example:

I made an Applicative JSON object parser here. Its operation is relatively trivial:

  1. Fail if any of the provided keys are duplicates;

  2. Collapse the list of pairs down into a radix tree;

  3. Run the input through the tree, applying the decoders on first occurrence of each relevant key;

  4. Fail if there are unmatched non-optional decoders in the resulting tree;

  5. Extract the data from the resulting tree.

Compilation-time evaluation can definitely take points 1 and 2, and may optimize 4 and 5 with tree references instead of keys.

The Template Haskell counterpart of that same object parser is here. It only uses typed splices and fail, so in my mind this is entirely type-safe and could well be a separate extension. The downsides are:

  • Referencing runtime values means lifting them into Code Q, so every existing type class is incompatible with this new model;

  • All code for points 1, 2, 4 and 5 must be written anew as well, even though morally these two versions should be interchangeable;

  • $$(pairsQ $ "key" .| [|| f ||]) is so much worse to write than pairsA ("key" .: f).

I don’t know how any of these can be addressed by Template Haskell and I find it impractical in its current state.

3 Likes
28

Thanks for giving it such a thorough try, that is very useful data.

I think that what you are describing are inadequacies in TH’s current implementation.

Referencing runtime values means lifting them into Code Q, so every existing type class is incompatible with this new model;

I’m not sure I understand this point completely without an example, but it sounds related to the problems discussed in Staging with Class.

All code for points 1, 2, 4 and 5 must be written anew as well, even though morally these two versions should be interchangeable;

Can’t you generate the non-TH version from the TH version? Intuitively, the latter should just be a semantically richer version of the former.

$(pairsQ $ "key" .| [|| f ||]) is so much worse to write than pairsA ("key" .: f).

Yes, that’s a bit ugly. If we had proper macros, we could probably sugar this up into pairsQ ("key" .| f), but we do not currently (and I would not hold my breath).
Another alternative to achieving neater syntax would be to infer the staging operations as exemplified in 2.3.2 of Staged Compilation with Two-Level Type Theory (Up arrow is “Code”). You would simply write pairsQ "key" f and let the type system work out via expected type that f is bound at runtime stage, "key" at compile-time and pairsQ at compile-time as well. Alas, I’m not sure where that fits into GHC’s current agenda, where we want to be more explicit about which binding is used at which stage.

Note that any other mechanism for compile-time eval would need to figure out these problems as well. TH is the best we have, yet still inadequate.

2 Likes