Inlining in PureLang

[myreen]

Here are some plans for the PureLang inliner.

The PureLang inliner implementation is to carry only let bindings that it can inline. The relational proofs are allowed to be more general.

I believe it only makes sense to carry:

• small-ish functions (for example, specialisations of foldr, map, etc.), and
• very simple non-function expressions: individual variables and constant expressions, such as 5, Nothing and [], but nothing more complicated because that would essentially be the reverse of common-subexpression elimination.

When the inliner comes across a letrec, it ought to try to specialise the letrec as the examples below suggests. If the specialisation was possible, then the inliner should do two things:

1. The inliner should output the new specialised version of the letrec (regardless of the next point)
2. The inliner should decide whether it wants to use the new specialised function as new let binding used for optimisation. This decision should be yes for small functions and no for large functions.

Inliner's actions when encountering the definition of the map function

letrec
  map = lam f xs -> ... f ... map f ys ...
in ...

At this point the inliner should call a new function, called specialise, which will attempt to turn this letrec definition into a let definition.

specialise `map` `lam f xs -> ... f ... map f ys ...` =
  SOME `lam f xs ->
          letrec
            map = lam xs -> ... f ... map ys ...
          in map xs`

which means that we know:

  letrec
    map = lam f xs -> ... f ... map f ys ...
  in rest
≅
  let
    map = lam f xs ->
            letrec
              map = lam xs -> ... f ... map ys ...
            in map xs
  in rest

The inliner should then conceptually produce this:

let
  map = lam f xs ->
          letrec
            map = lam xs -> ... f ... map ys ...
          in map xs
in ...

which after freshening becomes:

let
  map = lam f xs ->
          letrec
            map' = lam xs' -> ... f ... map' ys' ...
          in map' xs
in ...

In this case, the inliner should decide whether to learn this as a rewrite (for map, the decision should be yes). It should then recurse into ... without decrement any max depth counter. It should also recurse into the left-hand side of the lam f xs -> and decrement a counter when doing so.

Inliner's actions when encountering full application of map

We assume that the inliner knows that map is:

        lam f xs ->
          letrec
            map' = lam xs' -> ... f y ... map' ys' ...
          in map' xs

When it arrives at a complete application of map, i.e.

        map (lam x -> 5) ys

The inliner should conceptually produce:

        (lam f xs ->
          letrec
            map' = lam xs' -> ... f y ... map' ys' ...
          in map' xs) (lam x -> 5) ys

which needs to be changed into a lets:

          let f = (lam x -> 5) in
          let xs = ys in
          letrec
            map' = lam xs' -> ... f y ... map' ys' ...
          in map' xs

The inliner should now recurse (after decrementing a max depth counter). The result of such a recursion could be:

          let f = (lam x -> 5) in
          let xs = ys in
          letrec
            map' = lam xs' -> ... 5 ... map' ys' ...
          in map' ys

Furthermore, a subsequent deadcode elimination pass might turn the above into:

          letrec
            map' = lam xs' -> ... 5 ... map' ys' ...
          in map' ys

[myreen]

For map, the specialise function should actually generate:

specialise `map` `lam f xs -> ... f ... map f ys ...` =
  SOME `lam f ->
          letrec
            map = lam xs -> ... f ... map ys ...
          in map`

because we want map (map (lam x -> 5)) to be specialised.

From the inliner's point of view, map is fully applied when applied to one argument.