Dependent vector types for data structuring in multirate Faust

Faust is a functional programming language dedicated to the specification of executable monorate synchronous musical applications. To extend Faust capabilities to important domains such as FFT-based spectral processing, we introduce here a multirate extension of the core Faust language. The novel idea is to link rate changes to data structure manipulation operations. Creating a vector-valued output signal divides the rate of input signals by the vector size, while serializing vectors multiplies rates accordingly. As duals to vectors, we also introduce record-like data structures, which are used to gather data but do not change signal rates. This interplay between data structures and rates is made possible in the language static semantics by the introduction of dependent types. We present a typing semantics, a denotational semantics and correctness theorems that show that this data structuring/multirate extension preserves the language synchronous characteristics. This new design is under implementation in the Faust compiler.

► The DSP language Faust provides multirate and structured-data-based capabilities.
► Vector primitives are signal rate transformers.
► Dependent typing is a powerful technique to enable efficient vector operations.