Implement the "Static Argument" transformation

[plt-amy]

The idea of the SAT as an optimisation is to reduce the number of arguments that must be passed to a recursive function, and, subsequently, the argument shuffling noise.

Example:

let map @a @b (f : a -> b) (xs : list a -> list b) =
  match xs with
  | [] -> [] @a
  | Cons (x, xs) ->
    let x = f x
    let xs = map @a @b f xs
    Cons (x, xs)

Here, the recursive call to map is always made with the same arguments @a, @b, f and xs. We call these the "static arguments" of map. We can lift them out of the recursive path:

let map @a @b (f : a -> b) =
   let rec map_sat (xs : list a -> list b) =
     let map_shadow @a @b (f : a -> b) (xs : list a -> list b) =
       map_sat xs
     match xs with
     | [] -> [] @a
     | Cons (x, xs) ->
       let x = f x
       let xs = map_shadow @a @b f xs
       Cons (x, xs)
   map_sat

Then, the shadow can inline:

let map @a @b (f : a -> b) =
   let rec map_sat (xs : list a -> list b) =
     match xs with
     | [] -> [] @a
     | Cons (x, xs) ->
       let x = f x
       let xs = map_sat xs
       Cons (x, xs)
   map_sat

Now the only parameter we have to pass in the recursive loop is 'xs'.

[SquidDev]

I get the terrible feeling that the call-finding code will behave badly when working with non-saturated usages. For instance, I believe the following:

external val opaque_id : 'a -> 'a = "function(x) return x end"
let map : forall 'a 'b. ('a -> 'b) -> list 'a -> list 'b = fun f -> function
| [] -> []
| Cons (x, xs) -> 
  let _ = (opaque_id map) id [1] (* Non-saturated usage of map *)
  Cons (x, map f xs)

would be converted into:

let map : forall 'a 'b. ('a -> 'b) -> list 'a -> list 'b = fun f -> 
  let rec worker xs =
    let map_shadow f xs = worker xs
    match xs in
    | [] -> []
    | Cons (x, xs) -> 
      let _ = (opaque_id map_shadow) id [1]
      Cons (x, map f xs)

which is not type correct.

The "solution" here would be to track when call variables are used in non-saturated contexts (i.e. any atom not in the function position of an application), and thus only perform the substitution on saturated calls. Yes, I realise this would be annoying to trace. I'll have a little think about it - afraid I'm visiting family today.

[plt-amy]

which is not type correct.

Not so! Any usage of the original function can be safely replaced by the shadow. Your function does get SAT'd and passes Core Lint. I'll add it as a test case.

[plt-amy]

Ok I was wrong. It's type-correct but it's not correct-correct. Fix comin' up.