Compiling Juvix to Michelson

1. Minimizing the number of dups

   An illustrative example is the following

   let f x = x
   

   Since Michelson lambdas have a high cost and it is quite limited in the forms it accepts, we opt to beta expand most lambdas away. Juvix is in a unique position due to part of our type theory known as Quantitative Type Theory (QTT), which tracks the usage of all variables. Under a normal compiler pipeline this would mean that most structures can avoid being in garbage collection, however for Michelson this means we can eliminate a single dup and dig drop. Thus, if were to compile the application of f within some nested computation where the x is stored five slots back in stack, then without QTT or some notion of linearity then the expansion would look like the following.

   5 dug dup 6 dig
   

   Indeed, there would be no way of knowing that it's safe to completely move away. However, if we were to consider Quantitative Type Theory, with x only being used once then we can always safely write

   5 dug
   

2. Placement of variables after lookup
   A more generic optimization is looking up a variable from the environment, which effectively caches the value on the stack until it is consumed.
   
   Let us consider the function f below where the usage of x is 3. Let us consider the application where x is 5 slots away.

   let f = x * x
   

   Then the generated code would be.

   5 dug dup 6 dig dup *
   

   Thus we can see that we did not have to do another dug dig combo, but instead dup the current variable.

   This technique relies on propagating usages effectively, as we have to know whether to dup a value or just move it to be consumed. As currently implemented, there is one restriction that will make this behavior less optimal than it should be. These inefficiencies will be discussed in the next section.

For those unfamiliar with currying, in an ML family language, functions only take a single argument.

f a b c = times (a + b + c)


g = f 2 3

h = g 5 6

l = f 2 3 5 6

j = f 2 3 4

Although it may look like each function takes multiple arguments, notice how this example works. f explicitly takes 3 arguments up front (named a b and c), but in reality takes a fourth unarmed argument. As application goes we show sending in 2 arguments to f twice, showing that you can partially apply f and get back a new function that takes two more arguments, where h finally makes it whole. We also can see that we can send in more arguments than there are names for and also the exact number of arguments. When compiling down to a language without curry semantics, it's quite important to get this optimization right.

1. Lambda Removal

   As discussed above, Lambdas are expensive, so we do beta reduction and inlining aggressively to avoid them. This beta reduction does not move the values on the stack at all, instead just naming them for when they are actually used.
   
   Beta reduction in Michelson turn out to be safe due to the limitations of what can be expressed in Michelson. Firstly, Michelson doesn't allow for custom types, instead providing their own data structures. So we currently can't send in any recursive structures, such as a list. Secondly, Michelson lacks functions and the typing to support converting recursive functions into CPS style (Michelson only has first-order typing). Thus all simple tail recursive functions will have to be translated into a Michelson loop before being sent into the backend.

2. Virtual stack

   This was also discussed above, we will just note items stored on the virtual stack that is not stored on the Michelson stack:

   1. Partially-applied functions

   2. Constants

      Specifically, these are propagated even through primitive functions if all the arguments are constants!

1. More Effective usage movement
   
   Currently, when we move a variable forward, we move all usages except 1 forward with it unless the variable only has one usage left. This means, we always keep behind a copy of the variable behind.
   
   Let us see the example we used before.

   let f = x * x
   

   Let us suppose x, like before, is five positions back, however now consider the usage of x being used twice and thrice.
   
   Twice:

   5 dug dup 6 dig 6 dug *
   

   thrice (as before):

   5 dug dup 6 dig dup *
   

   As we can see, if we only use x twice we pay a cost of digging five again to move the copy over. The first x we moved over has a usage one where we are going to use it right away, so this usage is saved. Thus the only free x is the one six stack positions away!
   
   A smarter plan would be to just move all the usages up, and if any usages are left over after using them, move them right before the consumption point.
   
   So to illustrate, consider the same example from above:
   
   Twice:

   5 dug dup *
   

   Thrice (as before):

   5 dug dup dup 3 dip *
   

   Notice this is much more efficient, as we don't have to go six positions back immediately, and when we do have to leave a copy behind it is only the minimum number three slots away.
   
   However this optimization is not safe currently. Consider the example below:

   f a (x + y) b
   

   If we were to do this technique with x and y having extra usages, then moving them back would cause b to no longer be an argument, instead replacing it with themselves!
   
   Once ANF form is up, the computation will instead be like this

   let xy0 = x + y in
   f a xy0 b
   

   where every function takes primitives, so these moves would have happened before, thus allowing this optimization to take place.

2. Loop fusion

   Another benefit of ANF is that with the extension of join points, we can effectively fuse (merge) independent loops into a single loop when they are composed together. This optimization will only show on operations through numbers sadly, as recursive structures in Michelson that are not primitive are not permitted.