The Monomorphizer

Monomorphizer in the Scilla Compiler

This document describes the monomorphizer [3] (specialization of polymorphic expressions) in the Scilla compiler. The compiler pass consists of the following components: (1) AST initialization (2) Type-flow analysis (3) Monomorphization

AST Initialization

We associate with each AST node, a TFA (type-flow-analysis) index. This index is the offset into a global array of tfa_els (short for TFA element). Each tfa_el contains the data-flow information we're tracking for that AST node.

Type-flow Analysis

The goal of the type-flow analysis is to compute, for each tfun 'A expression, the set of closed types that may be substituted for 'A at runtime (via the @ operator). To achieve this, the analysis keeps track of

1. The flow of closed types from the argument of a type instantiation expression @foo, to the type variable 'A of the tfun 'A expressions that foo may resolve to at runtime.
2. The flow of tfun expressions.
3. Control-flow analysis: the flow of fun expressions to improve the precision of the analysis.

(2) is carried out using the same constraints as done for control-flow analysis. (2) and (3) is performed without context sensitivity. (1) is context sensitive.

Analysis data element tfa_el

  (* The context of free variables in a (type) closure. *)
  type context_env = Context.t IntMap.t

  (* We track the flow of Funs and TFuns as a pair of tfa_data index
   * and the context environment of its free type variables. *)
  type clo_env = int * context_env

  type rev_ref = ExprRef of expr_annot ref | VarRef of eannot Identifier.t

  (* Data element propagated in the type-flow analysis. *)
  type tfa_el = {
    (* The TFun expressions that reach a program point or variable. *)
    reaching_tfuns : CloSet.t;
    (* The Fun expressions that reach a program point or variable. *)
    reaching_funs : CloSet.t;
    (* The closed types that reach a type variable, in a given context. *)
    reaching_ctyps : TypSet.t Context.Map.t;
    (* A back reference to who this information belongs to. *)
    elof : rev_ref;
    (* The free type variables at a TFun.
     * Useful in building the context_env for reaching_tfuns. *)
    free_tvars : int list;
    (* Is fun being analyzed already? *)
    on_analysis_stack : bool;
  }

The terms context environment is used as in [1]. The flow of both tfun and fun expressions track the flow of clo_env, which is a pair of the closure itself (identified by its TFA index) and the environment for its free type variables.

The Analysis

The analysis is an AST walk, repeated until there is no change to the tfa_el associated with any of the AST nodes. TFA elements are updated during the analysis by an include_in : ~a:tfa_el -> ~b:tfa_el -> (tfa_bol * bool) function which includes the sets in b into that of a. This is the data-flow analysis merge operation (compiler text books typically use a lattice meet operation to represent this, while program analyses texts denote it as a lattice join operation). The include_in function simply performs set inclusion for each of the three constituents of the analysis and returns if anything changed in a.

The environment for the analysis itself is defined as

  type tfa_env = {
    (* The contexts of currently free type variables. *)
    ctx_env : context_env;
    (* The current calling context. *)
    cctx : Context.t;
  }

I next outline what the analysis does for relevant AST node types. In each case, whenever a set inclusion is computed, changes, if any are noted, and will lead to one more iteration of the analysis. For an expression e:

1. App (f, actual_args): Three operations are performed at function applications. For each tfun expression f' that may flow into f:
   1. The TFA information from the actual arguments are included in the TFA information of the corresponding formal arguments of f'.
   2. The body of f' is analyzed.
   3. The TFA information from the body of f' is included in the TFA information of function application we are currently analyzing.
2. TFun _ | Fun _ : The expresssion e is included in its own corresponding TFA information (reaching_tfuns and reaching_funs respectively), with the right context environment for the free type variables (recall that we track the reaching closures as a pair of the closure itself and the context environment for its free type variables).
3. TApp (tf, targs):
   1. For each free type variable 'A in the current context, the set of types that may flow into 'A is queried.
   2. For each targ in targs, substitute the free type variables in targ with the set of types that may flow into them. This involves computing all possible permutations into a final set of closed types targ_specls for each targ. For example, if we have @foo 'X -> 'Y and in the current context, 'X has Int32, Int64 flowing into it, and 'Y has String and ByStr20 flowing into it, then the actual parameter (there is only one in this example) will have the set of closed types targ_specls computed as Int32 -> String, Int32 -> ByStr20, Int64 -> String and Int64 -> ByStr20.
   3. The current context is appened with this TApp site
   4. apply env tf [targ :: remaining_args]: For each tfun 'A expression tf' that flows into tf, do the following:
      1. targ's specializations computed earlier (targ_specls) is included into the formal argument 'A.
      2. tf''s sub-expression tf'_subexpr is analyzed, with an updated current context that includes 'A as a free type variable.
      3. The environment is updated to include 'A as a free type variable. Let's call this env'.
      4. apply recursively: apply env' tf'_subexpr remaining_args.
      5. As a precision improvement heuristic, before applying tf'_subexpr, we remove those reaching_tfuns in it whose context environments are incompatible with the current one. This is helpful because reaching_tfuns is not context sensitive.

Non-termination Issue

Consider the following church encoded natural numbers and an exponentiation function for it written in Scilla.

