Existentially quantified parameters

[rachitnigam]

Parameters in Filament are universally quantified. For example, for the following module:

comp Foo[#W]() -> () where #W >= 32 { ... }

The parameter #W is universally quantified: forall values of #W that respect the constraints, we generate a component that is well-pipelined. Such universal quantification allows the calling context to decide how to use the module by providing a concrete instantiation for #W. In return, the calling context must prove that the binding for #W satisfies the constraint.

Existential types are the dual of universally quantified types. Instead of the calling context deciding how to use the module, the module tells the context how it's allowed to use it. For example:

comp ShiftSome[exists #L]<G: 1>(@[G, G+1] in: 32) -> (@[G+#L, G+#L+1] out: 32) 

This module delays the signal by some amount #L that is unknown to the calling context. Instead, when the calling context instantiates a shift circuit, it must use the specific instance of #L bound to that ShiftSome component:

comp main<G: 1>(... in: 32) -> () {
  S := new ShiftSome; // We don't provide a parameter here
  s0 := S<G>(in);
  mux := new Mux[32]<G+S.#L>(sel, s0.out, ...); // Scheduling must use S.#L to correctly use the signal s0.out
}

Note that when scheduling this program, we have to use S.#L to schedule things. S.#L is unknown when we write the program but will turned into a concrete value during compilation. While all invocations of S will get the same constant, different instantiations of ShiftSome might get different values of #L. This is important because it opens the door to something really cool–per-instance retiming.

Constraints on existential parameters must be satisfied by the body of the component defining them and can be assumed by the calling context.

Compilation

The compilation strategy for existentials involves turning them into universally quantified types. This has the effect of turning the quantifiers "inside out". For each instance, we decide (somehow), the binding for each existential variable and replace all instantiations to use those constants. For example, in the above program, if we decide #L=10 is a good binding for the variable, we change:

S := new ShiftSome;

Into:

S := new ShiftSome[10]

And make the signature of the component take to have #L be universally quantified parameter.

This is not fully developed yet but I think it's a good starting point.

[rachitnigam]

One way to measure the success of this feature is implementing a generic version of the Aetherling conv2d stencils and providing them with a "compute" module inside the hierarchy. The idea is that depending on the parameters exposed by the compute module, the rest of the hierarchy should reconfigure itself to implement one of the design points reported in the original Aetherling paper. This way, we can claim to implement Aetherling's entire design space with just one implementation.

[rachitnigam]

Here is an example program that we can start with:

import "primitives/core.fil";

comp Mul[#W]<G:1>(
    left: [G, G+1] #W,
    right: [G, G+1] #W
) -> (
    out: [G+#L, G+#L+1] #W
) with {
    exists #L;
} where #L > 0 {
    mult := new MultComb[#W]<G>(left, right);
    sh := new Shift[#W, #L]<G>(mult.out);
    out = mult.out;

    // This is the hidden value of the quantified parameter. This value is not
    // visible to callers.
    exists #L = 3;
}

// The main component is allowed to use existentially quantified variables.
// These are removed during monomorphization.
comp main<G:1>(in: [G, G+1] 32) -> (out: [G+#L, G+#L+1] 32) with {
    exists #L;
} where #L > 0 {
    // Explicitly define the instance because we need to access the parameter.
    M0 := new Mul[32];
    mul0 := M0<G>(in, in);

    // The next invoke is scheduled using the existentially quantified parameter.
    M1 := new Mul[32];
    mul1 := M1<G+M0.#L>(mul0.out, mul0.out);

    out = mul1.out;
    // This module defines the (hidden) relationship that the latency is the sum of the
    // the latencies of the two instances.
    exists #L = M0.#L + M1.#L;
}