Mutable parameters

[UnsignedByte]

Now that existential types are implemented, this opens up the possibility of using components that we can treat almost "latency insensitively", meaning a component with some existential output latency that we have minimal information about that we have to treat sort of like a black box.

Chaining such components, however, is currently pretty complex. For example, let us have some component Calc that performs some complex calculation internally, defined as follows:

comp Calc[W, I]<'G: L>(
    go: interface['G],
    in: ['G, 'G+1] W
) -> (
    out: ['G+L, 'G+L+1] W
) with {
    exists L;
} where W > 0 {
   exists L = I;
   // I is used here just to change the behavior of the component based on the index in the list.

   delay := new Shift[W, L]<'G>(in);
   out = delay.out;
}

Chaining these currently would have to be done recursively (as parameters are immutable) as follows:

comp CalcChain[W, I]<'G, L>(
   go: interface['G],
   in: ['G, 'G+1] W
) -> (
    out: ['G+L, 'G+L+1] W
) with {
    exists L;
} where W > 0 {
   if I == 0 {
      exists L = 0;
      out = in;
   } else {
      chain := new CalcChain[W, I-1]<'G>(in);
      calc := new Calc[W, I-1]<'G+chain::L>(chain.out);
      out = calc.out;
      exists L = chain::L + calc::L;
   }
}

This would require us to implement a new component every time we do something similar to this, and, frankly, is a lot less intuitive than doing so in a for loop. Maybe we could consider looking into enabling mutable parameters so that we could do things like this in a much easier way?

[rachitnigam]

This is certainly a problem I was thinking about as well! A tricky thing about mutability is that it would make the verification of parameteric designs hard. Right now, let-bound parameters are not even represented in the IR; they get immediately inlined into their use locations. However, mutability will not allow for this kind of inlining. This is not that big a problem but does require thought.

The big problem is that it would be hard to figure out how to encode constraints on parameter that are mutated:

L = 0;
...
if C > 10 {
  L += 10
} else {
  L += 20
}

If we want to prove that L > 10, we'd have to build a complex constraint to make it work.

FWIW, bundles also came into existence to solve a similar problem: it was not possible to refer to ports defined in different iterations of a loop. The same problem now exists with parameter. Is there a different representation that we can use that retains immutability and ease of encoding?

[UnsignedByte]

Theoretically if we did something like bundle with parameters (such as an array) I think that could solve most of our issues. We could imagine fixing most of the for loop parameter issues with something like the following non-recursive version of CalcChain:

// somehow tell the compiler here that Delays exists, and ensure that each index is bound exactly once later on
let Delays[N+1]; 
// we can use `Delays[j]` before it is bound here because we know it will be bound by compile time
bundle connections[N + 1]: for<j> ['G+Delays[j], 'G+Delays[j]+1];
connections{0} = in;
Delays[0] = 0;
for i in 0..N {
   calc := new Calc<'G+Delays[i]>(connections{i});
   connections{i+1} = calc.out;
   Delays[i+1] = Delays[i] + calc::L;
}
out = connections{N};
exists L = Delays[N];

Sorry if the code isn't exactly correct, but while something like this is still somewhat tedious as we need to separately store delay information and port information. An alternative that might be even simpler is somehow giving access to a port's liveness information, but that will probably lead to unsafe code/abuse so we would definitely have to restrict that somehow.

[UnsignedByte]

Question from meeting with @rachitnigam: How do we type check above? There are some restrictions on the possible values of Delay: we require that Delay[i] > Delay[i-1] (specifically that it is equal to the i-1th calc's L), but as loops are not unrolled during typechecking, this is difficult to tell the solver. We might need some sort of notation similar to how bundles are implemented that will allow us to type check properly.