(* Church-encoded natural numbers *)
(* zero *)
let c0 = tfun 'X => fun (s : 'X -> 'X) => fun (z : 'X) => z
in
(* one *)
let c1 = tfun 'X => fun (s : 'X -> 'X) => fun (z : 'X) => s z
in
(* two *)
let c2 = tfun 'X => fun (s : 'X -> 'X) => fun (z : 'X) => let sz = s z in s sz
in
(* exponentiation *)
let cexp : (forall 'X. ('X -> 'X) -> 'X -> 'X) -> (forall 'X. ('X -> 'X) -> 'X -> 'X) -> (forall 'X. ('X -> 'X) -> 'X -> 'X) =
  fun (m : forall 'X. ('X -> 'X) -> 'X -> 'X) =>
  fun (n : forall 'X. ('X -> 'X) -> 'X -> 'X) =>
  tfun 'X =>
  let ni = @n ('X -> 'X) in
  let mi = @m 'X in
  ni mi
in
(* Convert Church-encoded nats to Uint32 *)
let church_nat_to_uint32 : (forall 'X. ('X -> 'X) -> 'X -> 'X) -> Uint32 =
  fun (c : forall 'X. ('X -> 'X) -> 'X -> 'X) =>
    let zero = Uint32 0 in
    let one = Uint32 1 in
    let add1 = fun (x : Uint32) => builtin add one x in
    let c32 = @c Uint32 in
    c32 add1 zero

When used as below results in the type-flow analysis going into an infinite loop.

let c4 = cexp c2 c2 in
let c256 = cexp c4 c4 in
church_nat_to_uint32 c256

This is because, in the type application @n ('X -> 'X) in cexp, on of the possible tfuns that reach n is the tfun 'X that is right above in the previous line (in cexp itself). This results in an infinite expansion of Uint32 -> Uint32, (Uint32->Uint32) -> (Uint32->Uint32) and so on being propagated into the formal argument 'X.

Infinite types The type-flow analysis aside, more investigation lead to the realization that we can actually have types growing in Scilla, not obvious statically.

let c1 = cexp c1 c1 in
let c1 = cexp c1 c1 in
let c1 = cexp c1 c1 in
let c1 = cexp c1 c1 in
let res = c1 in
church_nat_to_uint32 res

Here, types grow exponentially at run-time.That’s because when you reduce exponent it does not reduce fully, but creates a lot of deferred function applications which actually causes the blowup, despite the value being very small (all the intermediate results and the final one correspond to 1).

While here, with a more sophisticated analysis, we may be able to statically determine the possible runtime types (for monomorphization), a similar setup inside a loop makes it impossible to do so.

let four = Uint32 4 in
let n = builtin to_nat four in
let folder = @nat_fold (forall 'X. ('X -> 'X) -> 'X -> 'X) in
let accf =
  fun (c : forall 'X. ('X -> 'X) -> 'X -> 'X) =>
  fun (i : Nat) =>
    cexp c c
in
let res = folder accf c2 n in
church_nat_to_uint32 res

This means that we cannot always monomorphize Scilla programs and need to define a subset that can indeed be monomorphized. While a fallback is of course to disallow non-prenex polymorphism, we could likely do better.

Current proposals:

1. For every type application, the type arguments must satisfy the following condition: The type argument must either be a closed type, or a unit function of a type variable. i.e., while @foo 'A is allowed, foo ('A -> 'A) or any other function of 'A wouldn't be allowed.

This might be too conservative. For example, we have the following line in ListUtils for list_map: let foldr = @list_foldr 'A (List 'B) in, and it obviously fails the test.

2. A relaxed version of (1) where the restriction on the arguments to the type application is relaxed if there is no higher-kinded type involved. In our example above, n contributes to the type of cexp being non-prenex, and hence wouldn't qualify. Note that this relaxation is yet to be defined formally / isn't well defined.
3. [Represent infinitely expanding types (like the one above) at runtime] via some sort of stat transitions systems. Totally unpractical, though.

Current fix:

Flow of types is now analyzed by tagging types with TApps through which that type has flowed through. This means reaching_ctyps : TypSet.t Context.Map.t; is now Int.Set.t TypMap.t Context.Map.t. When analyzing at a TApp, if a type flowing in already has that TApp's index tagged, then there's a cycle. If that TApp isn't a simple type variable occurrence, i.e., just 'A, then there's a possibility of growth of types. We reject the program. See https://github.com/Zilliqa/scilla-compiler/pull/56.

Monomorphization (Specialization of TFun expressions)

TBD

Current Remarks

• Mixing impredicativity under folds makes us as powerful as polymorphic recursion. This is bad news for the type-flow analysis.
• If we forbid impredicativity under folds, this removes a part of the problem that has to do with polymorphic recursion. It doesn't solve the entire problem, as we still have int32_to_nat, which means even for recursion-free programs we can't predict the static set of types in the presence of something like Church numerals with exponentiation.
• I am still hopeful that those types can be compiled to some runtime function-producing structure due to their regularity. And this something can be extracted from the analysis. But this is another story...
• So far, Vaivas' solution that combines non-expansiveness and cycles in the analysis seems like the best practical one. That said, it's still not fully formal.

References:

1. Principles of Program Analysis by Flemming Nielson, Hanne R. Nielson, Chris Hankin.
2. An Efficient Type- and Control-Flow Analysis for System F - Adsit and Fluet.
3. https://github.com/Zilliqa/scilla-compiler/blob/master/src/astlowering/Monomorphize.ml