comped function optimization with linear pattern-match on HVM - full example

compiled_function_optimization_example.md

The function:

data T = (A a b ...) | (B a b ...)

F = λx λr λs
  match x with rs = (+ r s) {
    A: (ret x.a x.b rs)
    B: (ret x.a x.b rs)
  }

Gets compiled to:

F = λx λr λs ((x
  λaλbλrs(R a b rs) // A-case
  λaλbλrs(R a b rs) // B-case
) (+ r s))

And called as:

x = (F λAλB(A 1 2) 10 20)

(From now on, I will use {{x}} to signal that x is a static term.)

({{ λxλrλs((x λaλbλrs(R a b rs) λaλbλrs(R a b rs)) (+ r s)) }} λAλB(A 1 2) 10 20)

We start by noticing we have 3 lams vs 3 apps, so we can substitute x r s statically. So, now we have:

{{ (x λaλbλrs(R a b rs) λaλbλrs(R a b rs) (+ r s)) }}

closure:
x <- λAλB(A 1 2)
r <- 10
s <- 20

Now, we have x on head position, so we consume it, making it a static term:

{{ (λAλB(A 1 2) λaλbλrs(R a b rs) λaλbλrs(R a b rs) (+ r s)) }}

closure:
r <- 10
s <- 20

Now, once again, we have 2 lams vs 2 apps, so we can substitute A B statically. So, now we have:

{{ (A 1 2 (+ r s)) }}

closure:
r <- 10
s <- 20
A <- {{ λaλbλrs(R a b rs) }}

Now, once again, we have A in a head position, so, we consume it:

{{ (λaλbλrs(R a b rs) 1 2 (+ r s)) }}

closure:
r <- 10
s <- 20

Now, again, we have 3 lams vs 3 apps, so we can substitute a b rs statically. So, now we have:

{{ (R a b rs) }}

closure:
r <- 10
s <- 20
a <- 1
b <- 2
rs <- (+ r s)

Now, we have R on head position, but it is not in the static closure; it is a REF, which can be seen as a rigid var. As such, we're forced to return (allocate). We call:

ctx = [ r <- 10 ; s <- 20 ; a <- 1 ; b <- 2 ; rs <- (+ r s) ]

<ALLOC {{ (R a b rs) }} ctx>

This will result in:

(R <REDUCE a ctx> <REDUCE b ctx> <REDUCE rs ctx>)

Which will then continue doing static reductions:

1. First recursive call:

{{ a }}

closure:
r <- 10
s <- 20
a <- 1
b <- 2
rs <- (+ r s)

This will just consume a and return 1.

2. Second recursive call:

{{ b }}

closure:
r <- 10
s <- 20
b <- 2
rs <- (+ r s)

This will just consume b and return 2.

3. Third recursive call:

{{ rs }}

closure:
r <- 10
s <- 20
rs <- (+ r s)

This will consume rs, so now we have:

{{ (+ r s) }}

closure:
r <- 10
s <- 20

Now, on "head position" we don't have a rigid var, but a native operation, +. So, we reduce r, s, and then proceed:

{{ (+ 10 20) }}

Which triggers the static (+ 10 20) evaluation. So, in the end, we must allocate:

(((R 1) 2) 30)

Note that we only allocated 3 APP nodes. The rest of this computation was done fully statically.

...