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

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

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.

…or an I/O action:

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.

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

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?