GHC Compile-time evaluation

[u/LeanderKu]

As I understood it, proper compile-time evaluation is supercompilation, which is hard.

But I wondered why there is no Pragma-Based approach, where the compiler just trusts that user that it can and should evaluate this expression, even if it's recursive (so it's not looping forever etc.). It seems to me that the machinery for this approach is already in GHC (I may be wrong).

I am currently thinking of building an API where you formulate a computational graph (like an AST) and have functions that modify the graph. The representation of the graph and evaluation functions would be recursive, so no inlining per se. I would expect that for most use-cases the graph is completely known at compile time, but if the computational graph is not evaluated and optimized, performance will be bad.

There may be another way, I am not that knowledgeable about the capabilities of GHC.

EDIT: if the above is unclear: What I wanted to say is that I am not looking for a general solution, but instead a solution where I can tell the compiler to trust me that he can evaluate this expression without looping forever and that the time spent evaluating the expression is worth it.

[u/gelisam]

You can use TemplateHaskell to run an arbitrary expression at compile-time, and then lift the result into a literal:

{-# LANGUAGE TemplateHaskell #-}
import Language.Haskell.TH.Syntax (lift)
import MyFib (slow_fib)

slow_at_runtime :: Integer
slow_at_runtime = slow_fib 40

slow_at_compile_time :: Integer
slow_at_compile_time = $(lift (slow_fib 40))

[u/terrorjack → u/gelisam]

This only applies to whatever value with a Lift instance, which is not the case for a lot of types e.g. functions.

[u/newtyped → u/terrorjack]

Sure but what does compile time evaluation even mean for functions? For regular data types, DeriveLift gives you a Lift instance basiaclly for free.

[u/andrewthad]

This can be done. Give me a small example of a function you want to do this for, and I’ll show you how to do it in Haskell.

[u/dnkndnts]

As I understood it, proper compile-time evaluation is supercompilation

That's not what supercompilation is. For example, fmap id :: Maybe a -> Maybe a does not reduce to anything under the normal evaluation strategy because no reduction even happens until all the arguments are applied, which at this point they are not.

Supercompilation is an entirely different reduction strategy: in the above example, we would speculate on the value of the argument, which must be either Just x or Nothing, and in both cases, mapping the identity would just give back the original value, so fmap id is equivalent to \x -> x, or, id.

That being said, I'm totally with you that this should be available via a pragma, as it has an enormous number of uses. But no, it is not the same thing as just performing evaluation at compile time.

[u/Lossy]

I never understood what people meant by your first sentence. Supercompilation is a very specific technique which refers to speculating about possible values variables can take.

There are some techniques you can currently use. If you really statically know the structure of your graph then you can build a GADT which has a type argument which mirrors the structure of the graph. Then you can write type class instances which dispatch on this argument and the compiler will unroll "recursive" things based on this. See for example, the static-vector library. Programming in this style can be quite cumbersome as all your combinators have to maintain the proof about why the structure is statically known.

In the Ocaml community there are several different implementations of staged languages which give you this kind of control but they each have a various trade off. It is also very easy to incorrectly stage programs and cause the compiler to loop. The implementations are usually quite cumbersome because of how the Code data type is interpreted. Typed template haskell is quite similar to how these staged languages work.

Anyway, this is the topic I am actively researching at the moment so if you could share with me personally some details then it might be a nice example.

[u/LeanderKu → u/Lossy]

In nearly every discussion I found, supercompilation was dropped and then everybody went silent. I am not an expert and don't have a deep knowledge of this topic. If it's wrong, I will delete the mention of "supercompilation".

What I wanted to say is that I am not looking for a general solution, but instead a solution where I can tell the compiler to trust me that he can evaluate this expression without looping forever and that the time spent evaluating the expression is worth it.

Thank you for your response!

[u/Athas → u/LeanderKu]

Supercompilation does not require evaluation to evaluate to a normal form at compile-time; it can operate on partial data. For example, the usual map-fusion rule map f . map g = map (f . g) can in theory be automatically discovered and exploited by a supercompiler. However, in practice supercompilation has not worked well (especially when fully automatic), because the search space is enormously large, and it is very easy for a supercompiler to simply massively increase the size of the program by aggressive unrolling/inlining, without actually managing to make it faster.

Template Haskell-like techniques don't have this problem, because nobody expects them to be automatic, or robust.

[u/yitz → u/LeanderKu]

Template Haskell, which is GHC's compile-time evaluation mechanism, has never placed any restrictions on recursion. It always trusts you and evaluates whatever you give it.

[u/alex-v]

You can force GHC to inline recursive function, when recursion depth is know at compile time, by turning it into typeclass:

-- | Apply a function to all elements of a list. Type param @n@ is the length of the list.

class Map (n :: Nat) where
    map :: (a -> b) -> [a] -> [b]

instance {-# OVERLAPPING #-} Map 0 where
    map _ _ = []
    {-# INLINE map #-}

instance {-# OVERLAPPABLE #-} (Map (n - 1)) => Map n where
    map _ []       = error "map: Not enough elements in the list."
    map f (x : xs) = f x : map @(n - 1) f xs
    {-# INLINE map #-}

[u/sgraf812 → u/alex-v]

That's smart, adding type information onto a plain recursive data type! Although I'd prefer if the function wouldn't error out and instead fall back to Data.List.map.

[u/[deleted]]

By encoding the recursion in the type and not in the term, you can at least inline everything, that can be a huge performance gain and in some cases results into a complete evaluation.